%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR081+4 : 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 : n012.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:02 AM UTC 2026
% Result : Theorem 24.62s 9.63s
% Output : Refutation 24.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 32
% Syntax : Number of formulae : 236 ( 43 unt; 10 def)
% Number of atoms : 759 ( 0 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1007 ( 484 ~; 486 |; 14 &)
% ( 10 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 17 ( 16 usr; 11 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 15 con; 0-0 aty)
% Number of variables : 146 ( 0 sgn 146 !; 0 ?)
% 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+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/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f71,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__mother(X0,X1)
=> s__parent(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_71) ).
fof(f1123,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__sibling(X0,X1)
=> s__sibling(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_1126) ).
fof(f5906,axiom,
s__subclass(s__Animal,s__Organism),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5980) ).
fof(f5923,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5997) ).
fof(f5956,axiom,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6030) ).
fof(f5972,axiom,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6046) ).
fof(f5999,axiom,
s__subclass(s__Primate,s__Mammal),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6073) ).
fof(f6009,axiom,
s__subclass(s__Hominid,s__Primate),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6083) ).
fof(f6012,axiom,
s__subclass(s__Human,s__Hominid),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6086) ).
fof(f6017,axiom,
s__subclass(s__Man,s__Human),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6091) ).
fof(f6021,axiom,
s__subclass(s__Woman,s__Human),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6095) ).
fof(f6530,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( s__mother(X1,X0)
=> s__attribute(X0,s__Female) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6612) ).
fof(f6555,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__Organism)
& s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( ( s__sibling(X0,X1)
& s__parent(X0,X2) )
=> s__parent(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6637) ).
fof(f6557,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( ( s__parent(X0,X1)
& s__attribute(X1,s__Female) )
=> s__mother(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6639) ).
fof(f7218,axiom,
s__instance(s__Bill7_1,s__Man),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f7219,axiom,
s__instance(s__Jane7_1,s__Woman),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f7220,axiom,
s__instance(s__Bob7_1,s__Man),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f7221,axiom,
s__mother(s__Bill7_1,s__Jane7_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_4) ).
fof(f7222,axiom,
s__sibling(s__Bob7_1,s__Bill7_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_5) ).
fof(f7223,conjecture,
( s__mother(s__Bill7_1,s__Jane7_1)
& s__mother(s__Bob7_1,s__Jane7_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f7224,negated_conjecture,
~ ( s__mother(s__Bill7_1,s__Jane7_1)
& s__mother(s__Bob7_1,s__Jane7_1) ),
inference(negated_conjecture,[status(cth)],[f7223]) ).
fof(f7318,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f7319,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(f7320,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,[],[f7319]) ).
fof(f7385,plain,
! [X0,X1] :
( s__parent(X0,X1)
| ~ s__mother(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f71]) ).
fof(f7386,plain,
! [X0,X1] :
( s__parent(X0,X1)
| ~ s__mother(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f7385]) ).
fof(f8233,plain,
! [X0,X1] :
( s__sibling(X1,X0)
| ~ s__sibling(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f1123]) ).
fof(f8234,plain,
! [X0,X1] :
( s__sibling(X1,X0)
| ~ s__sibling(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f8233]) ).
fof(f12243,plain,
! [X0,X1] :
( s__attribute(X0,s__Female)
| ~ s__mother(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f6530]) ).
fof(f12244,plain,
! [X0,X1] :
( s__attribute(X0,s__Female)
| ~ s__mother(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f12243]) ).
fof(f12253,plain,
! [X0,X1,X2] :
( s__parent(X1,X2)
| ~ s__sibling(X0,X1)
| ~ s__parent(X0,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f6555]) ).
fof(f12254,plain,
! [X0,X1,X2] :
( s__parent(X1,X2)
| ~ s__sibling(X0,X1)
| ~ s__parent(X0,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f12253]) ).
fof(f12257,plain,
! [X0,X1] :
( s__mother(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__attribute(X1,s__Female)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f6557]) ).
fof(f12258,plain,
! [X0,X1] :
( s__mother(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__attribute(X1,s__Female)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f12257]) ).
fof(f12412,plain,
( ~ s__mother(s__Bill7_1,s__Jane7_1)
| ~ s__mother(s__Bob7_1,s__Jane7_1) ),
inference(ennf_transformation,[],[f7224]) ).
fof(f14338,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7318]) ).
fof(f14339,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7318]) ).
fof(f14340,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,[],[f7320]) ).
fof(f14383,plain,
! [X0,X1] :
( ~ s__mother(X0,X1)
| s__parent(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f7386]) ).
fof(f15587,plain,
! [X0,X1] :
( s__sibling(X1,X0)
| ~ s__sibling(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f8234]) ).
fof(f21035,plain,
s__subclass(s__Animal,s__Organism),
inference(cnf_transformation,[],[f5906]) ).
fof(f21057,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[],[f5923]) ).
fof(f21090,plain,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f5956]) ).
fof(f21108,plain,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
inference(cnf_transformation,[],[f5972]) ).
fof(f21135,plain,
s__subclass(s__Primate,s__Mammal),
inference(cnf_transformation,[],[f5999]) ).
fof(f21145,plain,
s__subclass(s__Hominid,s__Primate),
inference(cnf_transformation,[],[f6009]) ).
fof(f21148,plain,
s__subclass(s__Human,s__Hominid),
inference(cnf_transformation,[],[f6012]) ).
fof(f21153,plain,
s__subclass(s__Man,s__Human),
inference(cnf_transformation,[],[f6017]) ).
fof(f21157,plain,
s__subclass(s__Woman,s__Human),
inference(cnf_transformation,[],[f6021]) ).
fof(f21796,plain,
! [X0,X1] :
( s__attribute(X0,s__Female)
| ~ s__mother(X1,X0)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f12244]) ).
fof(f21821,plain,
! [X2,X0,X1] :
( s__parent(X1,X2)
| ~ s__sibling(X0,X1)
| ~ s__parent(X0,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f12254]) ).
fof(f21823,plain,
! [X0,X1] :
( s__mother(X0,X1)
| ~ s__parent(X0,X1)
| ~ s__attribute(X1,s__Female)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f12258]) ).
fof(f22560,plain,
s__instance(s__Bill7_1,s__Man),
inference(cnf_transformation,[],[f7218]) ).
fof(f22561,plain,
s__instance(s__Jane7_1,s__Woman),
inference(cnf_transformation,[],[f7219]) ).
fof(f22562,plain,
s__instance(s__Bob7_1,s__Man),
inference(cnf_transformation,[],[f7220]) ).
fof(f22563,plain,
s__mother(s__Bill7_1,s__Jane7_1),
inference(cnf_transformation,[],[f7221]) ).
fof(f22564,plain,
s__sibling(s__Bob7_1,s__Bill7_1),
inference(cnf_transformation,[],[f7222]) ).
fof(f22565,plain,
( ~ s__mother(s__Bill7_1,s__Jane7_1)
| ~ s__mother(s__Bob7_1,s__Jane7_1) ),
inference(cnf_transformation,[],[f12412]) ).
fof(f23000,definition,
( spl504_1
<=> s__mother(s__Bob7_1,s__Jane7_1) ),
introduced(definition,[new_symbols(definition,[spl504_1])],[avatar_definition]) ).
fof(f23002,plain,
( ~ s__mother(s__Bob7_1,s__Jane7_1)
| spl504_1 ),
inference(avatar_component_clause,[],[f23000]) ).
fof(f23004,definition,
( spl504_2
<=> s__mother(s__Bill7_1,s__Jane7_1) ),
introduced(definition,[new_symbols(definition,[spl504_2])],[avatar_definition]) ).
fof(f23005,plain,
( s__mother(s__Bill7_1,s__Jane7_1)
| ~ spl504_2 ),
inference(avatar_component_clause,[],[f23004]) ).
fof(f23007,plain,
( ~ spl504_1
| ~ spl504_2 ),
inference(avatar_split_clause,[],[f22565,f23004,f23000]) ).
fof(f23010,plain,
spl504_2,
inference(avatar_split_clause,[],[f22563,f23004]) ).
fof(f32088,plain,
( s__parent(s__Bill7_1,s__Jane7_1)
| ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(s__Bill7_1,s__Organism)
| ~ spl504_2 ),
inference(resolution,[],[f14383,f23005]) ).
fof(f32090,definition,
( spl504_227
<=> s__instance(s__Bill7_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl504_227])],[avatar_definition]) ).
fof(f32091,plain,
( s__instance(s__Bill7_1,s__Organism)
| ~ spl504_227 ),
inference(avatar_component_clause,[],[f32090]) ).
fof(f32092,plain,
( ~ s__instance(s__Bill7_1,s__Organism)
| spl504_227 ),
inference(avatar_component_clause,[],[f32090]) ).
fof(f32094,definition,
( spl504_228
<=> s__instance(s__Jane7_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl504_228])],[avatar_definition]) ).
fof(f32095,plain,
( s__instance(s__Jane7_1,s__Organism)
| ~ spl504_228 ),
inference(avatar_component_clause,[],[f32094]) ).
fof(f32096,plain,
( ~ s__instance(s__Jane7_1,s__Organism)
| spl504_228 ),
inference(avatar_component_clause,[],[f32094]) ).
fof(f32098,definition,
( spl504_229
<=> s__parent(s__Bill7_1,s__Jane7_1) ),
introduced(definition,[new_symbols(definition,[spl504_229])],[avatar_definition]) ).
fof(f32100,plain,
( s__parent(s__Bill7_1,s__Jane7_1)
| ~ spl504_229 ),
inference(avatar_component_clause,[],[f32098]) ).
fof(f32101,plain,
( ~ spl504_227
| ~ spl504_228
| spl504_229
| ~ spl504_2 ),
inference(avatar_split_clause,[],[f32088,f23004,f32098,f32094,f32090]) ).
fof(f72749,definition,
( spl504_356
<=> s__instance(s__Human,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl504_356])],[avatar_definition]) ).
fof(f72750,plain,
( s__instance(s__Human,s__SetOrClass)
| ~ spl504_356 ),
inference(avatar_component_clause,[],[f72749]) ).
fof(f72751,plain,
( ~ s__instance(s__Human,s__SetOrClass)
| spl504_356 ),
inference(avatar_component_clause,[],[f72749]) ).
fof(f72771,plain,
( ! [X0] : ~ s__subclass(X0,s__Human)
| spl504_356 ),
inference(resolution,[],[f72751,f14338]) ).
fof(f72779,plain,
( $false
| spl504_356 ),
inference(resolution,[],[f72771,f21157]) ).
fof(f72782,plain,
spl504_356,
inference(avatar_contradiction_clause,[],[f72779]) ).
fof(f73629,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(s__Organism,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(resolution,[],[f14340,f32092]) ).
fof(f73655,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f73629,f14338]) ).
fof(f73870,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Bill7_1,X0) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f73655,f14339]) ).
fof(f74077,plain,
( ~ s__instance(s__Bill7_1,s__Animal)
| spl504_227 ),
inference(resolution,[],[f73870,f21035]) ).
fof(f74082,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(resolution,[],[f74077,f14340]) ).
fof(f74083,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f74082,f14338]) ).
fof(f74084,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Bill7_1,X0) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f74083,f14339]) ).
fof(f75898,plain,
( ~ s__instance(s__Bill7_1,s__Vertebrate)
| spl504_227 ),
inference(resolution,[],[f74084,f21057]) ).
fof(f75905,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(resolution,[],[f75898,f14340]) ).
fof(f75906,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f75905,f14338]) ).
fof(f75907,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Bill7_1,X0) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f75906,f14339]) ).
fof(f75994,plain,
( ~ s__instance(s__Bill7_1,s__WarmBloodedVertebrate)
| spl504_227 ),
inference(resolution,[],[f75907,f21090]) ).
fof(f76012,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(resolution,[],[f75994,f14340]) ).
fof(f76013,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f76012,f14338]) ).
fof(f76014,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Bill7_1,X0) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f76013,f14339]) ).
fof(f76100,plain,
( ~ s__instance(s__Bill7_1,s__Mammal)
| spl504_227 ),
inference(resolution,[],[f76014,f21108]) ).
fof(f76118,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(s__Mammal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(resolution,[],[f76100,f14340]) ).
fof(f76119,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f76118,f14338]) ).
fof(f76120,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Bill7_1,X0) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f76119,f14339]) ).
fof(f76285,plain,
( ~ s__instance(s__Bill7_1,s__Primate)
| spl504_227 ),
inference(resolution,[],[f76120,f21135]) ).
fof(f76317,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(s__Primate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(resolution,[],[f76285,f14340]) ).
fof(f76318,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f76317,f14338]) ).
fof(f76319,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Bill7_1,X0) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f76318,f14339]) ).
fof(f76646,plain,
( ~ s__instance(s__Bill7_1,s__Hominid)
| spl504_227 ),
inference(resolution,[],[f76319,f21145]) ).
fof(f76673,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(s__Hominid,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(resolution,[],[f76646,f14340]) ).
fof(f76674,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f76673,f14338]) ).
fof(f76675,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Bill7_1,X0) )
| spl504_227 ),
inference(forward_subsumption_resolution,[],[f76674,f14339]) ).
fof(f80450,plain,
( ~ s__instance(s__Bill7_1,s__Human)
| spl504_227 ),
inference(resolution,[],[f76675,f21148]) ).
fof(f80537,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(s__Human,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227 ),
inference(resolution,[],[f80450,f14340]) ).
fof(f80538,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Bill7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_227
| ~ spl504_356 ),
inference(forward_subsumption_resolution,[],[f80537,f72750]) ).
fof(f80539,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Bill7_1,X0) )
| spl504_227
| ~ spl504_356 ),
inference(forward_subsumption_resolution,[],[f80538,f14339]) ).
fof(f80578,plain,
( ~ s__instance(s__Bill7_1,s__Man)
| spl504_227
| ~ spl504_356 ),
inference(resolution,[],[f80539,f21153]) ).
fof(f80579,plain,
( $false
| spl504_227
| ~ spl504_356 ),
inference(forward_subsumption_resolution,[],[f80578,f22560]) ).
fof(f80580,plain,
( spl504_227
| ~ spl504_356 ),
inference(avatar_contradiction_clause,[],[f80579]) ).
fof(f80593,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(s__Organism,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(resolution,[],[f32096,f14340]) ).
fof(f80594,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80593,f14338]) ).
fof(f80595,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Jane7_1,X0) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80594,f14339]) ).
fof(f80599,definition,
( spl504_423
<=> s__instance(s__Organism,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl504_423])],[avatar_definition]) ).
fof(f80600,plain,
( s__instance(s__Organism,s__SetOrClass)
| ~ spl504_423 ),
inference(avatar_component_clause,[],[f80599]) ).
fof(f80601,plain,
( ~ s__instance(s__Organism,s__SetOrClass)
| spl504_423 ),
inference(avatar_component_clause,[],[f80599]) ).
fof(f80609,plain,
( ! [X0] : ~ s__subclass(X0,s__Organism)
| spl504_423 ),
inference(resolution,[],[f80601,f14338]) ).
fof(f80632,plain,
( $false
| spl504_423 ),
inference(resolution,[],[f80609,f21035]) ).
fof(f80639,plain,
spl504_423,
inference(avatar_contradiction_clause,[],[f80632]) ).
fof(f80658,plain,
( ~ s__instance(s__Jane7_1,s__Animal)
| spl504_228 ),
inference(resolution,[],[f80595,f21035]) ).
fof(f80663,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(resolution,[],[f80658,f14340]) ).
fof(f80664,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80663,f14338]) ).
fof(f80665,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Jane7_1,X0) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80664,f14339]) ).
fof(f80699,plain,
( ~ s__instance(s__Jane7_1,s__Vertebrate)
| spl504_228 ),
inference(resolution,[],[f80665,f21057]) ).
fof(f80707,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(resolution,[],[f80699,f14340]) ).
fof(f80708,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80707,f14338]) ).
fof(f80709,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Jane7_1,X0) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80708,f14339]) ).
fof(f80768,plain,
( ~ s__instance(s__Jane7_1,s__WarmBloodedVertebrate)
| spl504_228 ),
inference(resolution,[],[f80709,f21090]) ).
fof(f80772,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(resolution,[],[f80768,f14340]) ).
fof(f80773,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80772,f14338]) ).
fof(f80774,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Jane7_1,X0) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80773,f14339]) ).
fof(f80889,plain,
( ~ s__instance(s__Jane7_1,s__Mammal)
| spl504_228 ),
inference(resolution,[],[f80774,f21108]) ).
fof(f80908,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(s__Mammal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(resolution,[],[f80889,f14340]) ).
fof(f80909,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80908,f14338]) ).
fof(f80910,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Jane7_1,X0) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f80909,f14339]) ).
fof(f81050,plain,
( ~ s__instance(s__Jane7_1,s__Primate)
| spl504_228 ),
inference(resolution,[],[f80910,f21135]) ).
fof(f81087,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(s__Primate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(resolution,[],[f81050,f14340]) ).
fof(f81088,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f81087,f14338]) ).
fof(f81089,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Jane7_1,X0) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f81088,f14339]) ).
fof(f81127,plain,
( ~ s__instance(s__Jane7_1,s__Hominid)
| spl504_228 ),
inference(resolution,[],[f81089,f21145]) ).
fof(f81147,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(s__Hominid,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(resolution,[],[f81127,f14340]) ).
fof(f81148,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f81147,f14338]) ).
fof(f81149,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Jane7_1,X0) )
| spl504_228 ),
inference(forward_subsumption_resolution,[],[f81148,f14339]) ).
fof(f81196,plain,
( ~ s__instance(s__Jane7_1,s__Human)
| spl504_228 ),
inference(resolution,[],[f81149,f21148]) ).
fof(f81197,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(s__Human,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228 ),
inference(resolution,[],[f81196,f14340]) ).
fof(f81198,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Jane7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_228
| ~ spl504_356 ),
inference(forward_subsumption_resolution,[],[f81197,f72750]) ).
fof(f81199,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Jane7_1,X0) )
| spl504_228
| ~ spl504_356 ),
inference(forward_subsumption_resolution,[],[f81198,f14339]) ).
fof(f81978,plain,
( ~ s__instance(s__Jane7_1,s__Woman)
| spl504_228
| ~ spl504_356 ),
inference(resolution,[],[f81199,f21157]) ).
fof(f81980,plain,
( $false
| spl504_228
| ~ spl504_356 ),
inference(forward_subsumption_resolution,[],[f81978,f22561]) ).
fof(f81981,plain,
( spl504_228
| ~ spl504_356 ),
inference(avatar_contradiction_clause,[],[f81980]) ).
fof(f87710,plain,
( ~ s__parent(s__Bob7_1,s__Jane7_1)
| ~ s__attribute(s__Jane7_1,s__Female)
| ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(s__Bob7_1,s__Organism)
| spl504_1 ),
inference(resolution,[],[f21823,f23002]) ).
fof(f87717,plain,
( ~ s__parent(s__Bob7_1,s__Jane7_1)
| ~ s__attribute(s__Jane7_1,s__Female)
| ~ s__instance(s__Bob7_1,s__Organism)
| spl504_1
| ~ spl504_228 ),
inference(forward_subsumption_resolution,[],[f87710,f32095]) ).
fof(f87719,definition,
( spl504_561
<=> s__instance(s__Bob7_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl504_561])],[avatar_definition]) ).
fof(f87720,plain,
( s__instance(s__Bob7_1,s__Organism)
| ~ spl504_561 ),
inference(avatar_component_clause,[],[f87719]) ).
fof(f87721,plain,
( ~ s__instance(s__Bob7_1,s__Organism)
| spl504_561 ),
inference(avatar_component_clause,[],[f87719]) ).
fof(f87723,definition,
( spl504_562
<=> s__attribute(s__Jane7_1,s__Female) ),
introduced(definition,[new_symbols(definition,[spl504_562])],[avatar_definition]) ).
fof(f87725,plain,
( ~ s__attribute(s__Jane7_1,s__Female)
| spl504_562 ),
inference(avatar_component_clause,[],[f87723]) ).
fof(f87727,definition,
( spl504_563
<=> s__parent(s__Bob7_1,s__Jane7_1) ),
introduced(definition,[new_symbols(definition,[spl504_563])],[avatar_definition]) ).
fof(f87729,plain,
( ~ s__parent(s__Bob7_1,s__Jane7_1)
| spl504_563 ),
inference(avatar_component_clause,[],[f87727]) ).
fof(f87730,plain,
( ~ spl504_561
| ~ spl504_562
| ~ spl504_563
| spl504_1
| ~ spl504_228 ),
inference(avatar_split_clause,[],[f87717,f32094,f23000,f87727,f87723,f87719]) ).
fof(f87744,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(s__Organism,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_561 ),
inference(resolution,[],[f87721,f14340]) ).
fof(f87745,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f87744,f80600]) ).
fof(f87746,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Bob7_1,X0) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f87745,f14339]) ).
fof(f87757,plain,
( ~ s__instance(s__Bob7_1,s__Animal)
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f87746,f21035]) ).
fof(f87768,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f87757,f14340]) ).
fof(f87769,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f87768,f14338]) ).
fof(f87770,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Bob7_1,X0) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f87769,f14339]) ).
fof(f87930,plain,
( ~ s__instance(s__Bob7_1,s__Vertebrate)
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f87770,f21057]) ).
fof(f87943,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f87930,f14340]) ).
fof(f87944,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f87943,f14338]) ).
fof(f87945,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Bob7_1,X0) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f87944,f14339]) ).
fof(f88754,plain,
( ~ s__instance(s__Bob7_1,s__WarmBloodedVertebrate)
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f87945,f21090]) ).
fof(f88773,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f88754,f14340]) ).
fof(f88774,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f88773,f14338]) ).
fof(f88775,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Bob7_1,X0) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f88774,f14339]) ).
fof(f88947,plain,
( ~ s__instance(s__Bob7_1,s__Mammal)
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f88775,f21108]) ).
fof(f88955,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(s__Mammal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f88947,f14340]) ).
fof(f88956,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f88955,f14338]) ).
fof(f88957,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Mammal)
| ~ s__instance(s__Bob7_1,X0) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f88956,f14339]) ).
fof(f89839,plain,
( ~ s__instance(s__Bob7_1,s__Primate)
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f88957,f21135]) ).
fof(f89885,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(s__Primate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f89839,f14340]) ).
fof(f89886,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f89885,f14338]) ).
fof(f89887,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Primate)
| ~ s__instance(s__Bob7_1,X0) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f89886,f14339]) ).
fof(f90330,plain,
( ~ s__instance(s__Bob7_1,s__Hominid)
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f89887,f21145]) ).
fof(f90412,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(s__Hominid,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f90330,f14340]) ).
fof(f90413,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f90412,f14338]) ).
fof(f90414,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Hominid)
| ~ s__instance(s__Bob7_1,X0) )
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f90413,f14339]) ).
fof(f90588,plain,
( ~ s__instance(s__Bob7_1,s__Human)
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f90414,f21148]) ).
fof(f90655,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(s__Human,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f90588,f14340]) ).
fof(f90656,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Bob7_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_356
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f90655,f72750]) ).
fof(f90657,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Human)
| ~ s__instance(s__Bob7_1,X0) )
| ~ spl504_356
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f90656,f14339]) ).
fof(f90863,plain,
( ~ s__instance(s__Bob7_1,s__Man)
| ~ spl504_356
| ~ spl504_423
| spl504_561 ),
inference(resolution,[],[f90657,f21153]) ).
fof(f90864,plain,
( $false
| ~ spl504_356
| ~ spl504_423
| spl504_561 ),
inference(forward_subsumption_resolution,[],[f90863,f22562]) ).
fof(f90865,plain,
( ~ spl504_356
| ~ spl504_423
| spl504_561 ),
inference(avatar_contradiction_clause,[],[f90864]) ).
fof(f90999,plain,
( ! [X0] :
( ~ s__mother(X0,s__Jane7_1)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Jane7_1,s__Organism) )
| spl504_562 ),
inference(resolution,[],[f87725,f21796]) ).
fof(f91002,plain,
( ! [X0] :
( ~ s__mother(X0,s__Jane7_1)
| ~ s__instance(X0,s__Organism) )
| ~ spl504_228
| spl504_562 ),
inference(forward_subsumption_resolution,[],[f90999,f32095]) ).
fof(f91102,plain,
( ~ s__instance(s__Bill7_1,s__Organism)
| ~ spl504_2
| ~ spl504_228
| spl504_562 ),
inference(resolution,[],[f91002,f23005]) ).
fof(f91107,plain,
( $false
| ~ spl504_2
| ~ spl504_227
| ~ spl504_228
| spl504_562 ),
inference(forward_subsumption_resolution,[],[f91102,f32091]) ).
fof(f91108,plain,
( ~ spl504_2
| ~ spl504_227
| ~ spl504_228
| spl504_562 ),
inference(avatar_contradiction_clause,[],[f91107]) ).
fof(f126916,plain,
( ! [X0] :
( ~ s__sibling(X0,s__Bob7_1)
| ~ s__parent(X0,s__Jane7_1)
| ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(s__Bob7_1,s__Organism)
| ~ s__instance(X0,s__Organism) )
| spl504_563 ),
inference(resolution,[],[f21821,f87729]) ).
fof(f126925,plain,
( ! [X0] :
( ~ s__sibling(X0,s__Bob7_1)
| ~ s__parent(X0,s__Jane7_1)
| ~ s__instance(s__Bob7_1,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl504_228
| spl504_563 ),
inference(forward_subsumption_resolution,[],[f126916,f32095]) ).
fof(f126926,plain,
( ! [X0] :
( ~ s__sibling(X0,s__Bob7_1)
| ~ s__parent(X0,s__Jane7_1)
| ~ s__instance(X0,s__Organism) )
| ~ spl504_228
| ~ spl504_561
| spl504_563 ),
inference(forward_subsumption_resolution,[],[f126925,f87720]) ).
fof(f127809,plain,
( ! [X0] :
( ~ s__parent(X0,s__Jane7_1)
| ~ s__instance(X0,s__Organism)
| ~ s__sibling(s__Bob7_1,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Bob7_1,s__Organism) )
| ~ spl504_228
| ~ spl504_561
| spl504_563 ),
inference(resolution,[],[f126926,f15587]) ).
fof(f127812,plain,
( ! [X0] :
( ~ s__parent(X0,s__Jane7_1)
| ~ s__instance(X0,s__Organism)
| ~ s__sibling(s__Bob7_1,X0)
| ~ s__instance(s__Bob7_1,s__Organism) )
| ~ spl504_228
| ~ spl504_561
| spl504_563 ),
inference(duplicate_literal_removal,[],[f127809]) ).
fof(f127813,plain,
( ! [X0] :
( ~ s__sibling(s__Bob7_1,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__parent(X0,s__Jane7_1) )
| ~ spl504_228
| ~ spl504_561
| spl504_563 ),
inference(forward_subsumption_resolution,[],[f127812,f87720]) ).
fof(f127814,plain,
( ~ s__instance(s__Bill7_1,s__Organism)
| ~ s__parent(s__Bill7_1,s__Jane7_1)
| ~ spl504_228
| ~ spl504_561
| spl504_563 ),
inference(resolution,[],[f127813,f22564]) ).
fof(f127819,plain,
( ~ s__parent(s__Bill7_1,s__Jane7_1)
| ~ spl504_227
| ~ spl504_228
| ~ spl504_561
| spl504_563 ),
inference(forward_subsumption_resolution,[],[f127814,f32091]) ).
fof(f127820,plain,
( $false
| ~ spl504_227
| ~ spl504_228
| ~ spl504_229
| ~ spl504_561
| spl504_563 ),
inference(forward_subsumption_resolution,[],[f127819,f32100]) ).
fof(f127821,plain,
( ~ spl504_227
| ~ spl504_228
| ~ spl504_229
| ~ spl504_561
| spl504_563 ),
inference(avatar_contradiction_clause,[],[f127820]) ).
cnf(s1,plain,
( ~ spl504_1
| ~ spl504_2 ),
inference(sat_conversion,[],[f23007]) ).
cnf(s3,plain,
spl504_2,
inference(sat_conversion,[],[f23010]) ).
cnf(s971,plain,
( ~ spl504_2
| ~ spl504_227
| ~ spl504_228
| spl504_229 ),
inference(sat_conversion,[],[f32101]) ).
cnf(s3866,plain,
spl504_356,
inference(sat_conversion,[],[f72782]) ).
cnf(s3917,plain,
( spl504_227
| ~ spl504_356 ),
inference(sat_conversion,[],[f80580]) ).
cnf(s3922,plain,
spl504_423,
inference(sat_conversion,[],[f80639]) ).
cnf(s3923,plain,
( spl504_228
| ~ spl504_356 ),
inference(sat_conversion,[],[f81981]) ).
cnf(s3998,plain,
( spl504_1
| ~ spl504_228
| ~ spl504_561
| ~ spl504_562
| ~ spl504_563 ),
inference(sat_conversion,[],[f87730]) ).
cnf(s3999,plain,
( ~ spl504_356
| ~ spl504_423
| spl504_561 ),
inference(sat_conversion,[],[f90865]) ).
cnf(s4000,plain,
( ~ spl504_2
| ~ spl504_227
| ~ spl504_228
| spl504_562 ),
inference(sat_conversion,[],[f91108]) ).
cnf(s4128,plain,
( ~ spl504_227
| ~ spl504_228
| ~ spl504_229
| ~ spl504_561
| spl504_563 ),
inference(sat_conversion,[],[f127821]) ).
cnf(s4151,plain,
spl504_561,
inference(rat,[],[s3999,s3922,s3866]) ).
cnf(s4152,plain,
spl504_228,
inference(rat,[],[s3923,s3866]) ).
cnf(s4153,plain,
spl504_227,
inference(rat,[],[s3917,s3866]) ).
cnf(s4195,plain,
( ~ spl504_2
| spl504_229 ),
inference(rat,[],[s971,s4152,s4153]) ).
cnf(s4301,plain,
spl504_562,
inference(rat,[],[s4000,s4153,s4152,s3]) ).
cnf(s4302,plain,
spl504_229,
inference(rat,[],[s4195,s3]) ).
cnf(s4303,plain,
spl504_563,
inference(rat,[],[s4128,s4153,s4151,s4152,s4302]) ).
cnf(s4304,plain,
spl504_1,
inference(rat,[],[s3998,s4301,s4152,s4151,s4303]) ).
cnf(s4305,plain,
$false,
inference(rat,[],[s1,s3,s4304]) ).
fof(f127822,plain,
$false,
inference(avatar_sat_refutation,[],[s4305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR081+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 22:32:04 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.12 Running first-order model finding
% 0.09/0.12 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
% 4.26/1.01 % (3867368)Will run a generic schedule for satisfiability detection.
% 4.26/1.01 % (3867374)% WARNING: option uhcvi not known.
% 4.26/1.01 % (3867377)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=875539585:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.26/1.01 % (3867375)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=765559910:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.26/1.01 % (3867373)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2514800691_2999 on theBenchmark for (2999ds/0Mi)
% 4.26/1.01 % (3867374)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2417121825:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.26/1.01 % (3867376)dis+10_1_sil=32000:sp=arity:random_seed=2211596383:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.26/1.01 % (3867378)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4211441228:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.26/1.01 % (3867379)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=627661061:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.26/1.01 % (3867376)Instruction limit reached!
% 4.26/1.01 % (3867376)------------------------------
% 4.26/1.01 % (3867376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.26/1.01 % (3867376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.01 % (3867376)CaDiCaL version: 2.1.3
% 4.26/1.01 % (3867376)Termination reason: Instruction limit
% 4.26/1.01 % (3867376)Termination phase: Property scanning
% 4.26/1.01 % (3867376)Time elapsed: 0.039 s
% 4.26/1.01 % (3867376)Peak memory usage: 24 MB
% 4.26/1.01 % (3867376)Instructions burned: 105 (million)
% 4.26/1.01 % (3867377)Instruction limit reached!
% 4.26/1.01 % (3867377)------------------------------
% 4.26/1.01 % (3867377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.26/1.01 % (3867377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.01 % (3867377)CaDiCaL version: 2.1.3
% 4.26/1.01 % (3867377)Termination reason: Instruction limit
% 4.26/1.01 % (3867377)Termination phase: Property scanning
% 4.26/1.01 % (3867377)Time elapsed: 0.042 s
% 4.26/1.01 % (3867377)Peak memory usage: 26 MB
% 4.26/1.01 % (3867377)Instructions burned: 116 (million)
% 4.26/1.01 % (3867378)Instruction limit reached!
% 4.26/1.01 % (3867378)------------------------------
% 4.26/1.01 % (3867378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.26/1.01 % (3867378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.01 % (3867378)CaDiCaL version: 2.1.3
% 4.26/1.01 % (3867378)Termination reason: Instruction limit
% 4.26/1.01 % (3867378)Termination phase: Property scanning
% 4.26/1.01 % (3867378)Time elapsed: 0.048 s
% 4.26/1.01 % (3867378)Peak memory usage: 24 MB
% 4.26/1.01 % (3867378)Instructions burned: 131 (million)
% 4.26/1.01 % (3867387)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=89541876:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 4.26/1.01 % (3867388)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1826798312:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.26/1.01 % (3867379)Instruction limit reached!
% 4.26/1.01 % (3867379)------------------------------
% 4.26/1.01 % (3867379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.26/1.01 % (3867379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.01 % (3867379)CaDiCaL version: 2.1.3
% 4.26/1.01 % (3867379)Termination reason: Instruction limit
% 4.26/1.01 % (3867379)Termination phase: Equality resolution with deletion
% 4.26/1.01 % (3867379)Time elapsed: 0.055 s
% 4.26/1.01 % (3867379)Peak memory usage: 25 MB
% 4.26/1.01 % (3867379)Instructions burned: 161 (million)
% 4.26/1.01 % (3867389)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=1948869791:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.26/1.01 % (3867392)ott-21_1_sil=16000:fs=off:random_seed=1466755066:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.26/1.01 % (3867388)Instruction limit reached!
% 4.26/1.01 % (3867388)------------------------------
% 4.26/1.01 % (3867388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.26/1.01 % (3867388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.59 % (3867388)CaDiCaL version: 2.1.3
% 8.26/1.59 % (3867388)Termination reason: Instruction limit
% 8.26/1.59 % (3867388)Termination phase: Property scanning
% 8.26/1.59 % (3867388)Time elapsed: 0.046 s
% 8.26/1.59 % (3867388)Peak memory usage: 24 MB
% 8.26/1.59 % (3867388)Instructions burned: 135 (million)
% 8.26/1.59 % (3867395)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=619156813:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 8.26/1.59 % (3867392)Instruction limit reached!
% 8.26/1.59 % (3867392)------------------------------
% 8.26/1.59 % (3867392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.59 % (3867392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.59 % (3867392)CaDiCaL version: 2.1.3
% 8.26/1.59 % (3867392)Termination reason: Instruction limit
% 8.26/1.59 % (3867392)Termination phase: Property scanning
% 8.26/1.59 % (3867392)Time elapsed: 0.057 s
% 8.26/1.59 % (3867392)Peak memory usage: 25 MB
% 8.26/1.59 % (3867392)Instructions burned: 180 (million)
% 8.26/1.59 % (3867397)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=448435134:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.26/1.59 % (3867387)Instruction limit reached!
% 8.26/1.59 % (3867387)------------------------------
% 8.26/1.59 % (3867387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.59 % (3867387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.59 % (3867387)CaDiCaL version: 2.1.3
% 8.26/1.59 % (3867387)Termination reason: Instruction limit
% 8.26/1.59 % (3867387)Termination phase: Finite model building preprocessing
% 8.26/1.59 % (3867387)Time elapsed: 0.191 s
% 8.26/1.59 % (3867387)Peak memory usage: 36 MB
% 8.26/1.59 % (3867387)Instructions burned: 714 (million)
% 8.26/1.59 % (3867395)Instruction limit reached!
% 8.26/1.59 % (3867395)------------------------------
% 8.26/1.59 % (3867395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.59 % (3867395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.59 % (3867395)CaDiCaL version: 2.1.3
% 8.26/1.59 % (3867395)Termination reason: Instruction limit
% 8.26/1.59 % (3867395)Termination phase: Saturation
% 8.26/1.59 % (3867395)Time elapsed: 0.140 s
% 8.26/1.59 % (3867395)Peak memory usage: 31 MB
% 8.26/1.59 % (3867395)Instructions burned: 480 (million)
% 8.26/1.59 % (3867399)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3007453166:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 8.26/1.59 % (3867389)Instruction limit reached!
% 8.26/1.59 % (3867389)------------------------------
% 8.26/1.59 % (3867389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.59 % (3867389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.59 % (3867389)CaDiCaL version: 2.1.3
% 8.26/1.59 % (3867389)Termination reason: Instruction limit
% 8.26/1.59 % (3867389)Termination phase: Saturation
% 8.26/1.59 % (3867389)Time elapsed: 0.203 s
% 8.26/1.59 % (3867389)Peak memory usage: 33 MB
% 8.26/1.59 % (3867389)Instructions burned: 684 (million)
% 8.26/1.59 % (3867400)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2351671493:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 8.26/1.59 % (3867402)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=633025990:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 8.26/1.60 % (3867397)Instruction limit reached!
% 8.26/1.60 % (3867397)------------------------------
% 8.26/1.60 % (3867397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.26/1.60 % (3867397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.26/1.60 % (3867397)CaDiCaL version: 2.1.3
% 8.26/1.60 % (3867397)Termination reason: Instruction limit
% 8.26/1.60 % (3867397)Termination phase: Finite model building preprocessing
% 8.26/1.60 % (3867397)Time elapsed: 0.233 s
% 8.26/1.60 % (3867397)Peak memory usage: 39 MB
% 8.26/1.60 % (3867397)Instructions burned: 865 (million)
% 8.26/1.60 % (3867405)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3949173490:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 8.26/1.60 % Detected minimum model sizes of [51]
% 8.26/1.60 % Detected maximum model sizes of [max]
% 8.26/1.60 % (3867373)Cannot represent all propositional literals internally
% 8.26/1.60 % (3867373)Refutation not found, incomplete strategy
% 8.26/1.60 % (3867373)------------------------------
% 16.32/2.68 % (3867373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.32/2.68 % (3867373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/2.68 % (3867373)CaDiCaL version: 2.1.3
% 16.32/2.68 % (3867373)Termination reason: Refutation not found, incomplete strategy
% 16.32/2.68 % (3867373)Time elapsed: 0.415 s
% 16.32/2.68 % (3867373)Peak memory usage: 48 MB
% 16.32/2.68 % (3867373)Instructions burned: 1462 (million)
% 16.32/2.68 % (3867373)------------------------------
% 16.32/2.68 % (3867373)------------------------------
% 16.32/2.68 % (3867407)fmb+10_1_sil=64000:random_seed=693238762:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 16.32/2.68 % (3867402)Instruction limit reached!
% 16.32/2.68 % (3867402)------------------------------
% 16.32/2.68 % (3867402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.32/2.68 % (3867402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/2.68 % (3867402)CaDiCaL version: 2.1.3
% 16.32/2.68 % (3867402)Termination reason: Instruction limit
% 16.32/2.68 % (3867402)Termination phase: Saturation
% 16.32/2.68 % (3867402)Time elapsed: 0.216 s
% 16.32/2.68 % (3867402)Peak memory usage: 36 MB
% 16.32/2.68 % (3867402)Instructions burned: 692 (million)
% 16.32/2.68 % (3867409)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=97315381:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 16.32/2.68 % (3867400)Instruction limit reached!
% 16.32/2.68 % (3867400)------------------------------
% 16.32/2.68 % (3867400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.32/2.68 % (3867400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/2.68 % (3867400)CaDiCaL version: 2.1.3
% 16.32/2.68 % (3867400)Termination reason: Instruction limit
% 16.32/2.68 % (3867400)Termination phase: Finite model building preprocessing
% 16.32/2.68 % (3867400)Time elapsed: 0.243 s
% 16.32/2.68 % (3867400)Peak memory usage: 40 MB
% 16.32/2.68 % (3867400)Instructions burned: 892 (million)
% 16.32/2.68 % (3867411)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1976202937:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 16.32/2.68 % (3867399)Instruction limit reached!
% 16.32/2.68 % (3867399)------------------------------
% 16.32/2.68 % (3867399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.32/2.68 % (3867399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/2.68 % (3867399)CaDiCaL version: 2.1.3
% 16.32/2.68 % (3867399)Termination reason: Instruction limit
% 16.32/2.68 % (3867399)Termination phase: Saturation
% 16.32/2.68 % (3867399)Time elapsed: 0.338 s
% 16.32/2.68 % (3867399)Peak memory usage: 36 MB
% 16.32/2.68 % (3867399)Instructions burned: 1180 (million)
% 16.32/2.68 % (3867413)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1922657061:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 16.32/2.68 % (3867405)Instruction limit reached!
% 16.32/2.68 % (3867405)------------------------------
% 16.32/2.68 % (3867405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.32/2.68 % (3867405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/2.68 % (3867405)CaDiCaL version: 2.1.3
% 16.32/2.68 % (3867405)Termination reason: Instruction limit
% 16.32/2.68 % (3867405)Termination phase: Saturation
% 16.32/2.68 % (3867405)Time elapsed: 0.240 s
% 16.32/2.68 % (3867405)Peak memory usage: 37 MB
% 16.32/2.68 % (3867405)Instructions burned: 880 (million)
% 16.32/2.68 % (3867415)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1595841659:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 16.32/2.68 % Detected minimum model sizes of [51]
% 16.32/2.68 % Detected maximum model sizes of [max]
% 16.32/2.68 % (3867407)Cannot represent all propositional literals internally
% 16.32/2.68 % (3867407)Refutation not found, incomplete strategy
% 16.32/2.68 % (3867407)------------------------------
% 16.32/2.68 % (3867407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.32/2.68 % (3867407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/2.68 % (3867407)CaDiCaL version: 2.1.3
% 16.32/2.68 % (3867407)Termination reason: Refutation not found, incomplete strategy
% 16.32/2.68 % (3867407)Time elapsed: 0.328 s
% 16.32/2.68 % (3867407)Peak memory usage: 42 MB
% 16.32/2.68 % (3867407)Instructions burned: 1182 (million)
% 16.32/2.68 % (3867407)------------------------------
% 16.32/2.68 % (3867407)------------------------------
% 16.32/2.68 % (3867411)Instruction limit reached!
% 21.96/3.46 % (3867411)------------------------------
% 21.96/3.46 % (3867411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.96/3.46 % (3867411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/3.46 % (3867411)CaDiCaL version: 2.1.3
% 21.96/3.46 % (3867411)Termination reason: Instruction limit
% 21.96/3.46 % (3867411)Termination phase: Finite model building preprocessing
% 21.96/3.46 % (3867411)Time elapsed: 0.248 s
% 21.96/3.46 % (3867411)Peak memory usage: 39 MB
% 21.96/3.46 % (3867411)Instructions burned: 924 (million)
% 21.96/3.46 % (3867417)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2120304471:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 21.96/3.46 % (3867418)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=33664713:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 21.96/3.46 % Detected minimum model sizes of [51]
% 21.96/3.46 % Detected maximum model sizes of [max]
% 21.96/3.46 % (3867409)Cannot represent all propositional literals internally
% 21.96/3.46 % (3867409)Refutation not found, incomplete strategy
% 21.96/3.46 % (3867409)------------------------------
% 21.96/3.46 % (3867409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.96/3.46 % (3867409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/3.46 % (3867409)CaDiCaL version: 2.1.3
% 21.96/3.46 % (3867409)Termination reason: Refutation not found, incomplete strategy
% 21.96/3.46 % (3867409)Time elapsed: 0.338 s
% 21.96/3.46 % (3867409)Peak memory usage: 44 MB
% 21.96/3.46 % (3867409)Instructions burned: 1257 (million)
% 21.96/3.46 % (3867409)------------------------------
% 21.96/3.46 % (3867409)------------------------------
% 21.96/3.46 % (3867421)ott-2_1_sil=16000:newcnf=on:random_seed=1834531063:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 21.96/3.46 % (3867415)Instruction limit reached!
% 21.96/3.46 % (3867415)------------------------------
% 21.96/3.46 % (3867415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.96/3.46 % (3867415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/3.46 % (3867415)CaDiCaL version: 2.1.3
% 21.96/3.46 % (3867415)Termination reason: Instruction limit
% 21.96/3.46 % (3867415)Termination phase: Saturation
% 21.96/3.46 % (3867415)Time elapsed: 0.427 s
% 21.96/3.46 % (3867415)Peak memory usage: 44 MB
% 21.96/3.46 % (3867415)Instructions burned: 1475 (million)
% 21.96/3.46 % (3867423)ott+10_1_sil=32000:tgt=ground:random_seed=2659500645:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 21.96/3.46 % (3867421)Instruction limit reached!
% 21.96/3.46 % (3867421)------------------------------
% 21.96/3.46 % (3867421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.96/3.46 % (3867421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/3.46 % (3867421)CaDiCaL version: 2.1.3
% 21.96/3.46 % (3867421)Termination reason: Instruction limit
% 21.96/3.46 % (3867421)Termination phase: Saturation
% 21.96/3.46 % (3867421)Time elapsed: 0.256 s
% 21.96/3.46 % (3867421)Peak memory usage: 38 MB
% 21.96/3.46 % (3867421)Instructions burned: 871 (million)
% 21.96/3.46 % (3867425)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1169916922:i=54282_2987 on theBenchmark for (2987ds/54282Mi)
% 21.96/3.46 % Detected minimum model sizes of [51]
% 21.96/3.46 % Detected maximum model sizes of [max]
% 21.96/3.46 % (3867417)Cannot represent all propositional literals internally
% 21.96/3.46 % (3867417)Refutation not found, incomplete strategy
% 21.96/3.46 % (3867417)------------------------------
% 21.96/3.46 % (3867417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.96/3.46 % (3867417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.96/3.46 % (3867417)CaDiCaL version: 2.1.3
% 21.96/3.46 % (3867417)Termination reason: Refutation not found, incomplete strategy
% 21.96/3.46 % (3867417)Time elapsed: 0.409 s
% 21.96/3.46 % (3867417)Peak memory usage: 48 MB
% 21.96/3.46 % (3867417)Instructions burned: 1457 (million)
% 21.96/3.46 % (3867417)------------------------------
% 21.96/3.46 % (3867417)------------------------------
% 21.96/3.46 % (3867427)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=244305757:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi)
% 21.96/3.46 % (3867418)Instruction limit reached!
% 21.96/3.46 % (3867418)------------------------------
% 21.96/3.46 % (3867418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.96/3.46 % (3867418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867418)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867418)Termination reason: Instruction limit
% 24.62/9.63 % (3867418)Termination phase: Finite model building preprocessing
% 24.62/9.63 % (3867418)Time elapsed: 0.574 s
% 24.62/9.63 % (3867418)Peak memory usage: 62 MB
% 24.62/9.63 % (3867418)Instructions burned: 2177 (million)
% 24.62/9.63 % (3867429)dis+21_1_sil=32000:sas=cadical:random_seed=1713852089:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi)
% 24.62/9.63 % Detected minimum model sizes of [51]
% 24.62/9.63 % Detected maximum model sizes of [max]
% 24.62/9.63 % (3867425)Cannot represent all propositional literals internally
% 24.62/9.63 % (3867425)Refutation not found, incomplete strategy
% 24.62/9.63 % (3867425)------------------------------
% 24.62/9.63 % (3867425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867425)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867425)Termination reason: Refutation not found, incomplete strategy
% 24.62/9.63 % (3867425)Time elapsed: 0.411 s
% 24.62/9.63 % (3867425)Peak memory usage: 48 MB
% 24.62/9.63 % (3867425)Instructions burned: 1464 (million)
% 24.62/9.63 % (3867425)------------------------------
% 24.62/9.63 % (3867425)------------------------------
% 24.62/9.63 % (3867431)ott+11_1_sil=16000:gs=on:random_seed=838006665:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi)
% 24.62/9.63 % (3867427)Instruction limit reached!
% 24.62/9.63 % (3867427)------------------------------
% 24.62/9.63 % (3867427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867427)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867427)Termination reason: Instruction limit
% 24.62/9.63 % (3867427)Termination phase: Saturation
% 24.62/9.63 % (3867427)Time elapsed: 0.842 s
% 24.62/9.63 % (3867427)Peak memory usage: 60 MB
% 24.62/9.63 % (3867427)Instructions burned: 3514 (million)
% 24.62/9.63 % (3867433)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2025625275:fmbsr=1.6:i=67534_2978 on theBenchmark for (2978ds/67534Mi)
% 24.62/9.63 % (3867413)Instruction limit reached!
% 24.62/9.63 % (3867413)------------------------------
% 24.62/9.63 % (3867413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867413)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867413)Termination reason: Instruction limit
% 24.62/9.63 % (3867413)Termination phase: Saturation
% 24.62/9.63 % (3867413)Time elapsed: 1.529 s
% 24.62/9.63 % (3867413)Peak memory usage: 57 MB
% 24.62/9.63 % (3867413)Instructions burned: 5132 (million)
% 24.62/9.63 % (3867435)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2583839286:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2977 on theBenchmark for (2977ds/4591Mi)
% 24.62/9.63 % (3867429)Instruction limit reached!
% 24.62/9.63 % (3867429)------------------------------
% 24.62/9.63 % (3867429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867429)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867429)Termination reason: Instruction limit
% 24.62/9.63 % (3867429)Termination phase: Saturation
% 24.62/9.63 % (3867429)Time elapsed: 0.944 s
% 24.62/9.63 % (3867429)Peak memory usage: 65 MB
% 24.62/9.63 % (3867429)Instructions burned: 3774 (million)
% 24.62/9.63 % (3867437)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4144260612:i=29340_2975 on theBenchmark for (2975ds/29340Mi)
% 24.62/9.63 % (3867431)Instruction limit reached!
% 24.62/9.63 % (3867431)------------------------------
% 24.62/9.63 % (3867431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867431)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867431)Termination reason: Instruction limit
% 24.62/9.63 % (3867431)Termination phase: Saturation
% 24.62/9.63 % (3867431)Time elapsed: 0.789 s
% 24.62/9.63 % (3867431)Peak memory usage: 75 MB
% 24.62/9.63 % (3867431)Instructions burned: 2252 (million)
% 24.62/9.63 % (3867439)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=656593836:i=5211_2975 on theBenchmark for (2975ds/5211Mi)
% 24.62/9.63 % Detected minimum model sizes of [51]
% 24.62/9.63 % Detected maximum model sizes of [max]
% 24.62/9.63 % (3867433)Cannot represent all propositional literals internally
% 24.62/9.63 % (3867433)Refutation not found, incomplete strategy
% 24.62/9.63 % (3867433)------------------------------
% 24.62/9.63 % (3867433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867433)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867433)Termination reason: Refutation not found, incomplete strategy
% 24.62/9.63 % (3867433)Time elapsed: 0.365 s
% 24.62/9.63 % (3867433)Peak memory usage: 45 MB
% 24.62/9.63 % (3867433)Instructions burned: 1418 (million)
% 24.62/9.63 % (3867433)------------------------------
% 24.62/9.63 % (3867433)------------------------------
% 24.62/9.63 % (3867441)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4125296156:i=5497:nm=2_2974 on theBenchmark for (2974ds/5497Mi)
% 24.62/9.63 % (3867423)Instruction limit reached!
% 24.62/9.63 % (3867423)------------------------------
% 24.62/9.63 % (3867423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867423)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867423)Termination reason: Instruction limit
% 24.62/9.63 % (3867423)Termination phase: Saturation
% 24.62/9.63 % (3867423)Time elapsed: 1.446 s
% 24.62/9.63 % (3867423)Peak memory usage: 63 MB
% 24.62/9.63 % (3867423)Instructions burned: 5117 (million)
% 24.62/9.63 % (3867443)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2424295188:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi)
% 24.62/9.63 % Detected minimum model sizes of [51]
% 24.62/9.63 % Detected maximum model sizes of [max]
% 24.62/9.63 % (3867441)Cannot represent all propositional literals internally
% 24.62/9.63 % (3867441)Refutation not found, incomplete strategy
% 24.62/9.63 % (3867441)------------------------------
% 24.62/9.63 % (3867441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867441)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867441)Termination reason: Refutation not found, incomplete strategy
% 24.62/9.63 % (3867441)Time elapsed: 0.365 s
% 24.62/9.63 % (3867441)Peak memory usage: 45 MB
% 24.62/9.63 % (3867441)Instructions burned: 1328 (million)
% 24.62/9.63 % (3867441)------------------------------
% 24.62/9.63 % (3867441)------------------------------
% 24.62/9.63 % (3867445)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1455062806:i=14071_2970 on theBenchmark for (2970ds/14071Mi)
% 24.62/9.63 % Detected minimum model sizes of [51]
% 24.62/9.63 % Detected maximum model sizes of [max]
% 24.62/9.63 % (3867443)Cannot represent all propositional literals internally
% 24.62/9.63 % (3867443)Refutation not found, incomplete strategy
% 24.62/9.63 % (3867443)------------------------------
% 24.62/9.63 % (3867443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867443)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867443)Termination reason: Refutation not found, incomplete strategy
% 24.62/9.63 % (3867443)Time elapsed: 0.374 s
% 24.62/9.63 % (3867443)Peak memory usage: 45 MB
% 24.62/9.63 % (3867443)Instructions burned: 1418 (million)
% 24.62/9.63 % (3867443)------------------------------
% 24.62/9.63 % (3867443)------------------------------
% 24.62/9.63 % (3867447)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1525521171:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi)
% 24.62/9.63 % Detected minimum model sizes of [51]
% 24.62/9.63 % Detected maximum model sizes of [max]
% 24.62/9.63 % (3867445)Cannot represent all propositional literals internally
% 24.62/9.63 % (3867445)Refutation not found, incomplete strategy
% 24.62/9.63 % (3867445)------------------------------
% 24.62/9.63 % (3867445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867445)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867445)Termination reason: Refutation not found, incomplete strategy
% 24.62/9.63 % (3867445)Time elapsed: 0.343 s
% 24.62/9.63 % (3867445)Peak memory usage: 46 MB
% 24.62/9.63 % (3867445)Instructions burned: 1286 (million)
% 24.62/9.63 % (3867445)------------------------------
% 24.62/9.63 % (3867445)------------------------------
% 24.62/9.63 % (3867449)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=10178656:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi)
% 24.62/9.63 % (3867439)Instruction limit reached!
% 24.62/9.63 % (3867439)------------------------------
% 24.62/9.63 % (3867439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867439)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867439)Termination reason: Instruction limit
% 24.62/9.63 % (3867439)Termination phase: Saturation
% 24.62/9.63 % (3867439)Time elapsed: 1.103 s
% 24.62/9.63 % (3867439)Peak memory usage: 47 MB
% 24.62/9.63 % (3867439)Instructions burned: 5213 (million)
% 24.62/9.63 % (3867451)dis+10_16:1_sil=16000:random_seed=1017279678:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi)
% 24.62/9.63 % (3867435)Instruction limit reached!
% 24.62/9.63 % (3867435)------------------------------
% 24.62/9.63 % (3867435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867435)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867435)Termination reason: Instruction limit
% 24.62/9.63 % (3867435)Termination phase: Saturation
% 24.62/9.63 % (3867435)Time elapsed: 1.478 s
% 24.62/9.63 % (3867435)Peak memory usage: 97 MB
% 24.62/9.63 % (3867435)Instructions burned: 4594 (million)
% 24.62/9.63 % (3867453)ott-3_8_sil=64000:random_seed=866921079:i=20139:bs=on_2962 on theBenchmark for (2962ds/20139Mi)
% 24.62/9.63 % (3867449)Instruction limit reached!
% 24.62/9.63 % (3867449)------------------------------
% 24.62/9.63 % (3867449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867449)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867449)Termination reason: Instruction limit
% 24.62/9.63 % (3867449)Termination phase: Saturation
% 24.62/9.63 % (3867449)Time elapsed: 2.484 s
% 24.62/9.63 % (3867449)Peak memory usage: 110 MB
% 24.62/9.63 % (3867449)Instructions burned: 8173 (million)
% 24.62/9.63 % (3867455)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4111416298:fmbsr=2:i=32576_2941 on theBenchmark for (2941ds/32576Mi)
% 24.62/9.63 % (3867451)Instruction limit reached!
% 24.62/9.63 % (3867451)------------------------------
% 24.62/9.63 % (3867451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867451)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867451)Termination reason: Instruction limit
% 24.62/9.63 % (3867451)Termination phase: Saturation
% 24.62/9.63 % (3867451)Time elapsed: 2.425 s
% 24.62/9.63 % (3867451)Peak memory usage: 92 MB
% 24.62/9.63 % (3867451)Instructions burned: 9158 (million)
% 24.62/9.63 % (3867457)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=358173902:i=11404_2939 on theBenchmark for (2939ds/11404Mi)
% 24.62/9.63 % Detected minimum model sizes of [51]
% 24.62/9.63 % Detected maximum model sizes of [max]
% 24.62/9.63 % (3867455)Cannot represent all propositional literals internally
% 24.62/9.63 % (3867455)Refutation not found, incomplete strategy
% 24.62/9.63 % (3867455)------------------------------
% 24.62/9.63 % (3867455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.63 % (3867455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.63 % (3867455)CaDiCaL version: 2.1.3
% 24.62/9.63 % (3867455)Termination reason: Refutation not found, incomplete strategy
% 24.62/9.63 % (3867455)Time elapsed: 0.406 s
% 24.62/9.63 % (3867455)Peak memory usage: 48 MB
% 24.62/9.63 % (3867455)Instructions burned: 1457 (million)
% 24.62/9.63 % (3867455)------------------------------
% 24.62/9.63 % (3867455)------------------------------
% 24.62/9.63 % (3867459)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3600413481:i=14134_2937 on theBenchmark for (2937ds/14134Mi)
% 24.62/9.63 % (3867459) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3867368-3867459"...
% 24.62/9.63 % (3867459)...printing done.
% 24.62/9.63 % (3867459)Refutation found. Thanks to Tanya!
% 24.62/9.63 % SZS status Theorem for theBenchmark
% 24.62/9.63 % SZS output start Proof for theBenchmark
% See solution above
% 24.62/9.64 % (3867459)------------------------------
% 24.62/9.64 % (3867459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.62/9.64 % (3867459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.62/9.64 % (3867459)CaDiCaL version: 2.1.3
% 24.62/9.64 % (3867459)Termination reason: Refutation
% 24.62/9.64 % (3867459)Time elapsed: 3.129 s
% 24.62/9.64 % (3867459)Peak memory usage: 95 MB
% 24.62/9.64 % (3867459)Instructions burned: 9108 (million)
% 24.62/9.64 % (3867368)Success in time 9.5 s
% 24.62/9.64 % Vampire exiting
%------------------------------------------------------------------------------