%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR092+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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 66.30s 23.65s
% Output : Refutation 66.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 21
% Syntax : Number of formulae : 137 ( 33 unt; 4 def)
% Number of atoms : 372 ( 4 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 456 ( 221 ~; 216 |; 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/sandbox/benchmark/Axioms/CSR003+1.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/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_27) ).
fof(f93,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__parent(X0,X1)
=> s__ancestor(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_93) ).
fof(f226,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__son(X0,X1)
=> s__parent(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_226) ).
fof(f7100,axiom,
s__subclass(s__Animal,s__Organism),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7174) ).
fof(f7117,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7191) ).
fof(f7150,axiom,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7224) ).
fof(f7166,axiom,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7240) ).
fof(f7193,axiom,
s__subclass(s__Primate,s__Mammal),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7267) ).
fof(f7203,axiom,
s__subclass(s__Hominid,s__Primate),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7277) ).
fof(f7206,axiom,
s__subclass(s__Human,s__Hominid),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7280) ).
fof(f7211,axiom,
s__subclass(s__Man,s__Human),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7285) ).
fof(f7215,axiom,
s__subclass(s__Woman,s__Human),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7289) ).
fof(f16749,axiom,
s__instance(s__Man22_1,s__Man),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f16750,axiom,
s__instance(s__Ancestor22_1,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f16751,axiom,
s__son(s__Man22_1,s__Ancestor22_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f16752,conjecture,
? [X0] :
( s__ancestor(s__Man22_1,X0)
& X0 = s__Ancestor22_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f16753,negated_conjecture,
~ ? [X0] :
( s__ancestor(s__Man22_1,X0)
& X0 = s__Ancestor22_1 ),
inference(negated_conjecture,[status(cth)],[f16752]) ).
fof(f17020,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f17021,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(f17022,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,[],[f17021]) ).
fof(f17133,plain,
! [X0,X1] :
( s__ancestor(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f93]) ).
fof(f17134,plain,
! [X0,X1] :
( s__ancestor(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f17133]) ).
fof(f17392,plain,
! [X0,X1] :
( s__parent(X0,X1)
| ~ s__son(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f226]) ).
fof(f17393,plain,
! [X0,X1] :
( s__parent(X0,X1)
| ~ s__son(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f17392]) ).
fof(f27121,plain,
! [X0] :
( ~ s__ancestor(s__Man22_1,X0)
| s__Ancestor22_1 != X0 ),
inference(ennf_transformation,[],[f16753]) ).
fof(f28681,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f17020]) ).
fof(f28682,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f17020]) ).
fof(f28683,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,[],[f17022]) ).
fof(f28749,plain,
! [X0,X1] :
( s__ancestor(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f17134]) ).
fof(f28879,plain,
! [X0,X1] :
( ~ s__son(X0,X1)
| s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f17393]) ).
fof(f36588,plain,
s__subclass(s__Animal,s__Organism),
inference(cnf_transformation,[],[f7100]) ).
fof(f36610,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[],[f7117]) ).
fof(f36643,plain,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f7150]) ).
fof(f36661,plain,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
inference(cnf_transformation,[],[f7166]) ).
fof(f36688,plain,
s__subclass(s__Primate,s__Mammal),
inference(cnf_transformation,[],[f7193]) ).
fof(f36698,plain,
s__subclass(s__Hominid,s__Primate),
inference(cnf_transformation,[],[f7203]) ).
fof(f36701,plain,
s__subclass(s__Human,s__Hominid),
inference(cnf_transformation,[],[f7206]) ).
fof(f36706,plain,
s__subclass(s__Man,s__Human),
inference(cnf_transformation,[],[f7211]) ).
fof(f36710,plain,
s__subclass(s__Woman,s__Human),
inference(cnf_transformation,[],[f7215]) ).
fof(f48578,plain,
s__instance(s__Man22_1,s__Man),
inference(cnf_transformation,[],[f16749]) ).
fof(f48579,plain,
s__instance(s__Ancestor22_1,s__Human),
inference(cnf_transformation,[],[f16750]) ).
fof(f48580,plain,
s__son(s__Man22_1,s__Ancestor22_1),
inference(cnf_transformation,[],[f16751]) ).
fof(f48581,plain,
! [X0] :
( ~ s__ancestor(s__Man22_1,X0)
| s__Ancestor22_1 != X0 ),
inference(cnf_transformation,[],[f27121]) ).
fof(f48996,plain,
~ s__ancestor(s__Man22_1,s__Ancestor22_1),
inference(equality_resolution,[],[f48581]) ).
fof(f56748,definition,
( spl1514_312
<=> s__instance(s__Human,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl1514_312])],[avatar_definition]) ).
fof(f56749,plain,
( s__instance(s__Human,s__SetOrClass)
| ~ spl1514_312 ),
inference(avatar_component_clause,[],[f56748]) ).
fof(f56750,plain,
( ~ s__instance(s__Human,s__SetOrClass)
| spl1514_312 ),
inference(avatar_component_clause,[],[f56748]) ).
fof(f56757,plain,
( ! [X0] : ~ s__subclass(X0,s__Human)
| spl1514_312 ),
inference(resolution,[],[f56750,f28681]) ).
fof(f56766,plain,
( $false
| spl1514_312 ),
inference(resolution,[],[f56757,f36710]) ).
fof(f56775,plain,
spl1514_312,
inference(avatar_contradiction_clause,[],[f56766]) ).
fof(f249315,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,[],[f28749,f48996]) ).
fof(f249319,definition,
( spl1514_1645
<=> s__instance(s__Man22_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl1514_1645])],[avatar_definition]) ).
fof(f249321,plain,
( ~ s__instance(s__Man22_1,s__Organism)
| spl1514_1645 ),
inference(avatar_component_clause,[],[f249319]) ).
fof(f249323,definition,
( spl1514_1646
<=> s__instance(s__Ancestor22_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl1514_1646])],[avatar_definition]) ).
fof(f249325,plain,
( ~ s__instance(s__Ancestor22_1,s__Organism)
| spl1514_1646 ),
inference(avatar_component_clause,[],[f249323]) ).
fof(f249327,definition,
( spl1514_1647
<=> s__parent(s__Man22_1,s__Ancestor22_1) ),
introduced(definition,[new_symbols(definition,[spl1514_1647])],[avatar_definition]) ).
fof(f249329,plain,
( ~ s__parent(s__Man22_1,s__Ancestor22_1)
| spl1514_1647 ),
inference(avatar_component_clause,[],[f249327]) ).
fof(f249330,plain,
( ~ spl1514_1645
| ~ spl1514_1646
| ~ spl1514_1647 ),
inference(avatar_split_clause,[],[f249315,f249327,f249323,f249319]) ).
fof(f249524,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,[],[f28879,f48580]) ).
fof(f249525,plain,
( ~ s__instance(s__Ancestor22_1,s__Organism)
| ~ s__instance(s__Man22_1,s__Organism)
| spl1514_1647 ),
inference(forward_subsumption_resolution,[],[f249524,f249329]) ).
fof(f249526,plain,
( ~ spl1514_1645
| ~ spl1514_1646
| spl1514_1647 ),
inference(avatar_split_clause,[],[f249525,f249327,f249323,f249319]) ).
fof(f322671,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Organism,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(resolution,[],[f28683,f249321]) ).
fof(f322857,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f322671,f28681]) ).
fof(f323609,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Man22_1,X0) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f322857,f28682]) ).
fof(f324341,plain,
( ~ s__instance(s__Man22_1,s__Animal)
| spl1514_1645 ),
inference(resolution,[],[f323609,f36588]) ).
fof(f324348,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(resolution,[],[f324341,f28683]) ).
fof(f324349,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f324348,f28681]) ).
fof(f324350,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Man22_1,X0) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f324349,f28682]) ).
fof(f324362,plain,
( ~ s__instance(s__Man22_1,s__Vertebrate)
| spl1514_1645 ),
inference(resolution,[],[f324350,f36610]) ).
fof(f324365,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(resolution,[],[f324362,f28683]) ).
fof(f324366,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f324365,f28681]) ).
fof(f324367,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Man22_1,X0) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f324366,f28682]) ).
fof(f330333,plain,
( ~ s__instance(s__Man22_1,s__WarmBloodedVertebrate)
| spl1514_1645 ),
inference(resolution,[],[f324367,f36643]) ).
fof(f330345,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(resolution,[],[f330333,f28683]) ).
fof(f330346,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f330345,f28681]) ).
fof(f330347,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Man22_1,X0) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f330346,f28682]) ).
fof(f330560,plain,
( ~ s__instance(s__Man22_1,s__Mammal)
| spl1514_1645 ),
inference(resolution,[],[f330347,f36661]) ).
fof(f330564,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Mammal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(resolution,[],[f330560,f28683]) ).
fof(f330565,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f330564,f28681]) ).
fof(f330566,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Man22_1,X0) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f330565,f28682]) ).
fof(f331264,plain,
( ~ s__instance(s__Man22_1,s__Primate)
| spl1514_1645 ),
inference(resolution,[],[f330566,f36688]) ).
fof(f331321,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Primate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(resolution,[],[f331264,f28683]) ).
fof(f331322,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f331321,f28681]) ).
fof(f331323,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Man22_1,X0) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f331322,f28682]) ).
fof(f346189,plain,
( ~ s__instance(s__Man22_1,s__Hominid)
| spl1514_1645 ),
inference(resolution,[],[f331323,f36698]) ).
fof(f346215,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Hominid,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(resolution,[],[f346189,f28683]) ).
fof(f346216,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f346215,f28681]) ).
fof(f346217,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Man22_1,X0) )
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f346216,f28682]) ).
fof(f346714,plain,
( ~ s__instance(s__Man22_1,s__Human)
| spl1514_1645 ),
inference(resolution,[],[f346217,f36701]) ).
fof(f346717,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(s__Human,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1645 ),
inference(resolution,[],[f346714,f28683]) ).
fof(f346718,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Man22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl1514_312
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f346717,f56749]) ).
fof(f346719,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Man22_1,X0) )
| ~ spl1514_312
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f346718,f28682]) ).
fof(f347012,plain,
( ~ s__instance(s__Man22_1,s__Man)
| ~ spl1514_312
| spl1514_1645 ),
inference(resolution,[],[f346719,f36706]) ).
fof(f347016,plain,
( $false
| ~ spl1514_312
| spl1514_1645 ),
inference(forward_subsumption_resolution,[],[f347012,f48578]) ).
fof(f347017,plain,
( ~ spl1514_312
| spl1514_1645 ),
inference(avatar_contradiction_clause,[],[f347016]) ).
fof(f347022,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Organism,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(resolution,[],[f249325,f28683]) ).
fof(f347023,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f347022,f28681]) ).
fof(f347024,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f347023,f28682]) ).
fof(f347027,plain,
( ~ s__instance(s__Ancestor22_1,s__Animal)
| spl1514_1646 ),
inference(resolution,[],[f347024,f36588]) ).
fof(f347034,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(resolution,[],[f347027,f28683]) ).
fof(f347035,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f347034,f28681]) ).
fof(f347036,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f347035,f28682]) ).
fof(f347072,plain,
( ~ s__instance(s__Ancestor22_1,s__Vertebrate)
| spl1514_1646 ),
inference(resolution,[],[f347036,f36610]) ).
fof(f347079,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(resolution,[],[f347072,f28683]) ).
fof(f347080,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f347079,f28681]) ).
fof(f347081,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f347080,f28682]) ).
fof(f349834,plain,
( ~ s__instance(s__Ancestor22_1,s__WarmBloodedVertebrate)
| spl1514_1646 ),
inference(resolution,[],[f347081,f36643]) ).
fof(f349844,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(resolution,[],[f349834,f28683]) ).
fof(f349845,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f349844,f28681]) ).
fof(f349846,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f349845,f28682]) ).
fof(f349986,plain,
( ~ s__instance(s__Ancestor22_1,s__Mammal)
| spl1514_1646 ),
inference(resolution,[],[f349846,f36661]) ).
fof(f349998,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Mammal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(resolution,[],[f349986,f28683]) ).
fof(f349999,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f349998,f28681]) ).
fof(f350000,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f349999,f28682]) ).
fof(f350482,plain,
( ~ s__instance(s__Ancestor22_1,s__Primate)
| spl1514_1646 ),
inference(resolution,[],[f350000,f36688]) ).
fof(f350511,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Primate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(resolution,[],[f350482,f28683]) ).
fof(f350512,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f350511,f28681]) ).
fof(f350513,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f350512,f28682]) ).
fof(f350743,plain,
( ~ s__instance(s__Ancestor22_1,s__Hominid)
| spl1514_1646 ),
inference(resolution,[],[f350513,f36698]) ).
fof(f350754,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(s__Hominid,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(resolution,[],[f350743,f28683]) ).
fof(f350755,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Ancestor22_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f350754,f28681]) ).
fof(f350756,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Ancestor22_1,X0) )
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f350755,f28682]) ).
fof(f351104,plain,
( ~ s__instance(s__Ancestor22_1,s__Human)
| spl1514_1646 ),
inference(resolution,[],[f350756,f36701]) ).
fof(f351105,plain,
( $false
| spl1514_1646 ),
inference(forward_subsumption_resolution,[],[f351104,f48579]) ).
fof(f351106,plain,
spl1514_1646,
inference(avatar_contradiction_clause,[],[f351105]) ).
cnf(s419,plain,
spl1514_312,
inference(sat_conversion,[],[f56775]) ).
cnf(s56816,plain,
( ~ spl1514_1645
| ~ spl1514_1646
| ~ spl1514_1647 ),
inference(sat_conversion,[],[f249330]) ).
cnf(s56819,plain,
( ~ spl1514_1645
| ~ spl1514_1646
| spl1514_1647 ),
inference(sat_conversion,[],[f249526]) ).
cnf(s60587,plain,
( ~ spl1514_312
| spl1514_1645 ),
inference(sat_conversion,[],[f347017]) ).
cnf(s60588,plain,
spl1514_1646,
inference(sat_conversion,[],[f351106]) ).
cnf(s60612,plain,
( ~ spl1514_1645
| spl1514_1647 ),
inference(rat,[],[s56819,s60588]) ).
cnf(s60614,plain,
( ~ spl1514_1645
| ~ spl1514_1647 ),
inference(rat,[],[s56816,s60588]) ).
cnf(s60690,plain,
spl1514_1645,
inference(rat,[],[s60587,s419]) ).
cnf(s60691,plain,
spl1514_1647,
inference(rat,[],[s60612,s60690]) ).
cnf(s60692,plain,
$false,
inference(rat,[],[s60614,s60691,s60690]) ).
fof(f351107,plain,
$false,
inference(avatar_sat_refutation,[],[s60692]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR092+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n006.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 22:41:40 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.75/3.47 % (290935)Will run a generic schedule for satisfiability detection.
% 19.75/3.47 % (290941)% WARNING: option uhcvi not known.
% 19.75/3.47 % (290941)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4030922411:i=135531:add=off:rawr=on_2995 on theBenchmark for (2995ds/135531Mi)
% 19.75/3.47 % (290940)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2584107924_2995 on theBenchmark for (2995ds/0Mi)
% 19.75/3.47 % (290942)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3335481533:i=88024:add=on:rawr=on_2995 on theBenchmark for (2995ds/88024Mi)
% 19.75/3.47 % (290943)dis+10_1_sil=32000:sp=arity:random_seed=1200799912:i=103:fgj=on_2995 on theBenchmark for (2995ds/103Mi)
% 19.75/3.47 % (290944)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3461177640:i=116_2995 on theBenchmark for (2995ds/116Mi)
% 19.75/3.47 % (290945)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=490747600:i=131_2995 on theBenchmark for (2995ds/131Mi)
% 19.75/3.47 % (290946)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1247924353:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2995 on theBenchmark for (2995ds/159Mi)
% 19.75/3.47 % (290943)Instruction limit reached!
% 19.75/3.47 % (290943)------------------------------
% 19.75/3.47 % (290943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.75/3.47 % (290943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.47 % (290943)CaDiCaL version: 2.1.3
% 19.75/3.47 % (290943)Termination reason: Instruction limit
% 19.75/3.47 % (290943)Termination phase: Preprocessing 3
% 19.75/3.47 % (290943)Time elapsed: 0.078 s
% 19.75/3.47 % (290943)Peak memory usage: 36 MB
% 19.75/3.47 % (290943)Instructions burned: 104 (million)
% 19.75/3.47 % (290945)Instruction limit reached!
% 19.75/3.47 % (290945)------------------------------
% 19.75/3.47 % (290945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.75/3.47 % (290945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.47 % (290945)CaDiCaL version: 2.1.3
% 19.75/3.47 % (290945)Termination reason: Instruction limit
% 19.75/3.47 % (290945)Termination phase: Preprocessing 3
% 19.75/3.47 % (290945)Time elapsed: 0.090 s
% 19.75/3.47 % (290945)Peak memory usage: 36 MB
% 19.75/3.47 % (290945)Instructions burned: 131 (million)
% 19.75/3.47 % (290944)Instruction limit reached!
% 19.75/3.47 % (290944)------------------------------
% 19.75/3.47 % (290944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.75/3.47 % (290944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.47 % (290944)CaDiCaL version: 2.1.3
% 19.75/3.47 % (290944)Termination reason: Instruction limit
% 19.75/3.47 % (290944)Termination phase: NewCNF
% 19.75/3.47 % (290944)Time elapsed: 0.093 s
% 19.75/3.47 % (290944)Peak memory usage: 38 MB
% 19.75/3.47 % (290944)Instructions burned: 116 (million)
% 19.75/3.47 % (290954)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3968150099:i=714:nm=2_2994 on theBenchmark for (2994ds/714Mi)
% 19.75/3.47 % (290946)Instruction limit reached!
% 19.75/3.47 % (290946)------------------------------
% 19.75/3.47 % (290946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.75/3.47 % (290946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.47 % (290946)CaDiCaL version: 2.1.3
% 19.75/3.47 % (290946)Termination reason: Instruction limit
% 19.75/3.47 % (290946)Termination phase: Preprocessing 3
% 19.75/3.47 % (290946)Time elapsed: 0.104 s
% 19.75/3.47 % (290946)Peak memory usage: 38 MB
% 19.75/3.47 % (290946)Instructions burned: 160 (million)
% 19.75/3.47 % (290955)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3699380088:i=131:bd=preordered:fsd=on_2994 on theBenchmark for (2994ds/131Mi)
% 19.75/3.47 % (290956)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=1509938819:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2994 on theBenchmark for (2994ds/684Mi)
% 19.75/3.47 % (290958)ott-21_1_sil=16000:fs=off:random_seed=891066687:i=180:av=off:fsr=off_2994 on theBenchmark for (2994ds/180Mi)
% 19.75/3.47 % (290955)Instruction limit reached!
% 19.75/3.47 % (290955)------------------------------
% 19.75/3.47 % (290955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.75/3.47 % (290955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.47 % (290955)CaDiCaL version: 2.1.3
% 19.75/3.47 % (290955)Termination reason: Instruction limit
% 37.71/5.90 % (290955)Termination phase: Preprocessing 3
% 37.71/5.90 % (290955)Time elapsed: 0.090 s
% 37.71/5.90 % (290955)Peak memory usage: 36 MB
% 37.71/5.90 % (290955)Instructions burned: 131 (million)
% 37.71/5.90 % (290962)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=640124541:i=477:bd=all_2993 on theBenchmark for (2993ds/477Mi)
% 37.71/5.90 % (290958)Instruction limit reached!
% 37.71/5.90 % (290958)------------------------------
% 37.71/5.90 % (290958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.71/5.90 % (290958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.71/5.90 % (290958)CaDiCaL version: 2.1.3
% 37.71/5.90 % (290958)Termination reason: Instruction limit
% 37.71/5.90 % (290958)Termination phase: Preprocessing 3
% 37.71/5.90 % (290958)Time elapsed: 0.118 s
% 37.71/5.90 % (290958)Peak memory usage: 38 MB
% 37.71/5.90 % (290958)Instructions burned: 182 (million)
% 37.71/5.90 % (290964)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2115520067:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 37.71/5.90 % (290956)Instruction limit reached!
% 37.71/5.90 % (290956)------------------------------
% 37.71/5.90 % (290956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.71/5.90 % (290956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.71/5.90 % (290956)CaDiCaL version: 2.1.3
% 37.71/5.90 % (290956)Termination reason: Instruction limit
% 37.71/5.90 % (290956)Termination phase: Saturation
% 37.71/5.90 % (290956)Time elapsed: 0.364 s
% 37.71/5.90 % (290956)Peak memory usage: 46 MB
% 37.71/5.90 % (290956)Instructions burned: 686 (million)
% 37.71/5.90 % (290962)Instruction limit reached!
% 37.71/5.90 % (290962)------------------------------
% 37.71/5.90 % (290962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.71/5.90 % (290962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.71/5.90 % (290962)CaDiCaL version: 2.1.3
% 37.71/5.90 % (290962)Termination reason: Instruction limit
% 37.71/5.90 % (290962)Termination phase: Saturation
% 37.71/5.90 % (290962)Time elapsed: 0.266 s
% 37.71/5.90 % (290962)Peak memory usage: 43 MB
% 37.71/5.90 % (290962)Instructions burned: 478 (million)
% 37.71/5.90 % (290954)Instruction limit reached!
% 37.71/5.90 % (290954)------------------------------
% 37.71/5.90 % (290954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.71/5.90 % (290954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.71/5.90 % (290954)CaDiCaL version: 2.1.3
% 37.71/5.90 % (290954)Termination reason: Instruction limit
% 37.71/5.90 % (290954)Termination phase: Property scanning
% 37.71/5.90 % (290954)Time elapsed: 0.403 s
% 37.71/5.90 % (290954)Peak memory usage: 73 MB
% 37.71/5.90 % (290954)Instructions burned: 716 (million)
% 37.71/5.90 % (290966)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2891275407:i=1179_2990 on theBenchmark for (2990ds/1179Mi)
% 37.71/5.90 % (290967)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1643057716:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi)
% 37.71/5.90 % (290969)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=1384290916:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 37.71/5.90 % (290964)Instruction limit reached!
% 37.71/5.90 % (290964)------------------------------
% 37.71/5.90 % (290964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.71/5.90 % (290964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.71/5.90 % (290964)CaDiCaL version: 2.1.3
% 37.71/5.90 % (290964)Termination reason: Instruction limit
% 37.71/5.90 % (290964)Termination phase: Property scanning
% 37.71/5.90 % (290964)Time elapsed: 0.450 s
% 37.71/5.90 % (290964)Peak memory usage: 71 MB
% 37.71/5.90 % (290964)Instructions burned: 867 (million)
% 37.71/5.90 % (290972)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=260571432:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 37.71/5.90 % (290969)Instruction limit reached!
% 37.71/5.90 % (290969)------------------------------
% 37.71/5.90 % (290969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.71/5.90 % (290969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.71/5.90 % (290969)CaDiCaL version: 2.1.3
% 37.71/5.90 % (290969)Termination reason: Instruction limit
% 37.71/5.90 % (290969)Termination phase: Saturation
% 47.85/7.40 % (290969)Time elapsed: 0.374 s
% 47.85/7.40 % (290969)Peak memory usage: 48 MB
% 47.85/7.40 % (290969)Instructions burned: 692 (million)
% 47.85/7.40 % (290974)fmb+10_1_sil=64000:random_seed=1914380916:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi)
% 47.85/7.40 % (290967)Instruction limit reached!
% 47.85/7.40 % (290967)------------------------------
% 47.85/7.40 % (290967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.40 % (290967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.40 % (290967)CaDiCaL version: 2.1.3
% 47.85/7.40 % (290967)Termination reason: Instruction limit
% 47.85/7.40 % (290967)Termination phase: Property scanning
% 47.85/7.40 % (290967)Time elapsed: 0.466 s
% 47.85/7.40 % (290967)Peak memory usage: 71 MB
% 47.85/7.40 % (290967)Instructions burned: 891 (million)
% 47.85/7.40 % (290976)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3681273370:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 47.85/7.40 % (290966)Instruction limit reached!
% 47.85/7.40 % (290966)------------------------------
% 47.85/7.40 % (290966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.40 % (290966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.40 % (290966)CaDiCaL version: 2.1.3
% 47.85/7.40 % (290966)Termination reason: Instruction limit
% 47.85/7.40 % (290966)Termination phase: Saturation
% 47.85/7.40 % (290966)Time elapsed: 0.634 s
% 47.85/7.40 % (290966)Peak memory usage: 54 MB
% 47.85/7.40 % (290966)Instructions burned: 1180 (million)
% 47.85/7.40 % (290978)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2465564733:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 47.85/7.40 % (290972)Instruction limit reached!
% 47.85/7.40 % (290972)------------------------------
% 47.85/7.40 % (290972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.40 % (290972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.40 % (290972)CaDiCaL version: 2.1.3
% 47.85/7.40 % (290972)Termination reason: Instruction limit
% 47.85/7.40 % (290972)Termination phase: Saturation
% 47.85/7.40 % (290972)Time elapsed: 0.470 s
% 47.85/7.40 % (290972)Peak memory usage: 58 MB
% 47.85/7.40 % (290972)Instructions burned: 881 (million)
% 47.85/7.40 % (290980)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1064783941:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 47.85/7.40 % (290978)Instruction limit reached!
% 47.85/7.40 % (290978)------------------------------
% 47.85/7.40 % (290978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.40 % (290978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.40 % (290978)CaDiCaL version: 2.1.3
% 47.85/7.40 % (290978)Termination reason: Instruction limit
% 47.85/7.40 % (290978)Termination phase: Property scanning
% 47.85/7.40 % (290978)Time elapsed: 0.461 s
% 47.85/7.40 % (290978)Peak memory usage: 71 MB
% 47.85/7.40 % (290978)Instructions burned: 920 (million)
% 47.85/7.40 % (290982)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2221912840:i=1472:ins=7:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/1472Mi)
% 47.85/7.40 % (290982)Instruction limit reached!
% 47.85/7.40 % (290982)------------------------------
% 47.85/7.40 % (290982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.40 % (290982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.40 % (290982)CaDiCaL version: 2.1.3
% 47.85/7.40 % (290982)Termination reason: Instruction limit
% 47.85/7.40 % (290982)Termination phase: Saturation
% 47.85/7.40 % (290982)Time elapsed: 0.819 s
% 47.85/7.40 % (290982)Peak memory usage: 60 MB
% 47.85/7.40 % (290982)Instructions burned: 1473 (million)
% 47.85/7.40 % (290984)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3956233111:i=6324_2970 on theBenchmark for (2970ds/6324Mi)
% 47.85/7.40 % Detected minimum model sizes of [447]
% 47.85/7.40 % Detected maximum model sizes of [max]
% 47.85/7.40 % (290940)Cannot represent all propositional literals internally
% 47.85/7.40 % (290940)Refutation not found, incomplete strategy
% 47.85/7.40 % (290940)------------------------------
% 47.85/7.40 % (290940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.85/7.40 % (290940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.85/7.40 % (290940)CaDiCaL version: 2.1.3
% 47.85/7.40 % (290940)Termination reason: Refutation not found, incomplete strategy
% 47.85/7.40 % (290940)Time elapsed: 2.791 s
% 47.85/7.40 % (290940)Peak memory usage: 148 MB
% 77.46/11.52 % (290940)Instructions burned: 5811 (million)
% 77.46/11.52 % (290940)------------------------------
% 77.46/11.52 % (290940)------------------------------
% 77.46/11.52 % (290986)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2979231595:fmbsr=2.30978:i=2174_2967 on theBenchmark for (2967ds/2174Mi)
% 77.46/11.52 % Detected minimum model sizes of [447]
% 77.46/11.52 % Detected maximum model sizes of [max]
% 77.46/11.52 % (290974)Cannot represent all propositional literals internally
% 77.46/11.52 % (290974)Refutation not found, incomplete strategy
% 77.46/11.52 % (290974)------------------------------
% 77.46/11.52 % (290974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 77.46/11.52 % (290974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.46/11.52 % (290974)CaDiCaL version: 2.1.3
% 77.46/11.52 % (290974)Termination reason: Refutation not found, incomplete strategy
% 77.46/11.52 % (290974)Time elapsed: 2.354 s
% 77.46/11.52 % (290974)Peak memory usage: 132 MB
% 77.46/11.52 % (290974)Instructions burned: 5024 (million)
% 77.46/11.52 % (290974)------------------------------
% 77.46/11.52 % (290974)------------------------------
% 77.46/11.52 % (290988)ott-2_1_sil=16000:newcnf=on:random_seed=3389102219:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2962 on theBenchmark for (2962ds/869Mi)
% 77.46/11.52 % Detected minimum model sizes of [447]
% 77.46/11.52 % Detected maximum model sizes of [max]
% 77.46/11.52 % (290976)Cannot represent all propositional literals internally
% 77.46/11.52 % (290976)Refutation not found, incomplete strategy
% 77.46/11.52 % (290976)------------------------------
% 77.46/11.52 % (290976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 77.46/11.52 % (290976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.46/11.52 % (290976)CaDiCaL version: 2.1.3
% 77.46/11.52 % (290976)Termination reason: Refutation not found, incomplete strategy
% 77.46/11.52 % (290976)Time elapsed: 2.398 s
% 77.46/11.52 % (290976)Peak memory usage: 137 MB
% 77.46/11.52 % (290976)Instructions burned: 5222 (million)
% 77.46/11.52 % (290976)------------------------------
% 77.46/11.52 % (290976)------------------------------
% 77.46/11.52 % (290990)ott+10_1_sil=32000:tgt=ground:random_seed=2705285530:i=5114:av=off_2961 on theBenchmark for (2961ds/5114Mi)
% 77.46/11.52 % (290988)Instruction limit reached!
% 77.46/11.52 % (290988)------------------------------
% 77.46/11.52 % (290988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 77.46/11.52 % (290988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.46/11.52 % (290988)CaDiCaL version: 2.1.3
% 77.46/11.52 % (290988)Termination reason: Instruction limit
% 77.46/11.52 % (290988)Termination phase: Saturation
% 77.46/11.52 % (290988)Time elapsed: 0.451 s
% 77.46/11.52 % (290988)Peak memory usage: 51 MB
% 77.46/11.52 % (290988)Instructions burned: 870 (million)
% 77.46/11.52 % (290992)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3474461406:i=54282_2957 on theBenchmark for (2957ds/54282Mi)
% 77.46/11.52 % (290980)Instruction limit reached!
% 77.46/11.52 % (290980)------------------------------
% 77.46/11.52 % (290980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 77.46/11.52 % (290980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.46/11.52 % (290980)CaDiCaL version: 2.1.3
% 77.46/11.52 % (290980)Termination reason: Instruction limit
% 77.46/11.52 % (290980)Termination phase: Saturation
% 77.46/11.52 % (290980)Time elapsed: 2.652 s
% 77.46/11.52 % (290980)Peak memory usage: 95 MB
% 77.46/11.52 % (290980)Instructions burned: 5132 (million)
% 77.46/11.52 % (290994)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=199252630:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 77.46/11.52 % (290986)Instruction limit reached!
% 77.46/11.52 % (290986)------------------------------
% 77.46/11.52 % (290986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 77.46/11.52 % (290986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.46/11.52 % (290986)CaDiCaL version: 2.1.3
% 77.46/11.52 % (290986)Termination reason: Instruction limit
% 77.46/11.52 % (290986)Termination phase: Finite model building preprocessing
% 77.46/11.52 % (290986)Time elapsed: 1.106 s
% 77.46/11.52 % (290986)Peak memory usage: 109 MB
% 77.46/11.52 % (290986)Instructions burned: 2175 (million)
% 77.46/11.52 % (290996)dis+21_1_sil=32000:sas=cadical:random_seed=1750530629:i=3773:amm=off_2955 on theBenchmark for (2955ds/3773Mi)
% 77.46/11.52 % Detected minimum model sizes of [447]
% 77.46/11.52 % Detected maximum model sizes of [max]
% 77.46/11.52 % (290984)Cannot represent all propositional literals internally
% 66.30/23.65 % (290984)Refutation not found, incomplete strategy
% 66.30/23.65 % (290984)------------------------------
% 66.30/23.65 % (290984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (290984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (290984)CaDiCaL version: 2.1.3
% 66.30/23.65 % (290984)Termination reason: Refutation not found, incomplete strategy
% 66.30/23.65 % (290984)Time elapsed: 2.717 s
% 66.30/23.65 % (290984)Peak memory usage: 147 MB
% 66.30/23.65 % (290984)Instructions burned: 5782 (million)
% 66.30/23.65 % (290984)------------------------------
% 66.30/23.65 % (290984)------------------------------
% 66.30/23.65 % (290998)ott+11_1_sil=16000:gs=on:random_seed=1108917158:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi)
% 66.30/23.65 % (290996)Instruction limit reached!
% 66.30/23.65 % (290996)------------------------------
% 66.30/23.65 % (290996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (290996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (290996)CaDiCaL version: 2.1.3
% 66.30/23.65 % (290996)Termination reason: Instruction limit
% 66.30/23.65 % (290996)Termination phase: Saturation
% 66.30/23.65 % (290996)Time elapsed: 1.615 s
% 66.30/23.65 % (290996)Peak memory usage: 67 MB
% 66.30/23.65 % (290996)Instructions burned: 3774 (million)
% 66.30/23.65 % (291000)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1083347700:fmbsr=1.6:i=67534_2939 on theBenchmark for (2939ds/67534Mi)
% 66.30/23.65 % (290994)Instruction limit reached!
% 66.30/23.65 % (290994)------------------------------
% 66.30/23.65 % (290994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (290994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (290994)CaDiCaL version: 2.1.3
% 66.30/23.65 % (290994)Termination reason: Instruction limit
% 66.30/23.65 % (290994)Termination phase: Saturation
% 66.30/23.65 % (290994)Time elapsed: 1.851 s
% 66.30/23.65 % (290994)Peak memory usage: 106 MB
% 66.30/23.65 % (290994)Instructions burned: 3513 (million)
% 66.30/23.65 % (291002)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=621067809:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2937 on theBenchmark for (2937ds/4591Mi)
% 66.30/23.65 % (290990)Instruction limit reached!
% 66.30/23.65 % (290990)------------------------------
% 66.30/23.65 % (290990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (290990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (290990)CaDiCaL version: 2.1.3
% 66.30/23.65 % (290990)Termination reason: Instruction limit
% 66.30/23.65 % (290990)Termination phase: Saturation
% 66.30/23.65 % (290990)Time elapsed: 2.838 s
% 66.30/23.65 % (290990)Peak memory usage: 76 MB
% 66.30/23.65 % (290990)Instructions burned: 5120 (million)
% 66.30/23.65 % (291004)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3063259752:i=29340_2932 on theBenchmark for (2932ds/29340Mi)
% 66.30/23.65 % Detected minimum model sizes of [447]
% 66.30/23.65 % Detected maximum model sizes of [max]
% 66.30/23.65 % (290992)Cannot represent all propositional literals internally
% 66.30/23.65 % (290992)Refutation not found, incomplete strategy
% 66.30/23.65 % (290992)------------------------------
% 66.30/23.65 % (290992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (290992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (290992)CaDiCaL version: 2.1.3
% 66.30/23.65 % (290992)Termination reason: Refutation not found, incomplete strategy
% 66.30/23.65 % (290992)Time elapsed: 2.728 s
% 66.30/23.65 % (290992)Peak memory usage: 149 MB
% 66.30/23.65 % (290992)Instructions burned: 5795 (million)
% 66.30/23.65 % (290992)------------------------------
% 66.30/23.65 % (290992)------------------------------
% 66.30/23.65 % (291006)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1712966446:i=5211_2929 on theBenchmark for (2929ds/5211Mi)
% 66.30/23.65 % (290998)Instruction limit reached!
% 66.30/23.65 % (290998)------------------------------
% 66.30/23.65 % (290998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (290998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (290998)CaDiCaL version: 2.1.3
% 66.30/23.65 % (290998)Termination reason: Instruction limit
% 66.30/23.65 % (290998)Termination phase: Saturation
% 66.30/23.65 % (290998)Time elapsed: 1.431 s
% 66.30/23.65 % (290998)Peak memory usage: 93 MB
% 66.30/23.65 % (290998)Instructions burned: 2251 (million)
% 66.30/23.65 % (291008)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4216102622:i=5497:nm=2_2928 on theBenchmark for (2928ds/5497Mi)
% 66.30/23.65 % (291002)Instruction limit reached!
% 66.30/23.65 % (291002)------------------------------
% 66.30/23.65 % (291002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291002)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291002)Termination reason: Instruction limit
% 66.30/23.65 % (291002)Termination phase: Saturation
% 66.30/23.65 % (291002)Time elapsed: 2.311 s
% 66.30/23.65 % (291002)Peak memory usage: 70 MB
% 66.30/23.65 % (291002)Instructions burned: 4593 (million)
% 66.30/23.65 % (291010)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=345628080:fmbsr=2:i=46332_2914 on theBenchmark for (2914ds/46332Mi)
% 66.30/23.65 % Detected minimum model sizes of [447]
% 66.30/23.65 % Detected maximum model sizes of [max]
% 66.30/23.65 % (291000)Cannot represent all propositional literals internally
% 66.30/23.65 % (291000)Refutation not found, incomplete strategy
% 66.30/23.65 % (291000)------------------------------
% 66.30/23.65 % (291000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291000)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291000)Termination reason: Refutation not found, incomplete strategy
% 66.30/23.65 % (291000)Time elapsed: 2.651 s
% 66.30/23.65 % (291000)Peak memory usage: 141 MB
% 66.30/23.65 % (291000)Instructions burned: 5795 (million)
% 66.30/23.65 % (291000)------------------------------
% 66.30/23.65 % (291000)------------------------------
% 66.30/23.65 % (291012)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=194073605:i=14071_2912 on theBenchmark for (2912ds/14071Mi)
% 66.30/23.65 % (291006)Instruction limit reached!
% 66.30/23.65 % (291006)------------------------------
% 66.30/23.65 % (291006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291006)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291006)Termination reason: Instruction limit
% 66.30/23.65 % (291006)Termination phase: Saturation
% 66.30/23.65 % (291006)Time elapsed: 2.352 s
% 66.30/23.65 % (291006)Peak memory usage: 70 MB
% 66.30/23.65 % (291006)Instructions burned: 5213 (million)
% 66.30/23.65 % (291014)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2119127476:i=22565:add=on:rawr=on_2905 on theBenchmark for (2905ds/22565Mi)
% 66.30/23.65 % Detected minimum model sizes of [447]
% 66.30/23.65 % Detected maximum model sizes of [max]
% 66.30/23.65 % (291008)Cannot represent all propositional literals internally
% 66.30/23.65 % (291008)Refutation not found, incomplete strategy
% 66.30/23.65 % (291008)------------------------------
% 66.30/23.65 % (291008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291008)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291008)Termination reason: Refutation not found, incomplete strategy
% 66.30/23.65 % (291008)Time elapsed: 2.604 s
% 66.30/23.65 % (291008)Peak memory usage: 141 MB
% 66.30/23.65 % (291008)Instructions burned: 5380 (million)
% 66.30/23.65 % (291008)------------------------------
% 66.30/23.65 % (291008)------------------------------
% 66.30/23.65 % (291016)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1936907972:i=8173:av=off_2901 on theBenchmark for (2901ds/8173Mi)
% 66.30/23.65 % Detected minimum model sizes of [447]
% 66.30/23.65 % Detected maximum model sizes of [max]
% 66.30/23.65 % (291012)Cannot represent all propositional literals internally
% 66.30/23.65 % (291012)Refutation not found, incomplete strategy
% 66.30/23.65 % (291012)------------------------------
% 66.30/23.65 % (291012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291012)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291012)Termination reason: Refutation not found, incomplete strategy
% 66.30/23.65 % (291012)Time elapsed: 2.472 s
% 66.30/23.65 % (291012)Peak memory usage: 140 MB
% 66.30/23.65 % (291012)Instructions burned: 5348 (million)
% 66.30/23.65 % Detected minimum model sizes of [447]
% 66.30/23.65 % Detected maximum model sizes of [max]
% 66.30/23.65 % (291010)Cannot represent all propositional literals internally
% 66.30/23.65 % (291010)Refutation not found, incomplete strategy
% 66.30/23.65 % (291010)------------------------------
% 66.30/23.65 % (291010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291010)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291010)Termination reason: Refutation not found, incomplete strategy
% 66.30/23.65 % (291010)Time elapsed: 2.676 s
% 66.30/23.65 % (291010)Peak memory usage: 141 MB
% 66.30/23.65 % (291010)Instructions burned: 5795 (million)
% 66.30/23.65 % (291012)------------------------------
% 66.30/23.65 % (291012)------------------------------
% 66.30/23.65 % (291010)------------------------------
% 66.30/23.65 % (291010)------------------------------
% 66.30/23.65 % (291019)ott-3_8_sil=64000:random_seed=165262007:i=20139:bs=on_2886 on theBenchmark for (2886ds/20139Mi)
% 66.30/23.65 % (291018)dis+10_16:1_sil=16000:random_seed=115537186:i=9155:fsr=off_2886 on theBenchmark for (2886ds/9155Mi)
% 66.30/23.65 % (291016)Instruction limit reached!
% 66.30/23.65 % (291016)------------------------------
% 66.30/23.65 % (291016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291016)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291016)Termination reason: Instruction limit
% 66.30/23.65 % (291016)Termination phase: Saturation
% 66.30/23.65 % (291016)Time elapsed: 5.062 s
% 66.30/23.65 % (291016)Peak memory usage: 93 MB
% 66.30/23.65 % (291016)Instructions burned: 8174 (million)
% 66.30/23.65 % (291022)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4254379983:fmbsr=2:i=32576_2850 on theBenchmark for (2850ds/32576Mi)
% 66.30/23.65 % (291018)Instruction limit reached!
% 66.30/23.65 % (291018)------------------------------
% 66.30/23.65 % (291018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291018)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291018)Termination reason: Instruction limit
% 66.30/23.65 % (291018)Termination phase: Saturation
% 66.30/23.65 % (291018)Time elapsed: 4.605 s
% 66.30/23.65 % (291018)Peak memory usage: 130 MB
% 66.30/23.65 % (291018)Instructions burned: 9155 (million)
% 66.30/23.65 % (291024)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2532918090:i=11404_2840 on theBenchmark for (2840ds/11404Mi)
% 66.30/23.65 % Detected minimum model sizes of [447]
% 66.30/23.65 % Detected maximum model sizes of [max]
% 66.30/23.65 % (291022)Cannot represent all propositional literals internally
% 66.30/23.65 % (291022)Refutation not found, incomplete strategy
% 66.30/23.65 % (291022)------------------------------
% 66.30/23.65 % (291022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.65 % (291022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.65 % (291022)CaDiCaL version: 2.1.3
% 66.30/23.65 % (291022)Termination reason: Refutation not found, incomplete strategy
% 66.30/23.65 % (291022)Time elapsed: 2.740 s
% 66.30/23.65 % (291022)Peak memory usage: 147 MB
% 66.30/23.65 % (291022)Instructions burned: 5782 (million)
% 66.30/23.65 % (291022)------------------------------
% 66.30/23.65 % (291022)------------------------------
% 66.30/23.65 % (291026)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3399669478:i=14134_2822 on theBenchmark for (2822ds/14134Mi)
% 66.30/23.65 % (291026) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-290935-291026"...
% 66.30/23.65 % (291026)...printing done.
% 66.30/23.65 % (291026)Refutation found. Thanks to Tanya!
% 66.30/23.65 % SZS status Theorem for theBenchmark
% 66.30/23.65 % SZS output start Proof for theBenchmark
% See solution above
% 66.30/23.67 % (291026)------------------------------
% 66.30/23.67 % (291026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.30/23.67 % (291026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.30/23.67 % (291026)CaDiCaL version: 2.1.3
% 66.30/23.67 % (291026)Termination reason: Refutation
% 66.30/23.67 % (291026)Time elapsed: 5.384 s
% 66.30/23.67 % (291026)Peak memory usage: 143 MB
% 66.30/23.67 % (291026)Instructions burned: 9521 (million)
% 66.30/23.67 % (290935)Success in time 23.402 s
% 66.30/23.67 % Vampire exiting
%------------------------------------------------------------------------------