%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR109+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 : n004.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:21 AM UTC 2026
% Result : Theorem 90.50s 16.46s
% Output : Refutation 90.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 33
% Syntax : Number of formulae : 228 ( 38 unt; 25 def)
% Number of atoms : 1025 ( 0 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 1500 ( 703 ~; 660 |; 107 &)
% ( 24 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 26 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 16 con; 0-0 aty)
% Number of variables : 112 ( 0 sgn 72 !; 40 ?)
% 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(f1291,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__subclass(X1,X2) )
=> s__subclass(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_1294) ).
fof(f5923,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5997) ).
fof(f5952,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6026) ).
fof(f6026,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6100) ).
fof(f7219,axiom,
( s__subclass(s__Reptile,s__Animal)
=> ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f7220,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f7221,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(negated_conjecture,[status(cth)],[f7220]) ).
fof(f7225,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(flattening,[],[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(f8540,plain,
! [X0,X1,X2] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f1291]) ).
fof(f8541,plain,
! [X0,X1,X2] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f8540]) ).
fof(f12410,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(ennf_transformation,[],[f7219]) ).
fof(f12460,definition,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f12461,plain,
( sP26
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(definition_folding,[],[f12410,f12460]) ).
fof(f13034,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) )
| ~ sP26 ),
inference(nnf_transformation,[],[f12460]) ).
fof(f13035,plain,
( ( s__instance(sK505,s__SetOrClass)
& s__instance(sK506,s__SetOrClass)
& s__instance(sK507,s__SetOrClass)
& s__instance(sK508,s__SetOrClass)
& s__instance(sK509,s__SetOrClass)
& s__instance(sK510,s__SetOrClass)
& s__instance(sK511,s__SetOrClass)
& s__instance(sK512,s__SetOrClass)
& s__instance(sK513,s__SetOrClass)
& s__instance(sK514,s__SetOrClass)
& s__subclass(sK505,sK506)
& s__subclass(sK506,sK507)
& s__subclass(sK507,sK508)
& s__subclass(sK508,sK509)
& s__subclass(sK509,sK510)
& s__subclass(sK510,sK511)
& s__subclass(sK511,sK512)
& s__subclass(sK512,sK513)
& s__subclass(sK513,sK514)
& s__subclass(sK514,s__Reptile)
& s__instance(s__Creature50_1,sK505) )
| ~ sP26 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK505,sK506,sK507,sK508,sK509,sK510,sK511,sK512,sK513,sK514]),skolemize(X0,sK505),skolemize(X1,sK506),skolemize(X2,sK507),skolemize(X3,sK508),skolemize(X4,sK509),skolemize(X5,sK510),skolemize(X6,sK511),skolemize(X7,sK512),skolemize(X8,sK513),skolemize(X9,sK514)],[f13034]) ).
fof(f14340,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7316]) ).
fof(f14341,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7316]) ).
fof(f14342,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(f15759,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f8541]) ).
fof(f21059,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[],[f5923]) ).
fof(f21088,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f5952]) ).
fof(f21164,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(cnf_transformation,[],[f6026]) ).
fof(f22563,plain,
( s__instance(s__Creature50_1,sK505)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22564,plain,
( s__subclass(sK514,s__Reptile)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22565,plain,
( s__subclass(sK513,sK514)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22566,plain,
( s__subclass(sK512,sK513)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22567,plain,
( s__subclass(sK511,sK512)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22568,plain,
( s__subclass(sK510,sK511)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22569,plain,
( s__subclass(sK509,sK510)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22570,plain,
( s__subclass(sK508,sK509)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22571,plain,
( s__subclass(sK507,sK508)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22572,plain,
( s__subclass(sK506,sK507)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22573,plain,
( s__subclass(sK505,sK506)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22574,plain,
( s__instance(sK514,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22575,plain,
( s__instance(sK513,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22576,plain,
( s__instance(sK512,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22577,plain,
( s__instance(sK511,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22578,plain,
( s__instance(sK510,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22579,plain,
( s__instance(sK509,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22580,plain,
( s__instance(sK508,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22581,plain,
( s__instance(sK507,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22582,plain,
( s__instance(sK506,s__SetOrClass)
| ~ sP26 ),
inference(cnf_transformation,[],[f13035]) ).
fof(f22584,plain,
( sP26
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[],[f12461]) ).
fof(f22585,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(cnf_transformation,[],[f7225]) ).
fof(f23020,definition,
( spl515_1
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl515_1])],[avatar_definition]) ).
fof(f23024,definition,
( spl515_2
<=> s__instance(s__Creature50_1,sK505) ),
introduced(definition,[new_symbols(definition,[spl515_2])],[avatar_definition]) ).
fof(f23026,plain,
( s__instance(s__Creature50_1,sK505)
| ~ spl515_2 ),
inference(avatar_component_clause,[],[f23024]) ).
fof(f23027,plain,
( ~ spl515_1
| spl515_2 ),
inference(avatar_split_clause,[],[f22563,f23024,f23020]) ).
fof(f23029,definition,
( spl515_3
<=> s__subclass(sK514,s__Reptile) ),
introduced(definition,[new_symbols(definition,[spl515_3])],[avatar_definition]) ).
fof(f23031,plain,
( s__subclass(sK514,s__Reptile)
| ~ spl515_3 ),
inference(avatar_component_clause,[],[f23029]) ).
fof(f23032,plain,
( ~ spl515_1
| spl515_3 ),
inference(avatar_split_clause,[],[f22564,f23029,f23020]) ).
fof(f23034,definition,
( spl515_4
<=> s__subclass(sK513,sK514) ),
introduced(definition,[new_symbols(definition,[spl515_4])],[avatar_definition]) ).
fof(f23036,plain,
( s__subclass(sK513,sK514)
| ~ spl515_4 ),
inference(avatar_component_clause,[],[f23034]) ).
fof(f23037,plain,
( ~ spl515_1
| spl515_4 ),
inference(avatar_split_clause,[],[f22565,f23034,f23020]) ).
fof(f23039,definition,
( spl515_5
<=> s__subclass(sK512,sK513) ),
introduced(definition,[new_symbols(definition,[spl515_5])],[avatar_definition]) ).
fof(f23041,plain,
( s__subclass(sK512,sK513)
| ~ spl515_5 ),
inference(avatar_component_clause,[],[f23039]) ).
fof(f23042,plain,
( ~ spl515_1
| spl515_5 ),
inference(avatar_split_clause,[],[f22566,f23039,f23020]) ).
fof(f23044,definition,
( spl515_6
<=> s__subclass(sK511,sK512) ),
introduced(definition,[new_symbols(definition,[spl515_6])],[avatar_definition]) ).
fof(f23046,plain,
( s__subclass(sK511,sK512)
| ~ spl515_6 ),
inference(avatar_component_clause,[],[f23044]) ).
fof(f23047,plain,
( ~ spl515_1
| spl515_6 ),
inference(avatar_split_clause,[],[f22567,f23044,f23020]) ).
fof(f23049,definition,
( spl515_7
<=> s__subclass(sK510,sK511) ),
introduced(definition,[new_symbols(definition,[spl515_7])],[avatar_definition]) ).
fof(f23051,plain,
( s__subclass(sK510,sK511)
| ~ spl515_7 ),
inference(avatar_component_clause,[],[f23049]) ).
fof(f23052,plain,
( ~ spl515_1
| spl515_7 ),
inference(avatar_split_clause,[],[f22568,f23049,f23020]) ).
fof(f23054,definition,
( spl515_8
<=> s__subclass(sK509,sK510) ),
introduced(definition,[new_symbols(definition,[spl515_8])],[avatar_definition]) ).
fof(f23056,plain,
( s__subclass(sK509,sK510)
| ~ spl515_8 ),
inference(avatar_component_clause,[],[f23054]) ).
fof(f23057,plain,
( ~ spl515_1
| spl515_8 ),
inference(avatar_split_clause,[],[f22569,f23054,f23020]) ).
fof(f23059,definition,
( spl515_9
<=> s__subclass(sK508,sK509) ),
introduced(definition,[new_symbols(definition,[spl515_9])],[avatar_definition]) ).
fof(f23061,plain,
( s__subclass(sK508,sK509)
| ~ spl515_9 ),
inference(avatar_component_clause,[],[f23059]) ).
fof(f23062,plain,
( ~ spl515_1
| spl515_9 ),
inference(avatar_split_clause,[],[f22570,f23059,f23020]) ).
fof(f23064,definition,
( spl515_10
<=> s__subclass(sK507,sK508) ),
introduced(definition,[new_symbols(definition,[spl515_10])],[avatar_definition]) ).
fof(f23066,plain,
( s__subclass(sK507,sK508)
| ~ spl515_10 ),
inference(avatar_component_clause,[],[f23064]) ).
fof(f23067,plain,
( ~ spl515_1
| spl515_10 ),
inference(avatar_split_clause,[],[f22571,f23064,f23020]) ).
fof(f23069,definition,
( spl515_11
<=> s__subclass(sK506,sK507) ),
introduced(definition,[new_symbols(definition,[spl515_11])],[avatar_definition]) ).
fof(f23071,plain,
( s__subclass(sK506,sK507)
| ~ spl515_11 ),
inference(avatar_component_clause,[],[f23069]) ).
fof(f23072,plain,
( ~ spl515_1
| spl515_11 ),
inference(avatar_split_clause,[],[f22572,f23069,f23020]) ).
fof(f23074,definition,
( spl515_12
<=> s__subclass(sK505,sK506) ),
introduced(definition,[new_symbols(definition,[spl515_12])],[avatar_definition]) ).
fof(f23076,plain,
( s__subclass(sK505,sK506)
| ~ spl515_12 ),
inference(avatar_component_clause,[],[f23074]) ).
fof(f23077,plain,
( ~ spl515_1
| spl515_12 ),
inference(avatar_split_clause,[],[f22573,f23074,f23020]) ).
fof(f23079,definition,
( spl515_13
<=> s__instance(sK514,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_13])],[avatar_definition]) ).
fof(f23081,plain,
( s__instance(sK514,s__SetOrClass)
| ~ spl515_13 ),
inference(avatar_component_clause,[],[f23079]) ).
fof(f23082,plain,
( ~ spl515_1
| spl515_13 ),
inference(avatar_split_clause,[],[f22574,f23079,f23020]) ).
fof(f23084,definition,
( spl515_14
<=> s__instance(sK513,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_14])],[avatar_definition]) ).
fof(f23086,plain,
( s__instance(sK513,s__SetOrClass)
| ~ spl515_14 ),
inference(avatar_component_clause,[],[f23084]) ).
fof(f23087,plain,
( ~ spl515_1
| spl515_14 ),
inference(avatar_split_clause,[],[f22575,f23084,f23020]) ).
fof(f23089,definition,
( spl515_15
<=> s__instance(sK512,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_15])],[avatar_definition]) ).
fof(f23091,plain,
( s__instance(sK512,s__SetOrClass)
| ~ spl515_15 ),
inference(avatar_component_clause,[],[f23089]) ).
fof(f23092,plain,
( ~ spl515_1
| spl515_15 ),
inference(avatar_split_clause,[],[f22576,f23089,f23020]) ).
fof(f23094,definition,
( spl515_16
<=> s__instance(sK511,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_16])],[avatar_definition]) ).
fof(f23096,plain,
( s__instance(sK511,s__SetOrClass)
| ~ spl515_16 ),
inference(avatar_component_clause,[],[f23094]) ).
fof(f23097,plain,
( ~ spl515_1
| spl515_16 ),
inference(avatar_split_clause,[],[f22577,f23094,f23020]) ).
fof(f23099,definition,
( spl515_17
<=> s__instance(sK510,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_17])],[avatar_definition]) ).
fof(f23101,plain,
( s__instance(sK510,s__SetOrClass)
| ~ spl515_17 ),
inference(avatar_component_clause,[],[f23099]) ).
fof(f23102,plain,
( ~ spl515_1
| spl515_17 ),
inference(avatar_split_clause,[],[f22578,f23099,f23020]) ).
fof(f23104,definition,
( spl515_18
<=> s__instance(sK509,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_18])],[avatar_definition]) ).
fof(f23106,plain,
( s__instance(sK509,s__SetOrClass)
| ~ spl515_18 ),
inference(avatar_component_clause,[],[f23104]) ).
fof(f23107,plain,
( ~ spl515_1
| spl515_18 ),
inference(avatar_split_clause,[],[f22579,f23104,f23020]) ).
fof(f23109,definition,
( spl515_19
<=> s__instance(sK508,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_19])],[avatar_definition]) ).
fof(f23111,plain,
( s__instance(sK508,s__SetOrClass)
| ~ spl515_19 ),
inference(avatar_component_clause,[],[f23109]) ).
fof(f23112,plain,
( ~ spl515_1
| spl515_19 ),
inference(avatar_split_clause,[],[f22580,f23109,f23020]) ).
fof(f23114,definition,
( spl515_20
<=> s__instance(sK507,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_20])],[avatar_definition]) ).
fof(f23116,plain,
( s__instance(sK507,s__SetOrClass)
| ~ spl515_20 ),
inference(avatar_component_clause,[],[f23114]) ).
fof(f23117,plain,
( ~ spl515_1
| spl515_20 ),
inference(avatar_split_clause,[],[f22581,f23114,f23020]) ).
fof(f23119,definition,
( spl515_21
<=> s__instance(sK506,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_21])],[avatar_definition]) ).
fof(f23121,plain,
( s__instance(sK506,s__SetOrClass)
| ~ spl515_21 ),
inference(avatar_component_clause,[],[f23119]) ).
fof(f23122,plain,
( ~ spl515_1
| spl515_21 ),
inference(avatar_split_clause,[],[f22582,f23119,f23020]) ).
fof(f23129,definition,
( spl515_23
<=> s__subclass(s__Reptile,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl515_23])],[avatar_definition]) ).
fof(f23131,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| spl515_23 ),
inference(avatar_component_clause,[],[f23129]) ).
fof(f23132,plain,
( ~ spl515_23
| spl515_1 ),
inference(avatar_split_clause,[],[f22584,f23020,f23129]) ).
fof(f26857,definition,
( spl515_186
<=> s__instance(s__Animal,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_186])],[avatar_definition]) ).
fof(f26858,plain,
( s__instance(s__Animal,s__SetOrClass)
| ~ spl515_186 ),
inference(avatar_component_clause,[],[f26857]) ).
fof(f26859,plain,
( ~ s__instance(s__Animal,s__SetOrClass)
| spl515_186 ),
inference(avatar_component_clause,[],[f26857]) ).
fof(f26865,plain,
( ! [X0] : ~ s__subclass(X0,s__Animal)
| spl515_186 ),
inference(resolution,[],[f26859,f14340]) ).
fof(f26874,plain,
( $false
| spl515_186 ),
inference(resolution,[],[f26865,f21059]) ).
fof(f26877,plain,
spl515_186,
inference(avatar_contradiction_clause,[],[f26874]) ).
fof(f78524,plain,
! [X0] :
( ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(s__Reptile,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f14342,f22585]) ).
fof(f78551,plain,
! [X0] :
( ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f78524,f14340]) ).
fof(f78784,plain,
! [X0] :
( ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Creature50_1,X0) ),
inference(forward_subsumption_resolution,[],[f78551,f14341]) ).
fof(f97739,definition,
( spl515_643
<=> s__instance(s__Reptile,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl515_643])],[avatar_definition]) ).
fof(f97740,plain,
( s__instance(s__Reptile,s__SetOrClass)
| ~ spl515_643 ),
inference(avatar_component_clause,[],[f97739]) ).
fof(f97741,plain,
( ~ s__instance(s__Reptile,s__SetOrClass)
| spl515_643 ),
inference(avatar_component_clause,[],[f97739]) ).
fof(f98079,plain,
( ! [X0] : ~ s__subclass(s__Reptile,X0)
| spl515_643 ),
inference(resolution,[],[f97741,f14341]) ).
fof(f98107,plain,
( $false
| spl515_643 ),
inference(resolution,[],[f98079,f21164]) ).
fof(f98114,plain,
spl515_643,
inference(avatar_contradiction_clause,[],[f98107]) ).
fof(f129074,plain,
( ! [X0] :
( ~ s__subclass(s__Reptile,X0)
| ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(s__Reptile,s__SetOrClass) )
| spl515_23 ),
inference(resolution,[],[f15759,f23131]) ).
fof(f129081,plain,
( ! [X0] :
( ~ s__subclass(s__Reptile,X0)
| ~ s__subclass(X0,s__Animal)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(s__Reptile,s__SetOrClass) )
| spl515_23
| ~ spl515_186 ),
inference(forward_subsumption_resolution,[],[f129074,f26858]) ).
fof(f129094,plain,
( ! [X0] :
( ~ s__subclass(s__Reptile,X0)
| ~ s__subclass(X0,s__Animal)
| ~ s__instance(X0,s__SetOrClass) )
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(forward_subsumption_resolution,[],[f129081,f97740]) ).
fof(f129107,plain,
( ! [X0] :
( ~ s__subclass(s__Reptile,X0)
| ~ s__subclass(X0,s__Animal) )
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(forward_subsumption_resolution,[],[f129094,f14340]) ).
fof(f129133,plain,
( ~ s__subclass(s__ColdBloodedVertebrate,s__Animal)
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(resolution,[],[f129107,f21164]) ).
fof(f129172,plain,
( ~ s__instance(s__Creature50_1,sK514)
| ~ spl515_3 ),
inference(resolution,[],[f23031,f78784]) ).
fof(f129209,plain,
( ! [X0] :
( ~ s__subclass(s__ColdBloodedVertebrate,X0)
| ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass) )
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(resolution,[],[f129133,f15759]) ).
fof(f129211,plain,
( ! [X0] :
( ~ s__subclass(s__ColdBloodedVertebrate,X0)
| ~ s__subclass(X0,s__Animal)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass) )
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(forward_subsumption_resolution,[],[f129209,f26858]) ).
fof(f129212,plain,
( ! [X0] :
( ~ s__subclass(s__ColdBloodedVertebrate,X0)
| ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass) )
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(forward_subsumption_resolution,[],[f129211,f14340]) ).
fof(f129213,plain,
( ! [X0] :
( ~ s__subclass(s__ColdBloodedVertebrate,X0)
| ~ s__subclass(X0,s__Animal) )
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(forward_subsumption_resolution,[],[f129212,f14341]) ).
fof(f129280,plain,
( ~ s__subclass(s__ColdBloodedVertebrate,s__Vertebrate)
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(resolution,[],[f129213,f21059]) ).
fof(f129281,plain,
( $false
| spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(forward_subsumption_resolution,[],[f129280,f21088]) ).
fof(f129282,plain,
( spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(avatar_contradiction_clause,[],[f129281]) ).
fof(f129302,plain,
( ! [X0] :
( ~ s__subclass(X0,sK514)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK514,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3 ),
inference(resolution,[],[f129172,f14342]) ).
fof(f129303,plain,
( ! [X0] :
( ~ s__subclass(X0,sK514)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_13 ),
inference(forward_subsumption_resolution,[],[f129302,f23081]) ).
fof(f129306,plain,
( ! [X0] :
( ~ s__subclass(X0,sK514)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_13 ),
inference(forward_subsumption_resolution,[],[f129303,f14341]) ).
fof(f129360,plain,
( ~ s__instance(s__Creature50_1,sK513)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_13 ),
inference(resolution,[],[f129306,f23036]) ).
fof(f129369,plain,
( ! [X0] :
( ~ s__subclass(X0,sK513)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK513,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_13 ),
inference(resolution,[],[f129360,f14342]) ).
fof(f129370,plain,
( ! [X0] :
( ~ s__subclass(X0,sK513)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_13
| ~ spl515_14 ),
inference(forward_subsumption_resolution,[],[f129369,f23086]) ).
fof(f129373,plain,
( ! [X0] :
( ~ s__subclass(X0,sK513)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_13
| ~ spl515_14 ),
inference(forward_subsumption_resolution,[],[f129370,f14341]) ).
fof(f129840,plain,
( ~ s__instance(s__Creature50_1,sK512)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_13
| ~ spl515_14 ),
inference(resolution,[],[f129373,f23041]) ).
fof(f129858,plain,
( ! [X0] :
( ~ s__subclass(X0,sK512)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK512,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_13
| ~ spl515_14 ),
inference(resolution,[],[f129840,f14342]) ).
fof(f129859,plain,
( ! [X0] :
( ~ s__subclass(X0,sK512)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15 ),
inference(forward_subsumption_resolution,[],[f129858,f23091]) ).
fof(f129862,plain,
( ! [X0] :
( ~ s__subclass(X0,sK512)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15 ),
inference(forward_subsumption_resolution,[],[f129859,f14341]) ).
fof(f130724,plain,
( ~ s__instance(s__Creature50_1,sK511)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15 ),
inference(resolution,[],[f129862,f23046]) ).
fof(f130734,plain,
( ! [X0] :
( ~ s__subclass(X0,sK511)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK511,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15 ),
inference(resolution,[],[f130724,f14342]) ).
fof(f130735,plain,
( ! [X0] :
( ~ s__subclass(X0,sK511)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16 ),
inference(forward_subsumption_resolution,[],[f130734,f23096]) ).
fof(f130738,plain,
( ! [X0] :
( ~ s__subclass(X0,sK511)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16 ),
inference(forward_subsumption_resolution,[],[f130735,f14341]) ).
fof(f131228,plain,
( ~ s__instance(s__Creature50_1,sK510)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16 ),
inference(resolution,[],[f130738,f23051]) ).
fof(f131243,plain,
( ! [X0] :
( ~ s__subclass(X0,sK510)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK510,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16 ),
inference(resolution,[],[f131228,f14342]) ).
fof(f131244,plain,
( ! [X0] :
( ~ s__subclass(X0,sK510)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17 ),
inference(forward_subsumption_resolution,[],[f131243,f23101]) ).
fof(f131247,plain,
( ! [X0] :
( ~ s__subclass(X0,sK510)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17 ),
inference(forward_subsumption_resolution,[],[f131244,f14341]) ).
fof(f133008,plain,
( ~ s__instance(s__Creature50_1,sK509)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17 ),
inference(resolution,[],[f131247,f23056]) ).
fof(f133035,plain,
( ! [X0] :
( ~ s__subclass(X0,sK509)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK509,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17 ),
inference(resolution,[],[f133008,f14342]) ).
fof(f133036,plain,
( ! [X0] :
( ~ s__subclass(X0,sK509)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18 ),
inference(forward_subsumption_resolution,[],[f133035,f23106]) ).
fof(f133039,plain,
( ! [X0] :
( ~ s__subclass(X0,sK509)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18 ),
inference(forward_subsumption_resolution,[],[f133036,f14341]) ).
fof(f135130,plain,
( ~ s__instance(s__Creature50_1,sK508)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18 ),
inference(resolution,[],[f133039,f23061]) ).
fof(f135146,plain,
( ! [X0] :
( ~ s__subclass(X0,sK508)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK508,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18 ),
inference(resolution,[],[f135130,f14342]) ).
fof(f135147,plain,
( ! [X0] :
( ~ s__subclass(X0,sK508)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19 ),
inference(forward_subsumption_resolution,[],[f135146,f23111]) ).
fof(f135150,plain,
( ! [X0] :
( ~ s__subclass(X0,sK508)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19 ),
inference(forward_subsumption_resolution,[],[f135147,f14341]) ).
fof(f144567,plain,
( ~ s__instance(s__Creature50_1,sK507)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19 ),
inference(resolution,[],[f135150,f23066]) ).
fof(f144573,plain,
( ! [X0] :
( ~ s__subclass(X0,sK507)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK507,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19 ),
inference(resolution,[],[f144567,f14342]) ).
fof(f144574,plain,
( ! [X0] :
( ~ s__subclass(X0,sK507)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20 ),
inference(forward_subsumption_resolution,[],[f144573,f23116]) ).
fof(f144577,plain,
( ! [X0] :
( ~ s__subclass(X0,sK507)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20 ),
inference(forward_subsumption_resolution,[],[f144574,f14341]) ).
fof(f144897,plain,
( ~ s__instance(s__Creature50_1,sK506)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_11
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20 ),
inference(resolution,[],[f144577,f23071]) ).
fof(f144913,plain,
( ! [X0] :
( ~ s__subclass(X0,sK506)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(sK506,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_11
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20 ),
inference(resolution,[],[f144897,f14342]) ).
fof(f144914,plain,
( ! [X0] :
( ~ s__subclass(X0,sK506)
| ~ s__instance(s__Creature50_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_11
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20
| ~ spl515_21 ),
inference(forward_subsumption_resolution,[],[f144913,f23121]) ).
fof(f144917,plain,
( ! [X0] :
( ~ s__subclass(X0,sK506)
| ~ s__instance(s__Creature50_1,X0) )
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_11
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20
| ~ spl515_21 ),
inference(forward_subsumption_resolution,[],[f144914,f14341]) ).
fof(f145729,plain,
( ~ s__instance(s__Creature50_1,sK505)
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_11
| ~ spl515_12
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20
| ~ spl515_21 ),
inference(resolution,[],[f144917,f23076]) ).
fof(f145730,plain,
( $false
| ~ spl515_2
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_11
| ~ spl515_12
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20
| ~ spl515_21 ),
inference(forward_subsumption_resolution,[],[f145729,f23026]) ).
fof(f145731,plain,
( ~ spl515_2
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_11
| ~ spl515_12
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20
| ~ spl515_21 ),
inference(avatar_contradiction_clause,[],[f145730]) ).
cnf(s1,plain,
( ~ spl515_1
| spl515_2 ),
inference(sat_conversion,[],[f23027]) ).
cnf(s2,plain,
( ~ spl515_1
| spl515_3 ),
inference(sat_conversion,[],[f23032]) ).
cnf(s3,plain,
( ~ spl515_1
| spl515_4 ),
inference(sat_conversion,[],[f23037]) ).
cnf(s4,plain,
( ~ spl515_1
| spl515_5 ),
inference(sat_conversion,[],[f23042]) ).
cnf(s5,plain,
( ~ spl515_1
| spl515_6 ),
inference(sat_conversion,[],[f23047]) ).
cnf(s6,plain,
( ~ spl515_1
| spl515_7 ),
inference(sat_conversion,[],[f23052]) ).
cnf(s7,plain,
( ~ spl515_1
| spl515_8 ),
inference(sat_conversion,[],[f23057]) ).
cnf(s8,plain,
( ~ spl515_1
| spl515_9 ),
inference(sat_conversion,[],[f23062]) ).
cnf(s9,plain,
( ~ spl515_1
| spl515_10 ),
inference(sat_conversion,[],[f23067]) ).
cnf(s10,plain,
( ~ spl515_1
| spl515_11 ),
inference(sat_conversion,[],[f23072]) ).
cnf(s11,plain,
( ~ spl515_1
| spl515_12 ),
inference(sat_conversion,[],[f23077]) ).
cnf(s12,plain,
( ~ spl515_1
| spl515_13 ),
inference(sat_conversion,[],[f23082]) ).
cnf(s13,plain,
( ~ spl515_1
| spl515_14 ),
inference(sat_conversion,[],[f23087]) ).
cnf(s14,plain,
( ~ spl515_1
| spl515_15 ),
inference(sat_conversion,[],[f23092]) ).
cnf(s15,plain,
( ~ spl515_1
| spl515_16 ),
inference(sat_conversion,[],[f23097]) ).
cnf(s16,plain,
( ~ spl515_1
| spl515_17 ),
inference(sat_conversion,[],[f23102]) ).
cnf(s17,plain,
( ~ spl515_1
| spl515_18 ),
inference(sat_conversion,[],[f23107]) ).
cnf(s18,plain,
( ~ spl515_1
| spl515_19 ),
inference(sat_conversion,[],[f23112]) ).
cnf(s19,plain,
( ~ spl515_1
| spl515_20 ),
inference(sat_conversion,[],[f23117]) ).
cnf(s20,plain,
( ~ spl515_1
| spl515_21 ),
inference(sat_conversion,[],[f23122]) ).
cnf(s22,plain,
( spl515_1
| ~ spl515_23 ),
inference(sat_conversion,[],[f23132]) ).
cnf(s223,plain,
spl515_186,
inference(sat_conversion,[],[f26877]) ).
cnf(s6418,plain,
spl515_643,
inference(sat_conversion,[],[f98114]) ).
cnf(s6544,plain,
( spl515_23
| ~ spl515_186
| ~ spl515_643 ),
inference(sat_conversion,[],[f129282]) ).
cnf(s6578,plain,
( ~ spl515_2
| ~ spl515_3
| ~ spl515_4
| ~ spl515_5
| ~ spl515_6
| ~ spl515_7
| ~ spl515_8
| ~ spl515_9
| ~ spl515_10
| ~ spl515_11
| ~ spl515_12
| ~ spl515_13
| ~ spl515_14
| ~ spl515_15
| ~ spl515_16
| ~ spl515_17
| ~ spl515_18
| ~ spl515_19
| ~ spl515_20
| ~ spl515_21 ),
inference(sat_conversion,[],[f145731]) ).
cnf(s6667,plain,
spl515_23,
inference(rat,[],[s6544,s6418,s223]) ).
cnf(s6742,plain,
spl515_1,
inference(rat,[],[s22,s6667]) ).
cnf(s6744,plain,
spl515_21,
inference(rat,[],[s20,s6742]) ).
cnf(s6745,plain,
spl515_20,
inference(rat,[],[s19,s6742]) ).
cnf(s6746,plain,
spl515_19,
inference(rat,[],[s18,s6742]) ).
cnf(s6747,plain,
spl515_18,
inference(rat,[],[s17,s6742]) ).
cnf(s6748,plain,
spl515_17,
inference(rat,[],[s16,s6742]) ).
cnf(s6749,plain,
spl515_16,
inference(rat,[],[s15,s6742]) ).
cnf(s6750,plain,
spl515_15,
inference(rat,[],[s14,s6742]) ).
cnf(s6751,plain,
spl515_14,
inference(rat,[],[s13,s6742]) ).
cnf(s6752,plain,
spl515_13,
inference(rat,[],[s12,s6742]) ).
cnf(s6753,plain,
spl515_12,
inference(rat,[],[s11,s6742]) ).
cnf(s6754,plain,
spl515_11,
inference(rat,[],[s10,s6742]) ).
cnf(s6755,plain,
spl515_10,
inference(rat,[],[s9,s6742]) ).
cnf(s6756,plain,
spl515_9,
inference(rat,[],[s8,s6742]) ).
cnf(s6757,plain,
spl515_8,
inference(rat,[],[s7,s6742]) ).
cnf(s6758,plain,
spl515_7,
inference(rat,[],[s6,s6742]) ).
cnf(s6759,plain,
spl515_6,
inference(rat,[],[s5,s6742]) ).
cnf(s6760,plain,
spl515_5,
inference(rat,[],[s4,s6742]) ).
cnf(s6761,plain,
spl515_4,
inference(rat,[],[s3,s6742]) ).
cnf(s6762,plain,
spl515_3,
inference(rat,[],[s2,s6742]) ).
cnf(s6763,plain,
~ spl515_2,
inference(rat,[],[s6578,s6744,s6745,s6746,s6747,s6748,s6749,s6750,s6751,s6752,s6753,s6754,s6755,s6756,s6757,s6758,s6759,s6760,s6761,s6762]) ).
cnf(s6765,plain,
$false,
inference(rat,[],[s1,s6763,s6742]) ).
fof(f145735,plain,
$false,
inference(avatar_sat_refutation,[],[s6765]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+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.08/0.20 % Computer : n004.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 23:00:37 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.10/1.69 % (875085)Will run a generic schedule for satisfiability detection.
% 7.10/1.69 % (875094)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4289997558:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 7.10/1.69 % (875091)% WARNING: option uhcvi not known.
% 7.10/1.69 % (875090)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2566078897_2998 on theBenchmark for (2998ds/0Mi)
% 7.10/1.69 % (875091)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1447662267:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 7.10/1.69 % (875092)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2748751394:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 7.10/1.69 % (875093)dis+10_1_sil=32000:sp=arity:random_seed=1518508213:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 7.10/1.69 % (875096)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=519840598:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 7.10/1.69 % (875095)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4158408869:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 7.10/1.69 % (875094)Instruction limit reached!
% 7.10/1.69 % (875094)------------------------------
% 7.10/1.69 % (875094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.69 % (875094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.69 % (875094)CaDiCaL version: 2.1.3
% 7.10/1.69 % (875094)Termination reason: Instruction limit
% 7.10/1.69 % (875094)Termination phase: Property scanning
% 7.10/1.69 % (875094)Time elapsed: 0.045 s
% 7.10/1.69 % (875094)Peak memory usage: 26 MB
% 7.10/1.69 % (875094)Instructions burned: 116 (million)
% 7.10/1.69 % (875104)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=482676646:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 7.10/1.69 % (875093)Instruction limit reached!
% 7.10/1.69 % (875093)------------------------------
% 7.10/1.69 % (875093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.69 % (875093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.69 % (875093)CaDiCaL version: 2.1.3
% 7.10/1.69 % (875093)Termination reason: Instruction limit
% 7.10/1.69 % (875093)Termination phase: Clausification
% 7.10/1.69 % (875093)Time elapsed: 0.066 s
% 7.10/1.69 % (875093)Peak memory usage: 24 MB
% 7.10/1.69 % (875093)Instructions burned: 104 (million)
% 7.10/1.69 % (875095)Instruction limit reached!
% 7.10/1.69 % (875095)------------------------------
% 7.10/1.69 % (875095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.69 % (875095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.69 % (875095)CaDiCaL version: 2.1.3
% 7.10/1.69 % (875095)Termination reason: Instruction limit
% 7.10/1.69 % (875095)Termination phase: Property scanning
% 7.10/1.69 % (875095)Time elapsed: 0.082 s
% 7.10/1.69 % (875095)Peak memory usage: 24 MB
% 7.10/1.69 % (875095)Instructions burned: 133 (million)
% 7.10/1.69 % (875106)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3498522856:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 7.10/1.69 % (875096)Instruction limit reached!
% 7.10/1.69 % (875096)------------------------------
% 7.10/1.69 % (875096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.69 % (875096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.69 % (875096)CaDiCaL version: 2.1.3
% 7.10/1.69 % (875096)Termination reason: Instruction limit
% 7.10/1.69 % (875096)Termination phase: Property scanning
% 7.10/1.69 % (875096)Time elapsed: 0.091 s
% 7.10/1.69 % (875096)Peak memory usage: 25 MB
% 7.10/1.69 % (875096)Instructions burned: 159 (million)
% 7.10/1.69 % (875107)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=2570977556:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 7.10/1.69 % (875109)ott-21_1_sil=16000:fs=off:random_seed=681733697:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 7.10/1.69 % (875106)Instruction limit reached!
% 7.10/1.69 % (875106)------------------------------
% 7.10/1.69 % (875106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.69 % (875106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.69 % (875106)CaDiCaL version: 2.1.3
% 7.10/1.69 % (875106)Termination reason: Instruction limit
% 15.37/2.76 % (875106)Termination phase: Property scanning
% 15.37/2.76 % (875106)Time elapsed: 0.081 s
% 15.37/2.76 % (875106)Peak memory usage: 25 MB
% 15.37/2.76 % (875106)Instructions burned: 132 (million)
% 15.37/2.76 % (875112)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1909224623:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 15.37/2.76 % (875109)Instruction limit reached!
% 15.37/2.76 % (875109)------------------------------
% 15.37/2.76 % (875109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.76 % (875109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.76 % (875109)CaDiCaL version: 2.1.3
% 15.37/2.76 % (875109)Termination reason: Instruction limit
% 15.37/2.76 % (875109)Termination phase: Property scanning
% 15.37/2.76 % (875109)Time elapsed: 0.098 s
% 15.37/2.76 % (875109)Peak memory usage: 25 MB
% 15.37/2.76 % (875109)Instructions burned: 182 (million)
% 15.37/2.76 % (875114)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=954354734:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 15.37/2.76 % (875104)Instruction limit reached!
% 15.37/2.76 % (875104)------------------------------
% 15.37/2.76 % (875104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.76 % (875104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.76 % (875104)CaDiCaL version: 2.1.3
% 15.37/2.76 % (875104)Termination reason: Instruction limit
% 15.37/2.76 % (875104)Termination phase: Finite model building preprocessing
% 15.37/2.76 % (875104)Time elapsed: 0.191 s
% 15.37/2.76 % (875104)Peak memory usage: 36 MB
% 15.37/2.76 % (875104)Instructions burned: 719 (million)
% 15.37/2.76 % (875116)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4059934728:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 15.37/2.76 % (875112)Instruction limit reached!
% 15.37/2.76 % (875112)------------------------------
% 15.37/2.76 % (875112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.76 % (875112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.76 % (875112)CaDiCaL version: 2.1.3
% 15.37/2.76 % (875112)Termination reason: Instruction limit
% 15.37/2.76 % (875112)Termination phase: Saturation
% 15.37/2.76 % (875112)Time elapsed: 0.251 s
% 15.37/2.76 % (875112)Peak memory usage: 30 MB
% 15.37/2.76 % (875112)Instructions burned: 477 (million)
% 15.37/2.76 % (875107)Instruction limit reached!
% 15.37/2.76 % (875107)------------------------------
% 15.37/2.76 % (875107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.76 % (875118)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4278541011:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 15.37/2.76 % (875107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.76 % (875107)CaDiCaL version: 2.1.3
% 15.37/2.76 % (875107)Termination reason: Instruction limit
% 15.37/2.76 % (875107)Termination phase: Saturation
% 15.37/2.76 % (875107)Time elapsed: 0.361 s
% 15.37/2.76 % (875107)Peak memory usage: 34 MB
% 15.37/2.76 % (875107)Instructions burned: 685 (million)
% 15.37/2.76 % (875120)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=3692790720:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 15.37/2.76 % (875116)Instruction limit reached!
% 15.37/2.76 % (875116)------------------------------
% 15.37/2.76 % (875116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.76 % (875116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.76 % (875116)CaDiCaL version: 2.1.3
% 15.37/2.76 % (875116)Termination reason: Instruction limit
% 15.37/2.76 % (875116)Termination phase: Saturation
% 15.37/2.76 % (875116)Time elapsed: 0.325 s
% 15.37/2.76 % (875116)Peak memory usage: 37 MB
% 15.37/2.76 % (875116)Instructions burned: 1181 (million)
% 15.37/2.76 % (875122)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=180496610:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 15.37/2.76 % (875114)Instruction limit reached!
% 15.37/2.76 % (875114)------------------------------
% 15.37/2.76 % (875114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/2.76 % (875114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/2.76 % (875114)CaDiCaL version: 2.1.3
% 15.37/2.76 % (875114)Termination reason: Instruction limit
% 15.37/2.76 % (875114)Termination phase: Finite model building preprocessing
% 26.78/4.26 % (875114)Time elapsed: 0.416 s
% 26.78/4.26 % (875114)Peak memory usage: 39 MB
% 26.78/4.26 % (875114)Instructions burned: 866 (million)
% 26.78/4.26 % (875124)fmb+10_1_sil=64000:random_seed=1123552558:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 26.78/4.26 % Detected minimum model sizes of [51]
% 26.78/4.26 % Detected maximum model sizes of [max]
% 26.78/4.26 % (875090)Cannot represent all propositional literals internally
% 26.78/4.26 % (875090)Refutation not found, incomplete strategy
% 26.78/4.26 % (875090)------------------------------
% 26.78/4.26 % (875090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.78/4.26 % (875090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.26 % (875090)CaDiCaL version: 2.1.3
% 26.78/4.26 % (875090)Termination reason: Refutation not found, incomplete strategy
% 26.78/4.26 % (875090)Time elapsed: 0.712 s
% 26.78/4.26 % (875090)Peak memory usage: 49 MB
% 26.78/4.26 % (875090)Instructions burned: 1474 (million)
% 26.78/4.26 % (875090)------------------------------
% 26.78/4.26 % (875090)------------------------------
% 26.78/4.26 % (875126)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=379936446:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 26.78/4.26 % (875122)Instruction limit reached!
% 26.78/4.26 % (875122)------------------------------
% 26.78/4.26 % (875122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.78/4.26 % (875122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.26 % (875122)CaDiCaL version: 2.1.3
% 26.78/4.26 % (875122)Termination reason: Instruction limit
% 26.78/4.26 % (875122)Termination phase: Saturation
% 26.78/4.26 % (875122)Time elapsed: 0.228 s
% 26.78/4.26 % (875122)Peak memory usage: 37 MB
% 26.78/4.26 % (875122)Instructions burned: 881 (million)
% 26.78/4.26 % (875128)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=23575502:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 26.78/4.26 % (875120)Instruction limit reached!
% 26.78/4.26 % (875120)------------------------------
% 26.78/4.26 % (875120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.78/4.26 % (875120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.26 % (875120)CaDiCaL version: 2.1.3
% 26.78/4.26 % (875120)Termination reason: Instruction limit
% 26.78/4.26 % (875120)Termination phase: Saturation
% 26.78/4.26 % (875120)Time elapsed: 0.382 s
% 26.78/4.26 % (875120)Peak memory usage: 36 MB
% 26.78/4.26 % (875120)Instructions burned: 693 (million)
% 26.78/4.26 % (875118)Instruction limit reached!
% 26.78/4.26 % (875118)------------------------------
% 26.78/4.26 % (875118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.78/4.26 % (875118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.26 % (875118)CaDiCaL version: 2.1.3
% 26.78/4.26 % (875118)Termination reason: Instruction limit
% 26.78/4.26 % (875118)Termination phase: Finite model building preprocessing
% 26.78/4.26 % (875118)Time elapsed: 0.426 s
% 26.78/4.26 % (875118)Peak memory usage: 40 MB
% 26.78/4.26 % (875118)Instructions burned: 889 (million)
% 26.78/4.26 % (875130)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3771580898:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 26.78/4.26 % (875132)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=745527239:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 26.78/4.26 % (875128)Instruction limit reached!
% 26.78/4.26 % (875128)------------------------------
% 26.78/4.26 % (875128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.78/4.26 % (875128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.26 % (875128)CaDiCaL version: 2.1.3
% 26.78/4.26 % (875128)Termination reason: Instruction limit
% 26.78/4.26 % (875128)Termination phase: Finite model building preprocessing
% 26.78/4.26 % (875128)Time elapsed: 0.240 s
% 26.78/4.26 % (875128)Peak memory usage: 39 MB
% 26.78/4.26 % (875128)Instructions burned: 924 (million)
% 26.78/4.26 % (875134)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3129206319:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 26.78/4.26 % Detected minimum model sizes of [51]
% 26.78/4.26 % Detected maximum model sizes of [max]
% 26.78/4.26 % (875124)Cannot represent all propositional literals internally
% 26.78/4.26 % (875124)Refutation not found, incomplete strategy
% 26.78/4.26 % (875124)------------------------------
% 26.78/4.26 % (875124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.71/5.59 % (875124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.71/5.59 % (875124)CaDiCaL version: 2.1.3
% 35.71/5.59 % (875124)Termination reason: Refutation not found, incomplete strategy
% 35.71/5.59 % (875124)Time elapsed: 0.553 s
% 35.71/5.59 % (875124)Peak memory usage: 43 MB
% 35.71/5.59 % (875124)Instructions burned: 1182 (million)
% 35.71/5.59 % (875124)------------------------------
% 35.71/5.59 % (875124)------------------------------
% 35.71/5.59 % (875136)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1337182328:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi)
% 35.71/5.59 % Detected minimum model sizes of [51]
% 35.71/5.59 % Detected maximum model sizes of [max]
% 35.71/5.59 % (875126)Cannot represent all propositional literals internally
% 35.71/5.59 % (875126)Refutation not found, incomplete strategy
% 35.71/5.59 % (875126)------------------------------
% 35.71/5.59 % (875126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.71/5.59 % (875126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.71/5.59 % (875126)CaDiCaL version: 2.1.3
% 35.71/5.59 % (875126)Termination reason: Refutation not found, incomplete strategy
% 35.71/5.59 % (875126)Time elapsed: 0.585 s
% 35.71/5.59 % (875126)Peak memory usage: 44 MB
% 35.71/5.59 % (875126)Instructions burned: 1257 (million)
% 35.71/5.59 % (875126)------------------------------
% 35.71/5.59 % (875126)------------------------------
% 35.71/5.59 % (875138)ott-2_1_sil=16000:newcnf=on:random_seed=2797214535:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2984 on theBenchmark for (2984ds/869Mi)
% 35.71/5.59 % Detected minimum model sizes of [51]
% 35.71/5.59 % Detected maximum model sizes of [max]
% 35.71/5.59 % (875134)Cannot represent all propositional literals internally
% 35.71/5.59 % (875134)Refutation not found, incomplete strategy
% 35.71/5.59 % (875134)------------------------------
% 35.71/5.59 % (875134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.71/5.59 % (875134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.71/5.59 % (875134)CaDiCaL version: 2.1.3
% 35.71/5.59 % (875134)Termination reason: Refutation not found, incomplete strategy
% 35.71/5.59 % (875134)Time elapsed: 0.382 s
% 35.71/5.59 % (875134)Peak memory usage: 48 MB
% 35.71/5.59 % (875134)Instructions burned: 1458 (million)
% 35.71/5.59 % (875134)------------------------------
% 35.71/5.59 % (875134)------------------------------
% 35.71/5.59 % (875140)ott+10_1_sil=32000:tgt=ground:random_seed=3126009465:i=5114:av=off_2982 on theBenchmark for (2982ds/5114Mi)
% 35.71/5.59 % (875132)Instruction limit reached!
% 35.71/5.59 % (875132)------------------------------
% 35.71/5.59 % (875132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.71/5.59 % (875132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.71/5.59 % (875132)CaDiCaL version: 2.1.3
% 35.71/5.59 % (875132)Termination reason: Instruction limit
% 35.71/5.59 % (875132)Termination phase: Saturation
% 35.71/5.59 % (875132)Time elapsed: 0.759 s
% 35.71/5.59 % (875132)Peak memory usage: 45 MB
% 35.71/5.59 % (875132)Instructions burned: 1473 (million)
% 35.71/5.59 % (875142)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3060737151:i=54282_2980 on theBenchmark for (2980ds/54282Mi)
% 35.71/5.59 % (875138)Instruction limit reached!
% 35.71/5.59 % (875138)------------------------------
% 35.71/5.59 % (875138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.71/5.59 % (875138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.71/5.59 % (875138)CaDiCaL version: 2.1.3
% 35.71/5.59 % (875138)Termination reason: Instruction limit
% 35.71/5.59 % (875138)Termination phase: Saturation
% 35.71/5.59 % (875138)Time elapsed: 0.454 s
% 35.71/5.59 % (875138)Peak memory usage: 38 MB
% 35.71/5.59 % (875138)Instructions burned: 870 (million)
% 35.71/5.59 % (875144)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=665062469:i=3512:aac=none_2979 on theBenchmark for (2979ds/3512Mi)
% 35.71/5.59 % (875136)Instruction limit reached!
% 35.71/5.59 % (875136)------------------------------
% 35.71/5.59 % (875136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.71/5.59 % (875136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.71/5.59 % (875136)CaDiCaL version: 2.1.3
% 35.71/5.59 % (875136)Termination reason: Instruction limit
% 35.71/5.59 % (875136)Termination phase: Finite model building preprocessing
% 35.71/5.59 % (875136)Time elapsed: 1.037 s
% 35.71/5.59 % (875136)Peak memory usage: 62 MB
% 90.50/16.46 % (875136)Instructions burned: 2174 (million)
% 90.50/16.46 % (875146)dis+21_1_sil=32000:sas=cadical:random_seed=1194486372:i=3773:amm=off_2974 on theBenchmark for (2974ds/3773Mi)
% 90.50/16.46 % Detected minimum model sizes of [51]
% 90.50/16.46 % Detected maximum model sizes of [max]
% 90.50/16.46 % (875142)Cannot represent all propositional literals internally
% 90.50/16.46 % (875142)Refutation not found, incomplete strategy
% 90.50/16.46 % (875142)------------------------------
% 90.50/16.46 % (875142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875142)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875142)Termination reason: Refutation not found, incomplete strategy
% 90.50/16.46 % (875142)Time elapsed: 0.701 s
% 90.50/16.46 % (875142)Peak memory usage: 49 MB
% 90.50/16.46 % (875142)Instructions burned: 1470 (million)
% 90.50/16.46 % (875142)------------------------------
% 90.50/16.46 % (875142)------------------------------
% 90.50/16.46 % (875148)ott+11_1_sil=16000:gs=on:random_seed=3042805063:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2973 on theBenchmark for (2973ds/2251Mi)
% 90.50/16.46 % (875140)Instruction limit reached!
% 90.50/16.46 % (875140)------------------------------
% 90.50/16.46 % (875140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875140)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875140)Termination reason: Instruction limit
% 90.50/16.46 % (875140)Termination phase: Saturation
% 90.50/16.46 % (875140)Time elapsed: 1.395 s
% 90.50/16.46 % (875140)Peak memory usage: 64 MB
% 90.50/16.46 % (875140)Instructions burned: 5117 (million)
% 90.50/16.46 % (875150)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3928775414:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi)
% 90.50/16.46 % Detected minimum model sizes of [51]
% 90.50/16.46 % Detected maximum model sizes of [max]
% 90.50/16.46 % (875150)Cannot represent all propositional literals internally
% 90.50/16.46 % (875150)Refutation not found, incomplete strategy
% 90.50/16.46 % (875150)------------------------------
% 90.50/16.46 % (875150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875150)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875150)Termination reason: Refutation not found, incomplete strategy
% 90.50/16.46 % (875150)Time elapsed: 0.359 s
% 90.50/16.46 % (875150)Peak memory usage: 45 MB
% 90.50/16.46 % (875150)Instructions burned: 1419 (million)
% 90.50/16.46 % (875150)------------------------------
% 90.50/16.46 % (875150)------------------------------
% 90.50/16.46 % (875152)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2211697191:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2965 on theBenchmark for (2965ds/4591Mi)
% 90.50/16.46 % (875144)Instruction limit reached!
% 90.50/16.46 % (875144)------------------------------
% 90.50/16.46 % (875144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875144)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875144)Termination reason: Instruction limit
% 90.50/16.46 % (875144)Termination phase: Saturation
% 90.50/16.46 % (875144)Time elapsed: 1.558 s
% 90.50/16.46 % (875144)Peak memory usage: 66 MB
% 90.50/16.46 % (875144)Instructions burned: 3513 (million)
% 90.50/16.46 % (875154)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2791583447:i=29340_2963 on theBenchmark for (2963ds/29340Mi)
% 90.50/16.46 % (875130)Instruction limit reached!
% 90.50/16.46 % (875130)------------------------------
% 90.50/16.46 % (875130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875130)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875130)Termination reason: Instruction limit
% 90.50/16.46 % (875130)Termination phase: Saturation
% 90.50/16.46 % (875130)Time elapsed: 2.644 s
% 90.50/16.46 % (875130)Peak memory usage: 57 MB
% 90.50/16.46 % (875130)Instructions burned: 5132 (million)
% 90.50/16.46 % (875156)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2774676166:i=5211_2962 on theBenchmark for (2962ds/5211Mi)
% 90.50/16.46 % (875148)Instruction limit reached!
% 90.50/16.46 % (875148)------------------------------
% 90.50/16.46 % (875148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875148)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875148)Termination reason: Instruction limit
% 90.50/16.46 % (875148)Termination phase: Saturation
% 90.50/16.46 % (875148)Time elapsed: 1.365 s
% 90.50/16.46 % (875148)Peak memory usage: 82 MB
% 90.50/16.46 % (875148)Instructions burned: 2252 (million)
% 90.50/16.46 % (875158)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1554957324:i=5497:nm=2_2959 on theBenchmark for (2959ds/5497Mi)
% 90.50/16.46 % (875146)Instruction limit reached!
% 90.50/16.46 % (875146)------------------------------
% 90.50/16.46 % (875146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875146)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875146)Termination reason: Instruction limit
% 90.50/16.46 % (875146)Termination phase: Saturation
% 90.50/16.46 % (875146)Time elapsed: 1.831 s
% 90.50/16.46 % (875146)Peak memory usage: 62 MB
% 90.50/16.46 % (875146)Instructions burned: 3773 (million)
% 90.50/16.46 % (875160)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1589297699:fmbsr=2:i=46332_2956 on theBenchmark for (2956ds/46332Mi)
% 90.50/16.46 % Detected minimum model sizes of [51]
% 90.50/16.46 % Detected maximum model sizes of [max]
% 90.50/16.46 % (875158)Cannot represent all propositional literals internally
% 90.50/16.46 % (875158)Refutation not found, incomplete strategy
% 90.50/16.46 % (875158)------------------------------
% 90.50/16.46 % (875158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875158)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875158)Termination reason: Refutation not found, incomplete strategy
% 90.50/16.46 % (875158)Time elapsed: 0.641 s
% 90.50/16.46 % (875158)Peak memory usage: 45 MB
% 90.50/16.46 % (875158)Instructions burned: 1328 (million)
% 90.50/16.46 % (875158)------------------------------
% 90.50/16.46 % (875158)------------------------------
% 90.50/16.46 % (875162)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2134337223:i=14071_2952 on theBenchmark for (2952ds/14071Mi)
% 90.50/16.46 % (875152)Instruction limit reached!
% 90.50/16.46 % (875152)------------------------------
% 90.50/16.46 % (875152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875152)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875152)Termination reason: Instruction limit
% 90.50/16.46 % (875152)Termination phase: Saturation
% 90.50/16.46 % (875152)Time elapsed: 1.429 s
% 90.50/16.46 % (875152)Peak memory usage: 95 MB
% 90.50/16.46 % (875152)Instructions burned: 4593 (million)
% 90.50/16.46 % (875164)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1732494865:i=22565:add=on:rawr=on_2950 on theBenchmark for (2950ds/22565Mi)
% 90.50/16.46 % Detected minimum model sizes of [51]
% 90.50/16.46 % Detected maximum model sizes of [max]
% 90.50/16.46 % (875160)Cannot represent all propositional literals internally
% 90.50/16.46 % (875160)Refutation not found, incomplete strategy
% 90.50/16.46 % (875160)------------------------------
% 90.50/16.46 % (875160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875160)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875160)Termination reason: Refutation not found, incomplete strategy
% 90.50/16.46 % (875160)Time elapsed: 0.648 s
% 90.50/16.46 % (875160)Peak memory usage: 45 MB
% 90.50/16.46 % (875160)Instructions burned: 1419 (million)
% 90.50/16.46 % (875160)------------------------------
% 90.50/16.46 % (875160)------------------------------
% 90.50/16.46 % (875166)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2498194776:i=8173:av=off_2949 on theBenchmark for (2949ds/8173Mi)
% 90.50/16.46 % Detected minimum model sizes of [51]
% 90.50/16.46 % Detected maximum model sizes of [max]
% 90.50/16.46 % (875162)Cannot represent all propositional literals internally
% 90.50/16.46 % (875162)Refutation not found, incomplete strategy
% 90.50/16.46 % (875162)------------------------------
% 90.50/16.46 % (875162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875162)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875162)Termination reason: Refutation not found, incomplete strategy
% 90.50/16.46 % (875162)Time elapsed: 0.615 s
% 90.50/16.46 % (875162)Peak memory usage: 45 MB
% 90.50/16.46 % (875162)Instructions burned: 1286 (million)
% 90.50/16.46 % (875162)------------------------------
% 90.50/16.46 % (875162)------------------------------
% 90.50/16.46 % (875168)dis+10_16:1_sil=16000:random_seed=1626735836:i=9155:fsr=off_2946 on theBenchmark for (2946ds/9155Mi)
% 90.50/16.46 % (875156)Instruction limit reached!
% 90.50/16.46 % (875156)------------------------------
% 90.50/16.46 % (875156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875156)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875156)Termination reason: Instruction limit
% 90.50/16.46 % (875156)Termination phase: Saturation
% 90.50/16.46 % (875156)Time elapsed: 2.012 s
% 90.50/16.46 % (875156)Peak memory usage: 47 MB
% 90.50/16.46 % (875156)Instructions burned: 5212 (million)
% 90.50/16.46 % (875170)ott-3_8_sil=64000:random_seed=1142814979:i=20139:bs=on_2941 on theBenchmark for (2941ds/20139Mi)
% 90.50/16.46 % (875166)Instruction limit reached!
% 90.50/16.46 % (875166)------------------------------
% 90.50/16.46 % (875166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875166)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875166)Termination reason: Instruction limit
% 90.50/16.46 % (875166)Termination phase: Saturation
% 90.50/16.46 % (875166)Time elapsed: 4.386 s
% 90.50/16.46 % (875166)Peak memory usage: 110 MB
% 90.50/16.46 % (875166)Instructions burned: 8174 (million)
% 90.50/16.46 % (875168)Instruction limit reached!
% 90.50/16.46 % (875168)------------------------------
% 90.50/16.46 % (875168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875168)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875168)Termination reason: Instruction limit
% 90.50/16.46 % (875168)Termination phase: Saturation
% 90.50/16.46 % (875168)Time elapsed: 4.124 s
% 90.50/16.46 % (875168)Peak memory usage: 92 MB
% 90.50/16.46 % (875168)Instructions burned: 9156 (million)
% 90.50/16.46 % (875172)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2218927241:fmbsr=2:i=32576_2905 on theBenchmark for (2905ds/32576Mi)
% 90.50/16.46 % (875174)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2560748022:i=11404_2904 on theBenchmark for (2904ds/11404Mi)
% 90.50/16.46 % Detected minimum model sizes of [51]
% 90.50/16.46 % Detected maximum model sizes of [max]
% 90.50/16.46 % (875172)Cannot represent all propositional literals internally
% 90.50/16.46 % (875172)Refutation not found, incomplete strategy
% 90.50/16.46 % (875172)------------------------------
% 90.50/16.46 % (875172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875172)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875172)Termination reason: Refutation not found, incomplete strategy
% 90.50/16.46 % (875172)Time elapsed: 0.770 s
% 90.50/16.46 % (875172)Peak memory usage: 48 MB
% 90.50/16.46 % (875172)Instructions burned: 1458 (million)
% 90.50/16.46 % (875172)------------------------------
% 90.50/16.46 % (875172)------------------------------
% 90.50/16.46 % (875176)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1763903987:i=14134_2897 on theBenchmark for (2897ds/14134Mi)
% 90.50/16.46 % (875164)Instruction limit reached!
% 90.50/16.46 % (875164)------------------------------
% 90.50/16.46 % (875164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.46 % (875164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.46 % (875164)CaDiCaL version: 2.1.3
% 90.50/16.46 % (875164)Termination reason: Instruction limit
% 90.50/16.46 % (875164)Termination phase: Saturation
% 90.50/16.46 % (875164)Time elapsed: 7.528 s
% 90.50/16.46 % (875164)Peak memory usage: 800 MB
% 90.50/16.46 % (875164)Instructions burned: 22568 (million)
% 90.50/16.46 % (875178)dis+33_16_sil=32000:sac=on:random_seed=4287383765:i=15851:nm=0_2874 on theBenchmark for (2874ds/15851Mi)
% 90.50/16.46 % (875176) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-875085-875176"...
% 90.50/16.46 % (875176)...printing done.
% 90.50/16.46 % (875176)Refutation found. Thanks to Tanya!
% 90.50/16.46 % SZS status Theorem for theBenchmark
% 90.50/16.46 % SZS output start Proof for theBenchmark
% See solution above
% 90.50/16.47 % (875176)------------------------------
% 90.50/16.47 % (875176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 90.50/16.47 % (875176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.50/16.47 % (875176)CaDiCaL version: 2.1.3
% 90.50/16.47 % (875176)Termination reason: Refutation
% 90.50/16.47 % (875176)Time elapsed: 5.740 s
% 90.50/16.47 % (875176)Peak memory usage: 99 MB
% 90.50/16.47 % (875176)Instructions burned: 9991 (million)
% 90.50/16.47 % (875085)Success in time 16.218 s
% 90.50/16.47 % Vampire exiting
%------------------------------------------------------------------------------