%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR093+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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:42:54 AM UTC 2026
% Result : Theorem 6.93s 1.84s
% Output : Refutation 8.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 54
% Syntax : Number of formulae : 263 ( 116 unt; 18 def)
% Number of atoms : 890 ( 0 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 1218 ( 591 ~; 595 |; 9 &)
% ( 18 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 19 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 81 ( 0 sgn 81 !; 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/theBenchmark.p',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/theBenchmark.p',kb_SUMO_27) ).
fof(f1504,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__Organism)
& s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( ( s__ancestor(X0,X1)
& s__ancestor(X1,X2) )
=> s__ancestor(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_1507) ).
fof(f32705,axiom,
s__subclass(s__Human,s__Organism),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_15957) ).
fof(f37982,axiom,
s__instance(s__Human23_1,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f37983,axiom,
s__instance(s__Human23_2,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f37984,axiom,
s__instance(s__Human23_3,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f37985,axiom,
s__instance(s__Human23_4,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_4) ).
fof(f37986,axiom,
s__instance(s__Human23_5,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_5) ).
fof(f37987,axiom,
s__instance(s__Human23_6,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_6) ).
fof(f37988,axiom,
s__instance(s__Human23_7,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_7) ).
fof(f37989,axiom,
s__instance(s__Human23_8,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_8) ).
fof(f37990,axiom,
s__instance(s__Human23_9,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_9) ).
fof(f37991,axiom,
s__instance(s__Human23_10,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_10) ).
fof(f37992,axiom,
s__instance(s__Human23_11,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_11) ).
fof(f37993,axiom,
s__instance(s__Human23_12,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_12) ).
fof(f37994,axiom,
s__instance(s__Human23_13,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_13) ).
fof(f37995,axiom,
s__instance(s__Human23_14,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_14) ).
fof(f37996,axiom,
s__instance(s__Human23_15,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_15) ).
fof(f37997,axiom,
s__instance(s__Human23_16,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_16) ).
fof(f37998,axiom,
s__ancestor(s__Human23_1,s__Human23_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_17) ).
fof(f37999,axiom,
s__ancestor(s__Human23_2,s__Human23_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_18) ).
fof(f38000,axiom,
s__ancestor(s__Human23_3,s__Human23_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_19) ).
fof(f38001,axiom,
s__ancestor(s__Human23_4,s__Human23_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_20) ).
fof(f38002,axiom,
s__ancestor(s__Human23_5,s__Human23_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_21) ).
fof(f38003,axiom,
s__ancestor(s__Human23_6,s__Human23_7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_22) ).
fof(f38004,axiom,
s__ancestor(s__Human23_7,s__Human23_8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_23) ).
fof(f38005,axiom,
s__ancestor(s__Human23_8,s__Human23_9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_24) ).
fof(f38006,axiom,
s__ancestor(s__Human23_9,s__Human23_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_25) ).
fof(f38007,axiom,
s__ancestor(s__Human23_10,s__Human23_11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_26) ).
fof(f38008,axiom,
s__ancestor(s__Human23_11,s__Human23_12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_27) ).
fof(f38009,axiom,
s__ancestor(s__Human23_12,s__Human23_13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_28) ).
fof(f38010,axiom,
s__ancestor(s__Human23_13,s__Human23_14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_29) ).
fof(f38011,axiom,
s__ancestor(s__Human23_14,s__Human23_15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_30) ).
fof(f38012,axiom,
s__ancestor(s__Human23_14,s__Human23_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_31) ).
fof(f38013,conjecture,
( s__ancestor(s__Human23_1,s__Human23_15)
& s__ancestor(s__Human23_1,s__Human23_16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f38014,negated_conjecture,
~ ( s__ancestor(s__Human23_1,s__Human23_15)
& s__ancestor(s__Human23_1,s__Human23_16) ),
inference(negated_conjecture,[status(cth)],[f38013]) ).
fof(f38025,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_15)
| ~ s__ancestor(s__Human23_1,s__Human23_16) ),
inference(ennf_transformation,[],[f38014]) ).
fof(f38032,plain,
! [X0,X1,X2] :
( s__ancestor(X0,X2)
| ~ s__ancestor(X0,X1)
| ~ s__ancestor(X1,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f1504]) ).
fof(f38033,plain,
! [X0,X1,X2] :
( s__ancestor(X0,X2)
| ~ s__ancestor(X0,X1)
| ~ s__ancestor(X1,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f38032]) ).
fof(f38077,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(f38078,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,[],[f38077]) ).
fof(f38079,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f38084,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_15)
| ~ s__ancestor(s__Human23_1,s__Human23_16) ),
inference(cnf_transformation,[],[f38025]) ).
fof(f38088,plain,
! [X2,X0,X1] :
( ~ s__ancestor(X1,X2)
| ~ s__ancestor(X0,X1)
| s__ancestor(X0,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f38033]) ).
fof(f38091,plain,
s__ancestor(s__Human23_1,s__Human23_2),
inference(cnf_transformation,[],[f37998]) ).
fof(f38092,plain,
s__instance(s__Human23_1,s__Human),
inference(cnf_transformation,[],[f37982]) ).
fof(f38093,plain,
s__ancestor(s__Human23_14,s__Human23_15),
inference(cnf_transformation,[],[f38011]) ).
fof(f38094,plain,
s__instance(s__Human23_15,s__Human),
inference(cnf_transformation,[],[f37996]) ).
fof(f38095,plain,
s__ancestor(s__Human23_14,s__Human23_16),
inference(cnf_transformation,[],[f38012]) ).
fof(f38096,plain,
s__instance(s__Human23_16,s__Human),
inference(cnf_transformation,[],[f37997]) ).
fof(f38107,plain,
s__subclass(s__Human,s__Organism),
inference(cnf_transformation,[],[f32705]) ).
fof(f38132,plain,
s__ancestor(s__Human23_2,s__Human23_3),
inference(cnf_transformation,[],[f37999]) ).
fof(f38133,plain,
s__instance(s__Human23_2,s__Human),
inference(cnf_transformation,[],[f37983]) ).
fof(f38139,plain,
s__ancestor(s__Human23_13,s__Human23_14),
inference(cnf_transformation,[],[f38010]) ).
fof(f38140,plain,
s__instance(s__Human23_14,s__Human),
inference(cnf_transformation,[],[f37995]) ).
fof(f38148,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,[],[f38078]) ).
fof(f38149,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f38079]) ).
fof(f38150,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f38079]) ).
fof(f38176,plain,
s__ancestor(s__Human23_3,s__Human23_4),
inference(cnf_transformation,[],[f38000]) ).
fof(f38177,plain,
s__instance(s__Human23_3,s__Human),
inference(cnf_transformation,[],[f37984]) ).
fof(f38178,plain,
s__ancestor(s__Human23_12,s__Human23_13),
inference(cnf_transformation,[],[f38009]) ).
fof(f38179,plain,
s__instance(s__Human23_13,s__Human),
inference(cnf_transformation,[],[f37994]) ).
fof(f38194,plain,
s__ancestor(s__Human23_4,s__Human23_5),
inference(cnf_transformation,[],[f38001]) ).
fof(f38195,plain,
s__instance(s__Human23_4,s__Human),
inference(cnf_transformation,[],[f37985]) ).
fof(f38196,plain,
s__ancestor(s__Human23_11,s__Human23_12),
inference(cnf_transformation,[],[f38008]) ).
fof(f38197,plain,
s__instance(s__Human23_12,s__Human),
inference(cnf_transformation,[],[f37993]) ).
fof(f38207,plain,
s__ancestor(s__Human23_5,s__Human23_6),
inference(cnf_transformation,[],[f38002]) ).
fof(f38208,plain,
s__instance(s__Human23_5,s__Human),
inference(cnf_transformation,[],[f37986]) ).
fof(f38209,plain,
s__ancestor(s__Human23_10,s__Human23_11),
inference(cnf_transformation,[],[f38007]) ).
fof(f38210,plain,
s__instance(s__Human23_11,s__Human),
inference(cnf_transformation,[],[f37992]) ).
fof(f38211,plain,
s__ancestor(s__Human23_6,s__Human23_7),
inference(cnf_transformation,[],[f38003]) ).
fof(f38212,plain,
s__instance(s__Human23_6,s__Human),
inference(cnf_transformation,[],[f37987]) ).
fof(f38213,plain,
s__ancestor(s__Human23_9,s__Human23_10),
inference(cnf_transformation,[],[f38006]) ).
fof(f38214,plain,
s__instance(s__Human23_10,s__Human),
inference(cnf_transformation,[],[f37991]) ).
fof(f38215,plain,
s__ancestor(s__Human23_7,s__Human23_8),
inference(cnf_transformation,[],[f38004]) ).
fof(f38216,plain,
s__instance(s__Human23_7,s__Human),
inference(cnf_transformation,[],[f37988]) ).
fof(f38217,plain,
s__ancestor(s__Human23_8,s__Human23_9),
inference(cnf_transformation,[],[f38005]) ).
fof(f38218,plain,
s__instance(s__Human23_9,s__Human),
inference(cnf_transformation,[],[f37990]) ).
fof(f38219,plain,
s__instance(s__Human23_8,s__Human),
inference(cnf_transformation,[],[f37989]) ).
fof(f38232,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f38148,f38149]) ).
fof(f38240,definition,
( spl2_1
<=> s__ancestor(s__Human23_1,s__Human23_16) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f38242,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_16)
| spl2_1 ),
inference(avatar_component_clause,[],[f38240]) ).
fof(f38244,definition,
( spl2_2
<=> s__ancestor(s__Human23_1,s__Human23_15) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f38247,plain,
( ~ spl2_1
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f38084,f38244,f38240]) ).
fof(f38248,plain,
! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X2,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f38232,f38150]) ).
fof(f38399,plain,
! [X0] :
( ~ s__instance(X0,s__Human)
| s__instance(X0,s__Organism) ),
inference(resolution,[],[f38248,f38107]) ).
fof(f39242,definition,
( spl2_127
<=> s__instance(s__Human23_14,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_127])],[avatar_definition]) ).
fof(f39243,plain,
( s__instance(s__Human23_14,s__Organism)
| ~ spl2_127 ),
inference(avatar_component_clause,[],[f39242]) ).
fof(f39244,plain,
( ~ s__instance(s__Human23_14,s__Organism)
| spl2_127 ),
inference(avatar_component_clause,[],[f39242]) ).
fof(f39246,definition,
( spl2_128
<=> s__instance(s__Human23_16,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_128])],[avatar_definition]) ).
fof(f39247,plain,
( s__instance(s__Human23_16,s__Organism)
| ~ spl2_128 ),
inference(avatar_component_clause,[],[f39246]) ).
fof(f39255,definition,
( spl2_130
<=> s__instance(s__Human23_15,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_130])],[avatar_definition]) ).
fof(f39256,plain,
( s__instance(s__Human23_15,s__Organism)
| ~ spl2_130 ),
inference(avatar_component_clause,[],[f39255]) ).
fof(f39264,definition,
( spl2_132
<=> s__instance(s__Human23_13,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_132])],[avatar_definition]) ).
fof(f39265,plain,
( s__instance(s__Human23_13,s__Organism)
| ~ spl2_132 ),
inference(avatar_component_clause,[],[f39264]) ).
fof(f39273,definition,
( spl2_134
<=> s__instance(s__Human23_12,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_134])],[avatar_definition]) ).
fof(f39274,plain,
( s__instance(s__Human23_12,s__Organism)
| ~ spl2_134 ),
inference(avatar_component_clause,[],[f39273]) ).
fof(f39275,plain,
( ~ s__instance(s__Human23_12,s__Organism)
| spl2_134 ),
inference(avatar_component_clause,[],[f39273]) ).
fof(f39282,definition,
( spl2_136
<=> s__instance(s__Human23_11,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_136])],[avatar_definition]) ).
fof(f39283,plain,
( s__instance(s__Human23_11,s__Organism)
| ~ spl2_136 ),
inference(avatar_component_clause,[],[f39282]) ).
fof(f39291,definition,
( spl2_138
<=> s__instance(s__Human23_10,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_138])],[avatar_definition]) ).
fof(f39292,plain,
( s__instance(s__Human23_10,s__Organism)
| ~ spl2_138 ),
inference(avatar_component_clause,[],[f39291]) ).
fof(f39293,plain,
( ~ s__instance(s__Human23_10,s__Organism)
| spl2_138 ),
inference(avatar_component_clause,[],[f39291]) ).
fof(f39300,definition,
( spl2_140
<=> s__instance(s__Human23_9,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_140])],[avatar_definition]) ).
fof(f39301,plain,
( s__instance(s__Human23_9,s__Organism)
| ~ spl2_140 ),
inference(avatar_component_clause,[],[f39300]) ).
fof(f39302,plain,
( ~ s__instance(s__Human23_9,s__Organism)
| spl2_140 ),
inference(avatar_component_clause,[],[f39300]) ).
fof(f39309,definition,
( spl2_142
<=> s__instance(s__Human23_8,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_142])],[avatar_definition]) ).
fof(f39310,plain,
( s__instance(s__Human23_8,s__Organism)
| ~ spl2_142 ),
inference(avatar_component_clause,[],[f39309]) ).
fof(f39318,definition,
( spl2_144
<=> s__instance(s__Human23_7,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_144])],[avatar_definition]) ).
fof(f39319,plain,
( s__instance(s__Human23_7,s__Organism)
| ~ spl2_144 ),
inference(avatar_component_clause,[],[f39318]) ).
fof(f39320,plain,
( ~ s__instance(s__Human23_7,s__Organism)
| spl2_144 ),
inference(avatar_component_clause,[],[f39318]) ).
fof(f39327,definition,
( spl2_146
<=> s__instance(s__Human23_6,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_146])],[avatar_definition]) ).
fof(f39328,plain,
( s__instance(s__Human23_6,s__Organism)
| ~ spl2_146 ),
inference(avatar_component_clause,[],[f39327]) ).
fof(f39329,plain,
( ~ s__instance(s__Human23_6,s__Organism)
| spl2_146 ),
inference(avatar_component_clause,[],[f39327]) ).
fof(f39336,definition,
( spl2_148
<=> s__instance(s__Human23_5,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_148])],[avatar_definition]) ).
fof(f39337,plain,
( s__instance(s__Human23_5,s__Organism)
| ~ spl2_148 ),
inference(avatar_component_clause,[],[f39336]) ).
fof(f39345,definition,
( spl2_150
<=> s__instance(s__Human23_4,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_150])],[avatar_definition]) ).
fof(f39346,plain,
( s__instance(s__Human23_4,s__Organism)
| ~ spl2_150 ),
inference(avatar_component_clause,[],[f39345]) ).
fof(f39347,plain,
( ~ s__instance(s__Human23_4,s__Organism)
| spl2_150 ),
inference(avatar_component_clause,[],[f39345]) ).
fof(f39354,definition,
( spl2_152
<=> s__instance(s__Human23_3,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_152])],[avatar_definition]) ).
fof(f39355,plain,
( s__instance(s__Human23_3,s__Organism)
| ~ spl2_152 ),
inference(avatar_component_clause,[],[f39354]) ).
fof(f39363,definition,
( spl2_154
<=> s__instance(s__Human23_2,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_154])],[avatar_definition]) ).
fof(f39364,plain,
( s__instance(s__Human23_2,s__Organism)
| ~ spl2_154 ),
inference(avatar_component_clause,[],[f39363]) ).
fof(f39365,plain,
( ~ s__instance(s__Human23_2,s__Organism)
| spl2_154 ),
inference(avatar_component_clause,[],[f39363]) ).
fof(f39372,definition,
( spl2_156
<=> s__instance(s__Human23_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl2_156])],[avatar_definition]) ).
fof(f39373,plain,
( s__instance(s__Human23_1,s__Organism)
| ~ spl2_156 ),
inference(avatar_component_clause,[],[f39372]) ).
fof(f39389,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_2)
| s__ancestor(X0,s__Human23_3)
| ~ s__instance(s__Human23_3,s__Organism)
| ~ s__instance(s__Human23_2,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38132]) ).
fof(f39390,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_3)
| s__ancestor(X0,s__Human23_4)
| ~ s__instance(s__Human23_4,s__Organism)
| ~ s__instance(s__Human23_3,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38176]) ).
fof(f39391,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_4)
| s__ancestor(X0,s__Human23_5)
| ~ s__instance(s__Human23_5,s__Organism)
| ~ s__instance(s__Human23_4,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38194]) ).
fof(f39392,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_5)
| s__ancestor(X0,s__Human23_6)
| ~ s__instance(s__Human23_6,s__Organism)
| ~ s__instance(s__Human23_5,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38207]) ).
fof(f39393,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_6)
| s__ancestor(X0,s__Human23_7)
| ~ s__instance(s__Human23_7,s__Organism)
| ~ s__instance(s__Human23_6,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38211]) ).
fof(f39394,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_7)
| s__ancestor(X0,s__Human23_8)
| ~ s__instance(s__Human23_8,s__Organism)
| ~ s__instance(s__Human23_7,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38215]) ).
fof(f39395,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_8)
| s__ancestor(X0,s__Human23_9)
| ~ s__instance(s__Human23_9,s__Organism)
| ~ s__instance(s__Human23_8,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38217]) ).
fof(f39396,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_9)
| s__ancestor(X0,s__Human23_10)
| ~ s__instance(s__Human23_10,s__Organism)
| ~ s__instance(s__Human23_9,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38213]) ).
fof(f39397,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_10)
| s__ancestor(X0,s__Human23_11)
| ~ s__instance(s__Human23_11,s__Organism)
| ~ s__instance(s__Human23_10,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38209]) ).
fof(f39398,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_11)
| s__ancestor(X0,s__Human23_12)
| ~ s__instance(s__Human23_12,s__Organism)
| ~ s__instance(s__Human23_11,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38196]) ).
fof(f39399,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_12)
| s__ancestor(X0,s__Human23_13)
| ~ s__instance(s__Human23_13,s__Organism)
| ~ s__instance(s__Human23_12,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38178]) ).
fof(f39400,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_13)
| s__ancestor(X0,s__Human23_14)
| ~ s__instance(s__Human23_14,s__Organism)
| ~ s__instance(s__Human23_13,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38139]) ).
fof(f39401,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_14)
| s__ancestor(X0,s__Human23_15)
| ~ s__instance(s__Human23_15,s__Organism)
| ~ s__instance(s__Human23_14,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38093]) ).
fof(f39402,plain,
! [X0] :
( ~ s__ancestor(X0,s__Human23_14)
| s__ancestor(X0,s__Human23_16)
| ~ s__instance(s__Human23_16,s__Organism)
| ~ s__instance(s__Human23_14,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f38088,f38095]) ).
fof(f39558,plain,
s__instance(s__Human23_1,s__Organism),
inference(resolution,[],[f38399,f38092]) ).
fof(f39559,plain,
s__instance(s__Human23_2,s__Organism),
inference(resolution,[],[f38399,f38133]) ).
fof(f39560,plain,
s__instance(s__Human23_3,s__Organism),
inference(resolution,[],[f38399,f38177]) ).
fof(f39561,plain,
s__instance(s__Human23_4,s__Organism),
inference(resolution,[],[f38399,f38195]) ).
fof(f39562,plain,
s__instance(s__Human23_5,s__Organism),
inference(resolution,[],[f38399,f38208]) ).
fof(f39563,plain,
s__instance(s__Human23_6,s__Organism),
inference(resolution,[],[f38399,f38212]) ).
fof(f39564,plain,
s__instance(s__Human23_7,s__Organism),
inference(resolution,[],[f38399,f38216]) ).
fof(f39565,plain,
s__instance(s__Human23_8,s__Organism),
inference(resolution,[],[f38399,f38219]) ).
fof(f39566,plain,
s__instance(s__Human23_9,s__Organism),
inference(resolution,[],[f38399,f38218]) ).
fof(f39567,plain,
s__instance(s__Human23_10,s__Organism),
inference(resolution,[],[f38399,f38214]) ).
fof(f39568,plain,
s__instance(s__Human23_11,s__Organism),
inference(resolution,[],[f38399,f38210]) ).
fof(f39569,plain,
s__instance(s__Human23_12,s__Organism),
inference(resolution,[],[f38399,f38197]) ).
fof(f39570,plain,
s__instance(s__Human23_13,s__Organism),
inference(resolution,[],[f38399,f38179]) ).
fof(f39571,plain,
s__instance(s__Human23_14,s__Organism),
inference(resolution,[],[f38399,f38140]) ).
fof(f39572,plain,
s__instance(s__Human23_15,s__Organism),
inference(resolution,[],[f38399,f38094]) ).
fof(f39573,plain,
s__instance(s__Human23_16,s__Organism),
inference(resolution,[],[f38399,f38096]) ).
fof(f39574,plain,
spl2_128,
inference(avatar_split_clause,[],[f39573,f39246]) ).
fof(f39575,plain,
spl2_130,
inference(avatar_split_clause,[],[f39572,f39255]) ).
fof(f39576,plain,
( $false
| spl2_127 ),
inference(forward_subsumption_resolution,[],[f39571,f39244]) ).
fof(f39577,plain,
spl2_127,
inference(avatar_contradiction_clause,[],[f39576]) ).
fof(f39578,plain,
spl2_132,
inference(avatar_split_clause,[],[f39570,f39264]) ).
fof(f39579,plain,
( $false
| spl2_134 ),
inference(forward_subsumption_resolution,[],[f39569,f39275]) ).
fof(f39580,plain,
spl2_134,
inference(avatar_contradiction_clause,[],[f39579]) ).
fof(f39581,plain,
spl2_136,
inference(avatar_split_clause,[],[f39568,f39282]) ).
fof(f39582,plain,
( $false
| spl2_138 ),
inference(forward_subsumption_resolution,[],[f39567,f39293]) ).
fof(f39583,plain,
spl2_138,
inference(avatar_contradiction_clause,[],[f39582]) ).
fof(f39584,plain,
( $false
| spl2_140 ),
inference(forward_subsumption_resolution,[],[f39566,f39302]) ).
fof(f39585,plain,
spl2_140,
inference(avatar_contradiction_clause,[],[f39584]) ).
fof(f39586,plain,
spl2_142,
inference(avatar_split_clause,[],[f39565,f39309]) ).
fof(f39587,plain,
( $false
| spl2_144 ),
inference(forward_subsumption_resolution,[],[f39564,f39320]) ).
fof(f39588,plain,
spl2_144,
inference(avatar_contradiction_clause,[],[f39587]) ).
fof(f39589,plain,
( $false
| spl2_146 ),
inference(forward_subsumption_resolution,[],[f39563,f39329]) ).
fof(f39590,plain,
spl2_146,
inference(avatar_contradiction_clause,[],[f39589]) ).
fof(f39591,plain,
spl2_148,
inference(avatar_split_clause,[],[f39562,f39336]) ).
fof(f39592,plain,
( $false
| spl2_150 ),
inference(forward_subsumption_resolution,[],[f39561,f39347]) ).
fof(f39593,plain,
spl2_150,
inference(avatar_contradiction_clause,[],[f39592]) ).
fof(f39594,plain,
spl2_152,
inference(avatar_split_clause,[],[f39560,f39354]) ).
fof(f39595,plain,
( $false
| spl2_154 ),
inference(forward_subsumption_resolution,[],[f39559,f39365]) ).
fof(f39596,plain,
spl2_154,
inference(avatar_contradiction_clause,[],[f39595]) ).
fof(f39597,plain,
spl2_156,
inference(avatar_split_clause,[],[f39558,f39372]) ).
fof(f39598,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_2)
| s__ancestor(X0,s__Human23_3)
| ~ s__instance(s__Human23_2,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_152 ),
inference(forward_subsumption_resolution,[],[f39389,f39355]) ).
fof(f39600,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_4)
| s__ancestor(X0,s__Human23_5)
| ~ s__instance(s__Human23_4,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_148 ),
inference(forward_subsumption_resolution,[],[f39391,f39337]) ).
fof(f39601,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_3)
| s__ancestor(X0,s__Human23_4)
| ~ s__instance(s__Human23_3,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_150 ),
inference(forward_subsumption_resolution,[],[f39390,f39346]) ).
fof(f39602,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_5)
| s__ancestor(X0,s__Human23_6)
| ~ s__instance(s__Human23_5,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_146 ),
inference(forward_subsumption_resolution,[],[f39392,f39328]) ).
fof(f39603,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_7)
| s__ancestor(X0,s__Human23_8)
| ~ s__instance(s__Human23_7,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_142 ),
inference(forward_subsumption_resolution,[],[f39394,f39310]) ).
fof(f39604,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_6)
| s__ancestor(X0,s__Human23_7)
| ~ s__instance(s__Human23_6,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_144 ),
inference(forward_subsumption_resolution,[],[f39393,f39319]) ).
fof(f39605,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_8)
| s__ancestor(X0,s__Human23_9)
| ~ s__instance(s__Human23_8,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_140 ),
inference(forward_subsumption_resolution,[],[f39395,f39301]) ).
fof(f39606,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_10)
| s__ancestor(X0,s__Human23_11)
| ~ s__instance(s__Human23_10,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_136 ),
inference(forward_subsumption_resolution,[],[f39397,f39283]) ).
fof(f39607,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_9)
| s__ancestor(X0,s__Human23_10)
| ~ s__instance(s__Human23_9,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_138 ),
inference(forward_subsumption_resolution,[],[f39396,f39292]) ).
fof(f39608,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_12)
| s__ancestor(X0,s__Human23_13)
| ~ s__instance(s__Human23_12,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_132 ),
inference(forward_subsumption_resolution,[],[f39399,f39265]) ).
fof(f39609,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_11)
| s__ancestor(X0,s__Human23_12)
| ~ s__instance(s__Human23_11,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_134 ),
inference(forward_subsumption_resolution,[],[f39398,f39274]) ).
fof(f39610,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_14)
| s__ancestor(X0,s__Human23_16)
| ~ s__instance(s__Human23_14,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_128 ),
inference(forward_subsumption_resolution,[],[f39402,f39247]) ).
fof(f39611,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_14)
| s__ancestor(X0,s__Human23_15)
| ~ s__instance(s__Human23_14,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_130 ),
inference(forward_subsumption_resolution,[],[f39401,f39256]) ).
fof(f39612,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_13)
| s__ancestor(X0,s__Human23_14)
| ~ s__instance(s__Human23_13,s__Organism)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_127 ),
inference(forward_subsumption_resolution,[],[f39400,f39243]) ).
fof(f39613,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_2)
| s__ancestor(X0,s__Human23_3)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_152
| ~ spl2_154 ),
inference(forward_subsumption_resolution,[],[f39598,f39364]) ).
fof(f39615,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_4)
| s__ancestor(X0,s__Human23_5)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_148
| ~ spl2_150 ),
inference(forward_subsumption_resolution,[],[f39600,f39346]) ).
fof(f39616,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_3)
| s__ancestor(X0,s__Human23_4)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_150
| ~ spl2_152 ),
inference(forward_subsumption_resolution,[],[f39601,f39355]) ).
fof(f39617,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_5)
| s__ancestor(X0,s__Human23_6)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_146
| ~ spl2_148 ),
inference(forward_subsumption_resolution,[],[f39602,f39337]) ).
fof(f39618,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_7)
| s__ancestor(X0,s__Human23_8)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_142
| ~ spl2_144 ),
inference(forward_subsumption_resolution,[],[f39603,f39319]) ).
fof(f39619,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_6)
| s__ancestor(X0,s__Human23_7)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_144
| ~ spl2_146 ),
inference(forward_subsumption_resolution,[],[f39604,f39328]) ).
fof(f39620,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_8)
| s__ancestor(X0,s__Human23_9)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_140
| ~ spl2_142 ),
inference(forward_subsumption_resolution,[],[f39605,f39310]) ).
fof(f39621,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_10)
| s__ancestor(X0,s__Human23_11)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_136
| ~ spl2_138 ),
inference(forward_subsumption_resolution,[],[f39606,f39292]) ).
fof(f39622,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_9)
| s__ancestor(X0,s__Human23_10)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_138
| ~ spl2_140 ),
inference(forward_subsumption_resolution,[],[f39607,f39301]) ).
fof(f39623,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_12)
| s__ancestor(X0,s__Human23_13)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_132
| ~ spl2_134 ),
inference(forward_subsumption_resolution,[],[f39608,f39274]) ).
fof(f39624,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_11)
| s__ancestor(X0,s__Human23_12)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_134
| ~ spl2_136 ),
inference(forward_subsumption_resolution,[],[f39609,f39283]) ).
fof(f39625,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_14)
| s__ancestor(X0,s__Human23_16)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_127
| ~ spl2_128 ),
inference(forward_subsumption_resolution,[],[f39610,f39243]) ).
fof(f39626,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_14)
| s__ancestor(X0,s__Human23_15)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_127
| ~ spl2_130 ),
inference(forward_subsumption_resolution,[],[f39611,f39243]) ).
fof(f39627,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_13)
| s__ancestor(X0,s__Human23_14)
| ~ s__instance(X0,s__Organism) )
| ~ spl2_127
| ~ spl2_132 ),
inference(forward_subsumption_resolution,[],[f39612,f39265]) ).
fof(f40542,plain,
( s__ancestor(s__Human23_1,s__Human23_3)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_152
| ~ spl2_154 ),
inference(resolution,[],[f39613,f38091]) ).
fof(f40543,plain,
( s__ancestor(s__Human23_1,s__Human23_3)
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f40542,f39373]) ).
fof(f40559,plain,
( s__ancestor(s__Human23_1,s__Human23_4)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f39616,f40543]) ).
fof(f40562,plain,
( s__ancestor(s__Human23_1,s__Human23_4)
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f40559,f39373]) ).
fof(f40702,plain,
( s__ancestor(s__Human23_1,s__Human23_5)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f40562,f39615]) ).
fof(f40707,plain,
( s__ancestor(s__Human23_1,s__Human23_5)
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f40702,f39373]) ).
fof(f40844,plain,
( s__ancestor(s__Human23_1,s__Human23_6)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f40707,f39617]) ).
fof(f40849,plain,
( s__ancestor(s__Human23_1,s__Human23_6)
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f40844,f39373]) ).
fof(f41027,plain,
( s__ancestor(s__Human23_1,s__Human23_7)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f40849,f39619]) ).
fof(f41032,plain,
( s__ancestor(s__Human23_1,s__Human23_7)
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f41027,f39373]) ).
fof(f41201,plain,
( s__ancestor(s__Human23_1,s__Human23_8)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f41032,f39618]) ).
fof(f41206,plain,
( s__ancestor(s__Human23_1,s__Human23_8)
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f41201,f39373]) ).
fof(f41359,plain,
( s__ancestor(s__Human23_1,s__Human23_9)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f41206,f39620]) ).
fof(f41364,plain,
( s__ancestor(s__Human23_1,s__Human23_9)
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f41359,f39373]) ).
fof(f41501,plain,
( s__ancestor(s__Human23_1,s__Human23_10)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f41364,f39622]) ).
fof(f41506,plain,
( s__ancestor(s__Human23_1,s__Human23_10)
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f41501,f39373]) ).
fof(f41627,plain,
( s__ancestor(s__Human23_1,s__Human23_11)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f41506,f39621]) ).
fof(f41632,plain,
( s__ancestor(s__Human23_1,s__Human23_11)
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f41627,f39373]) ).
fof(f41737,plain,
( s__ancestor(s__Human23_1,s__Human23_12)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f41632,f39624]) ).
fof(f41742,plain,
( s__ancestor(s__Human23_1,s__Human23_12)
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f41737,f39373]) ).
fof(f41831,plain,
( s__ancestor(s__Human23_1,s__Human23_13)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f41742,f39623]) ).
fof(f41836,plain,
( s__ancestor(s__Human23_1,s__Human23_13)
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f41831,f39373]) ).
fof(f42203,plain,
( s__ancestor(s__Human23_1,s__Human23_14)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_127
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f41836,f39627]) ).
fof(f42208,plain,
( s__ancestor(s__Human23_1,s__Human23_14)
| ~ spl2_127
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f42203,f39373]) ).
fof(f42237,plain,
( s__ancestor(s__Human23_1,s__Human23_15)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_127
| ~ spl2_130
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f42208,f39626]) ).
fof(f42238,plain,
( s__ancestor(s__Human23_1,s__Human23_16)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl2_127
| ~ spl2_128
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(resolution,[],[f42208,f39625]) ).
fof(f42243,plain,
( ~ s__instance(s__Human23_1,s__Organism)
| spl2_1
| ~ spl2_127
| ~ spl2_128
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f42238,f38242]) ).
fof(f42244,plain,
( s__ancestor(s__Human23_1,s__Human23_15)
| ~ spl2_127
| ~ spl2_130
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f42237,f39373]) ).
fof(f42247,plain,
( $false
| spl2_1
| ~ spl2_127
| ~ spl2_128
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(forward_subsumption_resolution,[],[f42243,f39373]) ).
fof(f42248,plain,
( spl2_1
| ~ spl2_127
| ~ spl2_128
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(avatar_contradiction_clause,[],[f42247]) ).
fof(f42249,plain,
( spl2_2
| ~ spl2_127
| ~ spl2_130
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(avatar_split_clause,[],[f42244,f39372,f39363,f39354,f39345,f39336,f39327,f39318,f39309,f39300,f39291,f39282,f39273,f39264,f39255,f39242,f38244]) ).
cnf(s1,plain,
( ~ spl2_1
| ~ spl2_2 ),
inference(sat_conversion,[],[f38247]) ).
cnf(s79,plain,
spl2_128,
inference(sat_conversion,[],[f39574]) ).
cnf(s80,plain,
spl2_130,
inference(sat_conversion,[],[f39575]) ).
cnf(s81,plain,
spl2_127,
inference(sat_conversion,[],[f39577]) ).
cnf(s82,plain,
spl2_132,
inference(sat_conversion,[],[f39578]) ).
cnf(s83,plain,
spl2_134,
inference(sat_conversion,[],[f39580]) ).
cnf(s84,plain,
spl2_136,
inference(sat_conversion,[],[f39581]) ).
cnf(s85,plain,
spl2_138,
inference(sat_conversion,[],[f39583]) ).
cnf(s86,plain,
spl2_140,
inference(sat_conversion,[],[f39585]) ).
cnf(s87,plain,
spl2_142,
inference(sat_conversion,[],[f39586]) ).
cnf(s88,plain,
spl2_144,
inference(sat_conversion,[],[f39588]) ).
cnf(s89,plain,
spl2_146,
inference(sat_conversion,[],[f39590]) ).
cnf(s90,plain,
spl2_148,
inference(sat_conversion,[],[f39591]) ).
cnf(s91,plain,
spl2_150,
inference(sat_conversion,[],[f39593]) ).
cnf(s92,plain,
spl2_152,
inference(sat_conversion,[],[f39594]) ).
cnf(s93,plain,
spl2_154,
inference(sat_conversion,[],[f39596]) ).
cnf(s94,plain,
spl2_156,
inference(sat_conversion,[],[f39597]) ).
cnf(s125,plain,
( spl2_1
| ~ spl2_127
| ~ spl2_128
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(sat_conversion,[],[f42248]) ).
cnf(s126,plain,
( spl2_2
| ~ spl2_127
| ~ spl2_130
| ~ spl2_132
| ~ spl2_134
| ~ spl2_136
| ~ spl2_138
| ~ spl2_140
| ~ spl2_142
| ~ spl2_144
| ~ spl2_146
| ~ spl2_148
| ~ spl2_150
| ~ spl2_152
| ~ spl2_154
| ~ spl2_156 ),
inference(sat_conversion,[],[f42249]) ).
cnf(s127,plain,
spl2_2,
inference(rat,[],[s126,s94,s93,s92,s91,s90,s89,s88,s87,s86,s85,s84,s83,s82,s81,s80]) ).
cnf(s128,plain,
spl2_1,
inference(rat,[],[s125,s94,s93,s92,s91,s90,s89,s88,s87,s86,s85,s84,s83,s82,s81,s79]) ).
cnf(s144,plain,
$false,
inference(rat,[],[s1,s127,s128]) ).
fof(f42250,plain,
$false,
inference(avatar_sat_refutation,[],[s144]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR093+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n006.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 22:42:10 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.93/1.83 % (291435)Detected formulas, will run a generic FOF schedule.
% 6.93/1.83 % (291446)dis-21_1_sil=8000:lcm=predicate:random_seed=2596657311:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 6.93/1.83 % (291445)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2205800761:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 6.93/1.83 % (291444)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2144634511:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 6.93/1.83 % (291441)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2445399528:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 6.93/1.83 % (291443)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2663693127:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 6.93/1.83 % (291440)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1453326989:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 6.93/1.83 % (291442)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=603998278:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 6.93/1.83 % (291446)Instruction limit reached!
% 6.93/1.83 % (291446)------------------------------
% 6.93/1.83 % (291446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291446)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291446)Termination reason: Instruction limit
% 6.93/1.83 % (291446)Termination phase: Preprocessing 2
% 6.93/1.83 % (291446)Time elapsed: 0.047 s
% 6.93/1.83 % (291446)Peak memory usage: 106 MB
% 6.93/1.83 % (291446)Instructions burned: 130 (million)
% 6.93/1.83 % (291443)Refutation not found, incomplete strategy
% 6.93/1.83 % (291443)------------------------------
% 6.93/1.83 % (291443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291443)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291443)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.83 % (291443)Time elapsed: 0.060 s
% 6.93/1.83 % (291443)Peak memory usage: 109 MB
% 6.93/1.83 % (291443)Instructions burned: 98 (million)
% 6.93/1.83 % (291445)Instruction limit reached!
% 6.93/1.83 % (291445)------------------------------
% 6.93/1.83 % (291445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291445)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291445)Termination reason: Instruction limit
% 6.93/1.83 % (291445)Termination phase: Property scanning
% 6.93/1.83 % (291445)Time elapsed: 0.061 s
% 6.93/1.83 % (291445)Peak memory usage: 104 MB
% 6.93/1.83 % (291445)Instructions burned: 141 (million)
% 6.93/1.83 % (291444)Instruction limit reached!
% 6.93/1.83 % (291444)------------------------------
% 6.93/1.83 % (291444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291444)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291444)Termination reason: Instruction limit
% 6.93/1.83 % (291444)Termination phase: Saturation
% 6.93/1.83 % (291444)Time elapsed: 0.075 s
% 6.93/1.83 % (291444)Peak memory usage: 108 MB
% 6.93/1.83 % (291444)Instructions burned: 120 (million)
% 6.93/1.83 % (291454)lrs+10_1_sil=8000:sp=occurrence:random_seed=2360415877:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 6.93/1.83 % (291455)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2146671363:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 6.93/1.83 % (291454)Instruction limit reached!
% 6.93/1.83 % (291454)------------------------------
% 6.93/1.83 % (291454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291454)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291454)Termination reason: Instruction limit
% 6.93/1.83 % (291454)Termination phase: Saturation
% 6.93/1.83 % (291454)Time elapsed: 0.097 s
% 6.93/1.83 % (291454)Peak memory usage: 111 MB
% 6.93/1.83 % (291454)Instructions burned: 286 (million)
% 6.93/1.83 % (291456)lrs+1011_1_sil=32000:sp=occurrence:random_seed=346337347:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 6.93/1.83 % (291455)Instruction limit reached!
% 6.93/1.83 % (291455)------------------------------
% 6.93/1.83 % (291455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291455)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291455)Termination reason: Instruction limit
% 6.93/1.83 % (291455)Termination phase: SInE selection
% 6.93/1.83 % (291455)Time elapsed: 0.069 s
% 6.93/1.83 % (291455)Peak memory usage: 104 MB
% 6.93/1.83 % (291455)Instructions burned: 158 (million)
% 6.93/1.83 % (291456)Refutation not found, incomplete strategy
% 6.93/1.83 % (291456)------------------------------
% 6.93/1.83 % (291456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291456)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291456)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.83 % (291456)Time elapsed: 0.064 s
% 6.93/1.83 % (291456)Peak memory usage: 109 MB
% 6.93/1.83 % (291456)Instructions burned: 87 (million)
% 6.93/1.83 % (291443)------------------------------
% 6.93/1.83 % (291443)------------------------------
% 6.93/1.83 % (291459)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3598926986:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 6.93/1.83 % (291459)Instruction limit reached!
% 6.93/1.83 % (291459)------------------------------
% 6.93/1.83 % (291459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291459)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291459)Termination reason: Instruction limit
% 6.93/1.83 % (291459)Termination phase: SInE selection
% 6.93/1.83 % (291459)Time elapsed: 0.070 s
% 6.93/1.83 % (291459)Peak memory usage: 105 MB
% 6.93/1.83 % (291459)Instructions burned: 251 (million)
% 6.93/1.83 % (291461)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=832792933:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 6.93/1.83 % (291463)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3330466771:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 6.93/1.83 % (291464)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3832928551:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 6.93/1.83 % (291461)Refutation not found, incomplete strategy
% 6.93/1.83 % (291461)------------------------------
% 6.93/1.83 % (291461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291461)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291461)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.83 % (291461)Time elapsed: 0.086 s
% 6.93/1.83 % (291461)Peak memory usage: 109 MB
% 6.93/1.83 % (291461)Instructions burned: 140 (million)
% 6.93/1.83 % (291464)Instruction limit reached!
% 6.93/1.83 % (291464)------------------------------
% 6.93/1.83 % (291464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291464)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291464)Termination reason: Instruction limit
% 6.93/1.83 % (291464)Termination phase: Saturation
% 6.93/1.83 % (291464)Time elapsed: 0.042 s
% 6.93/1.83 % (291464)Peak memory usage: 109 MB
% 6.93/1.83 % (291464)Instructions burned: 115 (million)
% 6.93/1.83 % (291456)------------------------------
% 6.93/1.83 % (291456)------------------------------
% 6.93/1.83 % (291468)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3765689244:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 6.93/1.83 % (291468)Instruction limit reached!
% 6.93/1.83 % (291468)------------------------------
% 6.93/1.83 % (291468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291468)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291468)Termination reason: Instruction limit
% 6.93/1.83 % (291468)Termination phase: Preprocessing 3
% 6.93/1.83 % (291468)Time elapsed: 0.057 s
% 6.93/1.83 % (291468)Peak memory usage: 110 MB
% 6.93/1.83 % (291468)Instructions burned: 131 (million)
% 6.93/1.83 % (291469)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=180416179:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 6.93/1.83 % (291461)------------------------------
% 6.93/1.83 % (291461)------------------------------
% 6.93/1.83 % (291469)Instruction limit reached!
% 6.93/1.83 % (291469)------------------------------
% 6.93/1.83 % (291469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291469)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291469)Termination reason: Instruction limit
% 6.93/1.83 % (291469)Termination phase: Property scanning
% 6.93/1.83 % (291469)Time elapsed: 0.053 s
% 6.93/1.83 % (291469)Peak memory usage: 104 MB
% 6.93/1.83 % (291469)Instructions burned: 114 (million)
% 6.93/1.83 % (291471)lrs+10_1_sil=8000:sp=occurrence:random_seed=1536626465:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 6.93/1.83 % (291471)First to succeed.
% 6.93/1.83 % (291471)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-291435"
% 6.93/1.83 % (291442)Refutation not found, incomplete strategy
% 6.93/1.83 % (291442)------------------------------
% 6.93/1.83 % (291442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.83 % (291442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.83 % (291442)CaDiCaL version: 2.1.3
% 6.93/1.83 % (291442)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.83 % (291442)Time elapsed: 0.857 s
% 6.93/1.83 % (291442)Peak memory usage: 175 MB
% 6.93/1.83 % (291442)Instructions burned: 1298 (million)
% 6.93/1.83 % (291473)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4021247276:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 6.93/1.83 % (291474)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2792289996:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 6.93/1.84 % (291473)Refutation not found, incomplete strategy
% 6.93/1.84 % (291473)------------------------------
% 6.93/1.84 % (291473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.84 % (291473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.84 % (291473)CaDiCaL version: 2.1.3
% 6.93/1.84 % (291473)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.84 % (291473)Time elapsed: 0.058 s
% 6.93/1.84 % (291473)Peak memory usage: 109 MB
% 6.93/1.84 % (291473)Instructions burned: 86 (million)
% 6.93/1.84 % (291441)Also succeeded, but the first one will report.
% 6.93/1.84 % (291471)Refutation found. Thanks to Tanya!
% 6.93/1.84 % SZS status Theorem for theBenchmark
% 6.93/1.84 % SZS output start Proof for theBenchmark
% See solution above
% 8.70/2.04 % (291471)------------------------------
% 8.70/2.04 % (291471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.04 % (291471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.04 % (291471)CaDiCaL version: 2.1.3
% 8.70/2.04 % (291471)Termination reason: Refutation
% 8.70/2.04 % (291471)Time elapsed: 0.079 s
% 8.70/2.04 % (291471)Peak memory usage: 111 MB
% 8.70/2.04 % (291471)Instructions burned: 203 (million)
% 8.70/2.04 % (291471)------------------------------
% 8.70/2.04 % (291471)------------------------------
% 8.70/2.04 % (291435)Success in time 1.425 s
% 8.70/2.04 % Vampire exiting
%------------------------------------------------------------------------------