%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR093+1 : 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 : n019.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 10.96s 2.17s
% Output : Refutation 11.97s
% 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(f1262,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_1265) ).
fof(f13273,axiom,
s__subclass(s__Human,s__Organism),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMOcache_6056) ).
fof(f14788,axiom,
s__instance(s__Human23_1,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f14789,axiom,
s__instance(s__Human23_2,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f14790,axiom,
s__instance(s__Human23_3,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f14791,axiom,
s__instance(s__Human23_4,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_4) ).
fof(f14792,axiom,
s__instance(s__Human23_5,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_5) ).
fof(f14793,axiom,
s__instance(s__Human23_6,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_6) ).
fof(f14794,axiom,
s__instance(s__Human23_7,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_7) ).
fof(f14795,axiom,
s__instance(s__Human23_8,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_8) ).
fof(f14796,axiom,
s__instance(s__Human23_9,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_9) ).
fof(f14797,axiom,
s__instance(s__Human23_10,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_10) ).
fof(f14798,axiom,
s__instance(s__Human23_11,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_11) ).
fof(f14799,axiom,
s__instance(s__Human23_12,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_12) ).
fof(f14800,axiom,
s__instance(s__Human23_13,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_13) ).
fof(f14801,axiom,
s__instance(s__Human23_14,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_14) ).
fof(f14802,axiom,
s__instance(s__Human23_15,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_15) ).
fof(f14803,axiom,
s__instance(s__Human23_16,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_16) ).
fof(f14804,axiom,
s__ancestor(s__Human23_1,s__Human23_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_17) ).
fof(f14805,axiom,
s__ancestor(s__Human23_2,s__Human23_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_18) ).
fof(f14806,axiom,
s__ancestor(s__Human23_3,s__Human23_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_19) ).
fof(f14807,axiom,
s__ancestor(s__Human23_4,s__Human23_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_20) ).
fof(f14808,axiom,
s__ancestor(s__Human23_5,s__Human23_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_21) ).
fof(f14809,axiom,
s__ancestor(s__Human23_6,s__Human23_7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_22) ).
fof(f14810,axiom,
s__ancestor(s__Human23_7,s__Human23_8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_23) ).
fof(f14811,axiom,
s__ancestor(s__Human23_8,s__Human23_9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_24) ).
fof(f14812,axiom,
s__ancestor(s__Human23_9,s__Human23_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_25) ).
fof(f14813,axiom,
s__ancestor(s__Human23_10,s__Human23_11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_26) ).
fof(f14814,axiom,
s__ancestor(s__Human23_11,s__Human23_12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_27) ).
fof(f14815,axiom,
s__ancestor(s__Human23_12,s__Human23_13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_28) ).
fof(f14816,axiom,
s__ancestor(s__Human23_13,s__Human23_14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_29) ).
fof(f14817,axiom,
s__ancestor(s__Human23_14,s__Human23_15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_30) ).
fof(f14818,axiom,
s__ancestor(s__Human23_14,s__Human23_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_31) ).
fof(f14819,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) ).
fof(f14820,negated_conjecture,
~ ( s__ancestor(s__Human23_1,s__Human23_15)
& s__ancestor(s__Human23_1,s__Human23_16) ),
inference(negated_conjecture,[status(cth)],[f14819]) ).
fof(f14895,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_15)
| ~ s__ancestor(s__Human23_1,s__Human23_16) ),
inference(ennf_transformation,[],[f14820]) ).
fof(f14902,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,[],[f1262]) ).
fof(f14903,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,[],[f14902]) ).
fof(f14947,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(f14948,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,[],[f14947]) ).
fof(f14949,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f15177,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_15)
| ~ s__ancestor(s__Human23_1,s__Human23_16) ),
inference(cnf_transformation,[],[f14895]) ).
fof(f15181,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,[],[f14903]) ).
fof(f15184,plain,
s__ancestor(s__Human23_1,s__Human23_2),
inference(cnf_transformation,[],[f14804]) ).
fof(f15185,plain,
s__instance(s__Human23_1,s__Human),
inference(cnf_transformation,[],[f14788]) ).
fof(f15186,plain,
s__ancestor(s__Human23_14,s__Human23_15),
inference(cnf_transformation,[],[f14817]) ).
fof(f15187,plain,
s__instance(s__Human23_15,s__Human),
inference(cnf_transformation,[],[f14802]) ).
fof(f15188,plain,
s__ancestor(s__Human23_14,s__Human23_16),
inference(cnf_transformation,[],[f14818]) ).
fof(f15189,plain,
s__instance(s__Human23_16,s__Human),
inference(cnf_transformation,[],[f14803]) ).
fof(f15222,plain,
s__ancestor(s__Human23_2,s__Human23_3),
inference(cnf_transformation,[],[f14805]) ).
fof(f15223,plain,
s__instance(s__Human23_2,s__Human),
inference(cnf_transformation,[],[f14789]) ).
fof(f15226,plain,
s__subclass(s__Human,s__Organism),
inference(cnf_transformation,[],[f13273]) ).
fof(f15231,plain,
s__ancestor(s__Human23_13,s__Human23_14),
inference(cnf_transformation,[],[f14816]) ).
fof(f15232,plain,
s__instance(s__Human23_14,s__Human),
inference(cnf_transformation,[],[f14801]) ).
fof(f15235,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,[],[f14948]) ).
fof(f15236,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f14949]) ).
fof(f15237,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f14949]) ).
fof(f15272,plain,
s__ancestor(s__Human23_3,s__Human23_4),
inference(cnf_transformation,[],[f14806]) ).
fof(f15273,plain,
s__instance(s__Human23_3,s__Human),
inference(cnf_transformation,[],[f14790]) ).
fof(f15278,plain,
s__ancestor(s__Human23_12,s__Human23_13),
inference(cnf_transformation,[],[f14815]) ).
fof(f15279,plain,
s__instance(s__Human23_13,s__Human),
inference(cnf_transformation,[],[f14800]) ).
fof(f15360,plain,
s__ancestor(s__Human23_4,s__Human23_5),
inference(cnf_transformation,[],[f14807]) ).
fof(f15361,plain,
s__instance(s__Human23_4,s__Human),
inference(cnf_transformation,[],[f14791]) ).
fof(f15362,plain,
s__ancestor(s__Human23_11,s__Human23_12),
inference(cnf_transformation,[],[f14814]) ).
fof(f15363,plain,
s__instance(s__Human23_12,s__Human),
inference(cnf_transformation,[],[f14799]) ).
fof(f15380,plain,
s__ancestor(s__Human23_5,s__Human23_6),
inference(cnf_transformation,[],[f14808]) ).
fof(f15381,plain,
s__instance(s__Human23_5,s__Human),
inference(cnf_transformation,[],[f14792]) ).
fof(f15382,plain,
s__ancestor(s__Human23_10,s__Human23_11),
inference(cnf_transformation,[],[f14813]) ).
fof(f15383,plain,
s__instance(s__Human23_11,s__Human),
inference(cnf_transformation,[],[f14798]) ).
fof(f15395,plain,
s__ancestor(s__Human23_6,s__Human23_7),
inference(cnf_transformation,[],[f14809]) ).
fof(f15396,plain,
s__instance(s__Human23_6,s__Human),
inference(cnf_transformation,[],[f14793]) ).
fof(f15397,plain,
s__ancestor(s__Human23_9,s__Human23_10),
inference(cnf_transformation,[],[f14812]) ).
fof(f15398,plain,
s__instance(s__Human23_10,s__Human),
inference(cnf_transformation,[],[f14797]) ).
fof(f15415,plain,
s__ancestor(s__Human23_7,s__Human23_8),
inference(cnf_transformation,[],[f14810]) ).
fof(f15416,plain,
s__instance(s__Human23_7,s__Human),
inference(cnf_transformation,[],[f14794]) ).
fof(f15417,plain,
s__ancestor(s__Human23_8,s__Human23_9),
inference(cnf_transformation,[],[f14811]) ).
fof(f15418,plain,
s__instance(s__Human23_9,s__Human),
inference(cnf_transformation,[],[f14796]) ).
fof(f15454,plain,
s__instance(s__Human23_8,s__Human),
inference(cnf_transformation,[],[f14795]) ).
fof(f15980,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,[],[f15235,f15236]) ).
fof(f15988,definition,
( spl13_3
<=> s__ancestor(s__Human23_1,s__Human23_16) ),
introduced(definition,[new_symbols(definition,[spl13_3])],[avatar_definition]) ).
fof(f15992,definition,
( spl13_4
<=> s__ancestor(s__Human23_1,s__Human23_15) ),
introduced(definition,[new_symbols(definition,[spl13_4])],[avatar_definition]) ).
fof(f15994,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_15)
| spl13_4 ),
inference(avatar_component_clause,[],[f15992]) ).
fof(f15995,plain,
( ~ spl13_3
| ~ spl13_4 ),
inference(avatar_split_clause,[],[f15177,f15992,f15988]) ).
fof(f15999,plain,
! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X2,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f15980,f15237]) ).
fof(f16672,plain,
! [X0] :
( ~ s__instance(X0,s__Human)
| s__instance(X0,s__Organism) ),
inference(resolution,[],[f15999,f15226]) ).
fof(f19608,definition,
( spl13_447
<=> s__instance(s__Human23_14,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_447])],[avatar_definition]) ).
fof(f19609,plain,
( s__instance(s__Human23_14,s__Organism)
| ~ spl13_447 ),
inference(avatar_component_clause,[],[f19608]) ).
fof(f19610,plain,
( ~ s__instance(s__Human23_14,s__Organism)
| spl13_447 ),
inference(avatar_component_clause,[],[f19608]) ).
fof(f19612,definition,
( spl13_448
<=> s__instance(s__Human23_16,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_448])],[avatar_definition]) ).
fof(f19613,plain,
( s__instance(s__Human23_16,s__Organism)
| ~ spl13_448 ),
inference(avatar_component_clause,[],[f19612]) ).
fof(f19621,definition,
( spl13_450
<=> s__instance(s__Human23_15,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_450])],[avatar_definition]) ).
fof(f19622,plain,
( s__instance(s__Human23_15,s__Organism)
| ~ spl13_450 ),
inference(avatar_component_clause,[],[f19621]) ).
fof(f19630,definition,
( spl13_452
<=> s__instance(s__Human23_13,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_452])],[avatar_definition]) ).
fof(f19631,plain,
( s__instance(s__Human23_13,s__Organism)
| ~ spl13_452 ),
inference(avatar_component_clause,[],[f19630]) ).
fof(f19639,definition,
( spl13_454
<=> s__instance(s__Human23_12,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_454])],[avatar_definition]) ).
fof(f19640,plain,
( s__instance(s__Human23_12,s__Organism)
| ~ spl13_454 ),
inference(avatar_component_clause,[],[f19639]) ).
fof(f19641,plain,
( ~ s__instance(s__Human23_12,s__Organism)
| spl13_454 ),
inference(avatar_component_clause,[],[f19639]) ).
fof(f19648,definition,
( spl13_456
<=> s__instance(s__Human23_11,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_456])],[avatar_definition]) ).
fof(f19649,plain,
( s__instance(s__Human23_11,s__Organism)
| ~ spl13_456 ),
inference(avatar_component_clause,[],[f19648]) ).
fof(f19657,definition,
( spl13_458
<=> s__instance(s__Human23_10,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_458])],[avatar_definition]) ).
fof(f19658,plain,
( s__instance(s__Human23_10,s__Organism)
| ~ spl13_458 ),
inference(avatar_component_clause,[],[f19657]) ).
fof(f19659,plain,
( ~ s__instance(s__Human23_10,s__Organism)
| spl13_458 ),
inference(avatar_component_clause,[],[f19657]) ).
fof(f19666,definition,
( spl13_460
<=> s__instance(s__Human23_9,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_460])],[avatar_definition]) ).
fof(f19667,plain,
( s__instance(s__Human23_9,s__Organism)
| ~ spl13_460 ),
inference(avatar_component_clause,[],[f19666]) ).
fof(f19668,plain,
( ~ s__instance(s__Human23_9,s__Organism)
| spl13_460 ),
inference(avatar_component_clause,[],[f19666]) ).
fof(f19675,definition,
( spl13_462
<=> s__instance(s__Human23_8,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_462])],[avatar_definition]) ).
fof(f19676,plain,
( s__instance(s__Human23_8,s__Organism)
| ~ spl13_462 ),
inference(avatar_component_clause,[],[f19675]) ).
fof(f19684,definition,
( spl13_464
<=> s__instance(s__Human23_7,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_464])],[avatar_definition]) ).
fof(f19685,plain,
( s__instance(s__Human23_7,s__Organism)
| ~ spl13_464 ),
inference(avatar_component_clause,[],[f19684]) ).
fof(f19686,plain,
( ~ s__instance(s__Human23_7,s__Organism)
| spl13_464 ),
inference(avatar_component_clause,[],[f19684]) ).
fof(f19693,definition,
( spl13_466
<=> s__instance(s__Human23_6,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_466])],[avatar_definition]) ).
fof(f19694,plain,
( s__instance(s__Human23_6,s__Organism)
| ~ spl13_466 ),
inference(avatar_component_clause,[],[f19693]) ).
fof(f19695,plain,
( ~ s__instance(s__Human23_6,s__Organism)
| spl13_466 ),
inference(avatar_component_clause,[],[f19693]) ).
fof(f19702,definition,
( spl13_468
<=> s__instance(s__Human23_5,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_468])],[avatar_definition]) ).
fof(f19703,plain,
( s__instance(s__Human23_5,s__Organism)
| ~ spl13_468 ),
inference(avatar_component_clause,[],[f19702]) ).
fof(f19711,definition,
( spl13_470
<=> s__instance(s__Human23_4,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_470])],[avatar_definition]) ).
fof(f19712,plain,
( s__instance(s__Human23_4,s__Organism)
| ~ spl13_470 ),
inference(avatar_component_clause,[],[f19711]) ).
fof(f19713,plain,
( ~ s__instance(s__Human23_4,s__Organism)
| spl13_470 ),
inference(avatar_component_clause,[],[f19711]) ).
fof(f19720,definition,
( spl13_472
<=> s__instance(s__Human23_3,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_472])],[avatar_definition]) ).
fof(f19721,plain,
( s__instance(s__Human23_3,s__Organism)
| ~ spl13_472 ),
inference(avatar_component_clause,[],[f19720]) ).
fof(f19729,definition,
( spl13_474
<=> s__instance(s__Human23_2,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_474])],[avatar_definition]) ).
fof(f19730,plain,
( s__instance(s__Human23_2,s__Organism)
| ~ spl13_474 ),
inference(avatar_component_clause,[],[f19729]) ).
fof(f19731,plain,
( ~ s__instance(s__Human23_2,s__Organism)
| spl13_474 ),
inference(avatar_component_clause,[],[f19729]) ).
fof(f19738,definition,
( spl13_476
<=> s__instance(s__Human23_1,s__Organism) ),
introduced(definition,[new_symbols(definition,[spl13_476])],[avatar_definition]) ).
fof(f19739,plain,
( s__instance(s__Human23_1,s__Organism)
| ~ spl13_476 ),
inference(avatar_component_clause,[],[f19738]) ).
fof(f20636,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,[],[f15181,f15222]) ).
fof(f20637,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,[],[f15181,f15272]) ).
fof(f20638,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,[],[f15181,f15360]) ).
fof(f20639,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,[],[f15181,f15380]) ).
fof(f20640,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,[],[f15181,f15395]) ).
fof(f20641,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,[],[f15181,f15415]) ).
fof(f20642,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,[],[f15181,f15417]) ).
fof(f20643,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,[],[f15181,f15397]) ).
fof(f20644,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,[],[f15181,f15382]) ).
fof(f20645,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,[],[f15181,f15362]) ).
fof(f20646,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,[],[f15181,f15278]) ).
fof(f20647,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,[],[f15181,f15231]) ).
fof(f20648,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,[],[f15181,f15186]) ).
fof(f20649,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,[],[f15181,f15188]) ).
fof(f22357,plain,
s__instance(s__Human23_1,s__Organism),
inference(resolution,[],[f16672,f15185]) ).
fof(f22358,plain,
s__instance(s__Human23_2,s__Organism),
inference(resolution,[],[f16672,f15223]) ).
fof(f22359,plain,
s__instance(s__Human23_3,s__Organism),
inference(resolution,[],[f16672,f15273]) ).
fof(f22360,plain,
s__instance(s__Human23_4,s__Organism),
inference(resolution,[],[f16672,f15361]) ).
fof(f22361,plain,
s__instance(s__Human23_5,s__Organism),
inference(resolution,[],[f16672,f15381]) ).
fof(f22362,plain,
s__instance(s__Human23_6,s__Organism),
inference(resolution,[],[f16672,f15396]) ).
fof(f22363,plain,
s__instance(s__Human23_7,s__Organism),
inference(resolution,[],[f16672,f15416]) ).
fof(f22364,plain,
s__instance(s__Human23_8,s__Organism),
inference(resolution,[],[f16672,f15454]) ).
fof(f22365,plain,
s__instance(s__Human23_9,s__Organism),
inference(resolution,[],[f16672,f15418]) ).
fof(f22366,plain,
s__instance(s__Human23_10,s__Organism),
inference(resolution,[],[f16672,f15398]) ).
fof(f22367,plain,
s__instance(s__Human23_11,s__Organism),
inference(resolution,[],[f16672,f15383]) ).
fof(f22368,plain,
s__instance(s__Human23_12,s__Organism),
inference(resolution,[],[f16672,f15363]) ).
fof(f22369,plain,
s__instance(s__Human23_13,s__Organism),
inference(resolution,[],[f16672,f15279]) ).
fof(f22370,plain,
s__instance(s__Human23_14,s__Organism),
inference(resolution,[],[f16672,f15232]) ).
fof(f22371,plain,
s__instance(s__Human23_15,s__Organism),
inference(resolution,[],[f16672,f15187]) ).
fof(f22372,plain,
s__instance(s__Human23_16,s__Organism),
inference(resolution,[],[f16672,f15189]) ).
fof(f22375,plain,
spl13_448,
inference(avatar_split_clause,[],[f22372,f19612]) ).
fof(f22376,plain,
spl13_450,
inference(avatar_split_clause,[],[f22371,f19621]) ).
fof(f22377,plain,
( $false
| spl13_447 ),
inference(forward_subsumption_resolution,[],[f22370,f19610]) ).
fof(f22378,plain,
spl13_447,
inference(avatar_contradiction_clause,[],[f22377]) ).
fof(f22379,plain,
spl13_452,
inference(avatar_split_clause,[],[f22369,f19630]) ).
fof(f22380,plain,
( $false
| spl13_454 ),
inference(forward_subsumption_resolution,[],[f22368,f19641]) ).
fof(f22381,plain,
spl13_454,
inference(avatar_contradiction_clause,[],[f22380]) ).
fof(f22382,plain,
spl13_456,
inference(avatar_split_clause,[],[f22367,f19648]) ).
fof(f22383,plain,
( $false
| spl13_458 ),
inference(forward_subsumption_resolution,[],[f22366,f19659]) ).
fof(f22384,plain,
spl13_458,
inference(avatar_contradiction_clause,[],[f22383]) ).
fof(f22385,plain,
( $false
| spl13_460 ),
inference(forward_subsumption_resolution,[],[f22365,f19668]) ).
fof(f22386,plain,
spl13_460,
inference(avatar_contradiction_clause,[],[f22385]) ).
fof(f22387,plain,
spl13_462,
inference(avatar_split_clause,[],[f22364,f19675]) ).
fof(f22388,plain,
( $false
| spl13_464 ),
inference(forward_subsumption_resolution,[],[f22363,f19686]) ).
fof(f22389,plain,
spl13_464,
inference(avatar_contradiction_clause,[],[f22388]) ).
fof(f22390,plain,
( $false
| spl13_466 ),
inference(forward_subsumption_resolution,[],[f22362,f19695]) ).
fof(f22391,plain,
spl13_466,
inference(avatar_contradiction_clause,[],[f22390]) ).
fof(f22392,plain,
spl13_468,
inference(avatar_split_clause,[],[f22361,f19702]) ).
fof(f22393,plain,
( $false
| spl13_470 ),
inference(forward_subsumption_resolution,[],[f22360,f19713]) ).
fof(f22394,plain,
spl13_470,
inference(avatar_contradiction_clause,[],[f22393]) ).
fof(f22395,plain,
spl13_472,
inference(avatar_split_clause,[],[f22359,f19720]) ).
fof(f22396,plain,
( $false
| spl13_474 ),
inference(forward_subsumption_resolution,[],[f22358,f19731]) ).
fof(f22397,plain,
spl13_474,
inference(avatar_contradiction_clause,[],[f22396]) ).
fof(f22398,plain,
spl13_476,
inference(avatar_split_clause,[],[f22357,f19738]) ).
fof(f22399,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) )
| ~ spl13_472 ),
inference(forward_subsumption_resolution,[],[f20636,f19721]) ).
fof(f22401,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) )
| ~ spl13_468 ),
inference(forward_subsumption_resolution,[],[f20638,f19703]) ).
fof(f22402,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) )
| ~ spl13_470 ),
inference(forward_subsumption_resolution,[],[f20637,f19712]) ).
fof(f22403,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) )
| ~ spl13_466 ),
inference(forward_subsumption_resolution,[],[f20639,f19694]) ).
fof(f22404,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) )
| ~ spl13_462 ),
inference(forward_subsumption_resolution,[],[f20641,f19676]) ).
fof(f22405,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) )
| ~ spl13_464 ),
inference(forward_subsumption_resolution,[],[f20640,f19685]) ).
fof(f22406,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) )
| ~ spl13_460 ),
inference(forward_subsumption_resolution,[],[f20642,f19667]) ).
fof(f22407,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) )
| ~ spl13_456 ),
inference(forward_subsumption_resolution,[],[f20644,f19649]) ).
fof(f22408,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) )
| ~ spl13_458 ),
inference(forward_subsumption_resolution,[],[f20643,f19658]) ).
fof(f22409,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) )
| ~ spl13_452 ),
inference(forward_subsumption_resolution,[],[f20646,f19631]) ).
fof(f22410,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) )
| ~ spl13_454 ),
inference(forward_subsumption_resolution,[],[f20645,f19640]) ).
fof(f22411,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) )
| ~ spl13_448 ),
inference(forward_subsumption_resolution,[],[f20649,f19613]) ).
fof(f22412,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) )
| ~ spl13_450 ),
inference(forward_subsumption_resolution,[],[f20648,f19622]) ).
fof(f22413,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) )
| ~ spl13_447 ),
inference(forward_subsumption_resolution,[],[f20647,f19609]) ).
fof(f22414,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_2)
| s__ancestor(X0,s__Human23_3)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_472
| ~ spl13_474 ),
inference(forward_subsumption_resolution,[],[f22399,f19730]) ).
fof(f22416,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_4)
| s__ancestor(X0,s__Human23_5)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_468
| ~ spl13_470 ),
inference(forward_subsumption_resolution,[],[f22401,f19712]) ).
fof(f22417,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_3)
| s__ancestor(X0,s__Human23_4)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_470
| ~ spl13_472 ),
inference(forward_subsumption_resolution,[],[f22402,f19721]) ).
fof(f22418,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_5)
| s__ancestor(X0,s__Human23_6)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_466
| ~ spl13_468 ),
inference(forward_subsumption_resolution,[],[f22403,f19703]) ).
fof(f22419,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_7)
| s__ancestor(X0,s__Human23_8)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_462
| ~ spl13_464 ),
inference(forward_subsumption_resolution,[],[f22404,f19685]) ).
fof(f22420,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_6)
| s__ancestor(X0,s__Human23_7)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_464
| ~ spl13_466 ),
inference(forward_subsumption_resolution,[],[f22405,f19694]) ).
fof(f22421,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_8)
| s__ancestor(X0,s__Human23_9)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_460
| ~ spl13_462 ),
inference(forward_subsumption_resolution,[],[f22406,f19676]) ).
fof(f22422,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_10)
| s__ancestor(X0,s__Human23_11)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_456
| ~ spl13_458 ),
inference(forward_subsumption_resolution,[],[f22407,f19658]) ).
fof(f22423,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_9)
| s__ancestor(X0,s__Human23_10)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_458
| ~ spl13_460 ),
inference(forward_subsumption_resolution,[],[f22408,f19667]) ).
fof(f22424,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_12)
| s__ancestor(X0,s__Human23_13)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_452
| ~ spl13_454 ),
inference(forward_subsumption_resolution,[],[f22409,f19640]) ).
fof(f22425,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_11)
| s__ancestor(X0,s__Human23_12)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_454
| ~ spl13_456 ),
inference(forward_subsumption_resolution,[],[f22410,f19649]) ).
fof(f22426,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_14)
| s__ancestor(X0,s__Human23_16)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_447
| ~ spl13_448 ),
inference(forward_subsumption_resolution,[],[f22411,f19609]) ).
fof(f22427,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_14)
| s__ancestor(X0,s__Human23_15)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_447
| ~ spl13_450 ),
inference(forward_subsumption_resolution,[],[f22412,f19609]) ).
fof(f22428,plain,
( ! [X0] :
( ~ s__ancestor(X0,s__Human23_13)
| s__ancestor(X0,s__Human23_14)
| ~ s__instance(X0,s__Organism) )
| ~ spl13_447
| ~ spl13_452 ),
inference(forward_subsumption_resolution,[],[f22413,f19631]) ).
fof(f25098,plain,
( s__ancestor(s__Human23_1,s__Human23_3)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_472
| ~ spl13_474 ),
inference(resolution,[],[f22414,f15184]) ).
fof(f25099,plain,
( s__ancestor(s__Human23_1,s__Human23_3)
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f25098,f19739]) ).
fof(f25115,plain,
( s__ancestor(s__Human23_1,s__Human23_4)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f22417,f25099]) ).
fof(f25118,plain,
( s__ancestor(s__Human23_1,s__Human23_4)
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f25115,f19739]) ).
fof(f25243,plain,
( s__ancestor(s__Human23_1,s__Human23_5)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f25118,f22416]) ).
fof(f25248,plain,
( s__ancestor(s__Human23_1,s__Human23_5)
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f25243,f19739]) ).
fof(f25440,plain,
( s__ancestor(s__Human23_1,s__Human23_6)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f25248,f22418]) ).
fof(f25445,plain,
( s__ancestor(s__Human23_1,s__Human23_6)
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f25440,f19739]) ).
fof(f25707,plain,
( s__ancestor(s__Human23_1,s__Human23_7)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f25445,f22420]) ).
fof(f25712,plain,
( s__ancestor(s__Human23_1,s__Human23_7)
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f25707,f19739]) ).
fof(f25923,plain,
( s__ancestor(s__Human23_1,s__Human23_8)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f25712,f22419]) ).
fof(f25928,plain,
( s__ancestor(s__Human23_1,s__Human23_8)
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f25923,f19739]) ).
fof(f26101,plain,
( s__ancestor(s__Human23_1,s__Human23_9)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f25928,f22421]) ).
fof(f26106,plain,
( s__ancestor(s__Human23_1,s__Human23_9)
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f26101,f19739]) ).
fof(f28391,plain,
( s__ancestor(s__Human23_1,s__Human23_10)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f26106,f22423]) ).
fof(f28396,plain,
( s__ancestor(s__Human23_1,s__Human23_10)
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f28391,f19739]) ).
fof(f28517,plain,
( s__ancestor(s__Human23_1,s__Human23_11)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f28396,f22422]) ).
fof(f28522,plain,
( s__ancestor(s__Human23_1,s__Human23_11)
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f28517,f19739]) ).
fof(f28623,plain,
( s__ancestor(s__Human23_1,s__Human23_12)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f28522,f22425]) ).
fof(f28628,plain,
( s__ancestor(s__Human23_1,s__Human23_12)
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f28623,f19739]) ).
fof(f28823,plain,
( s__ancestor(s__Human23_1,s__Human23_13)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f28628,f22424]) ).
fof(f28828,plain,
( s__ancestor(s__Human23_1,s__Human23_13)
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f28823,f19739]) ).
fof(f28981,plain,
( s__ancestor(s__Human23_1,s__Human23_14)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_447
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f28828,f22428]) ).
fof(f28986,plain,
( s__ancestor(s__Human23_1,s__Human23_14)
| ~ spl13_447
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f28981,f19739]) ).
fof(f29107,plain,
( s__ancestor(s__Human23_1,s__Human23_15)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_447
| ~ spl13_450
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f28986,f22427]) ).
fof(f29108,plain,
( s__ancestor(s__Human23_1,s__Human23_16)
| ~ s__instance(s__Human23_1,s__Organism)
| ~ spl13_447
| ~ spl13_448
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(resolution,[],[f28986,f22426]) ).
fof(f29113,plain,
( s__ancestor(s__Human23_1,s__Human23_16)
| ~ spl13_447
| ~ spl13_448
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f29108,f19739]) ).
fof(f29114,plain,
( ~ s__instance(s__Human23_1,s__Organism)
| spl13_4
| ~ spl13_447
| ~ spl13_450
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f29107,f15994]) ).
fof(f29117,plain,
( spl13_3
| ~ spl13_447
| ~ spl13_448
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(avatar_split_clause,[],[f29113,f19738,f19729,f19720,f19711,f19702,f19693,f19684,f19675,f19666,f19657,f19648,f19639,f19630,f19612,f19608,f15988]) ).
fof(f29118,plain,
( $false
| spl13_4
| ~ spl13_447
| ~ spl13_450
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(forward_subsumption_resolution,[],[f29114,f19739]) ).
fof(f29119,plain,
( spl13_4
| ~ spl13_447
| ~ spl13_450
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(avatar_contradiction_clause,[],[f29118]) ).
cnf(s2,plain,
( ~ spl13_3
| ~ spl13_4 ),
inference(sat_conversion,[],[f15995]) ).
cnf(s326,plain,
spl13_448,
inference(sat_conversion,[],[f22375]) ).
cnf(s327,plain,
spl13_450,
inference(sat_conversion,[],[f22376]) ).
cnf(s328,plain,
spl13_447,
inference(sat_conversion,[],[f22378]) ).
cnf(s329,plain,
spl13_452,
inference(sat_conversion,[],[f22379]) ).
cnf(s330,plain,
spl13_454,
inference(sat_conversion,[],[f22381]) ).
cnf(s331,plain,
spl13_456,
inference(sat_conversion,[],[f22382]) ).
cnf(s332,plain,
spl13_458,
inference(sat_conversion,[],[f22384]) ).
cnf(s333,plain,
spl13_460,
inference(sat_conversion,[],[f22386]) ).
cnf(s334,plain,
spl13_462,
inference(sat_conversion,[],[f22387]) ).
cnf(s335,plain,
spl13_464,
inference(sat_conversion,[],[f22389]) ).
cnf(s336,plain,
spl13_466,
inference(sat_conversion,[],[f22391]) ).
cnf(s337,plain,
spl13_468,
inference(sat_conversion,[],[f22392]) ).
cnf(s338,plain,
spl13_470,
inference(sat_conversion,[],[f22394]) ).
cnf(s339,plain,
spl13_472,
inference(sat_conversion,[],[f22395]) ).
cnf(s340,plain,
spl13_474,
inference(sat_conversion,[],[f22397]) ).
cnf(s341,plain,
spl13_476,
inference(sat_conversion,[],[f22398]) ).
cnf(s521,plain,
( spl13_3
| ~ spl13_447
| ~ spl13_448
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(sat_conversion,[],[f29117]) ).
cnf(s522,plain,
( spl13_4
| ~ spl13_447
| ~ spl13_450
| ~ spl13_452
| ~ spl13_454
| ~ spl13_456
| ~ spl13_458
| ~ spl13_460
| ~ spl13_462
| ~ spl13_464
| ~ spl13_466
| ~ spl13_468
| ~ spl13_470
| ~ spl13_472
| ~ spl13_474
| ~ spl13_476 ),
inference(sat_conversion,[],[f29119]) ).
cnf(s526,plain,
spl13_4,
inference(rat,[],[s522,s341,s340,s339,s338,s337,s336,s335,s334,s333,s332,s331,s330,s329,s328,s327]) ).
cnf(s527,plain,
spl13_3,
inference(rat,[],[s521,s341,s340,s339,s338,s337,s336,s335,s334,s333,s332,s331,s330,s329,s328,s326]) ).
cnf(s543,plain,
$false,
inference(rat,[],[s2,s526,s527]) ).
fof(f29120,plain,
$false,
inference(avatar_sat_refutation,[],[s543]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR093+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n019.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 22:42:33 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 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
% 10.96/2.14 % (355633)Detected formulas, will run a generic FOF schedule.
% 10.96/2.14 % (355644)dis-21_1_sil=8000:lcm=predicate:random_seed=1743524309:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 10.96/2.14 % (355640)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=1617046319:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 10.96/2.14 % (355643)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3994474779:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 10.96/2.14 % (355638)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=1145563518:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 10.96/2.14 % (355641)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1986514534:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 10.96/2.14 % (355639)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=4055788011:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 10.96/2.14 % (355642)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=366537496:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 10.96/2.14 % (355644)Instruction limit reached!
% 10.96/2.14 % (355644)------------------------------
% 10.96/2.14 % (355644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.14 % (355644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.14 % (355644)CaDiCaL version: 2.1.3
% 10.96/2.14 % (355644)Termination reason: Instruction limit
% 10.96/2.14 % (355644)Termination phase: Preprocessing 3
% 10.96/2.14 % (355644)Time elapsed: 0.044 s
% 10.96/2.14 % (355644)Peak memory usage: 96 MB
% 10.96/2.14 % (355644)Instructions burned: 129 (million)
% 10.96/2.14 % (355641)Refutation not found, incomplete strategy
% 10.96/2.14 % (355641)------------------------------
% 10.96/2.14 % (355641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.14 % (355641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.14 % (355641)CaDiCaL version: 2.1.3
% 10.96/2.14 % (355641)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.14 % (355641)Time elapsed: 0.032 s
% 10.96/2.14 % (355641)Peak memory usage: 97 MB
% 10.96/2.14 % (355641)Instructions burned: 61 (million)
% 10.96/2.14 % (355642)Instruction limit reached!
% 10.96/2.14 % (355642)------------------------------
% 10.96/2.14 % (355642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.14 % (355642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.14 % (355642)CaDiCaL version: 2.1.3
% 10.96/2.14 % (355642)Termination reason: Instruction limit
% 10.96/2.14 % (355642)Termination phase: Saturation
% 10.96/2.14 % (355642)Time elapsed: 0.064 s
% 10.96/2.14 % (355642)Peak memory usage: 97 MB
% 10.96/2.14 % (355642)Instructions burned: 120 (million)
% 10.96/2.14 % (355643)Instruction limit reached!
% 10.96/2.14 % (355643)------------------------------
% 10.96/2.14 % (355643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.14 % (355643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.14 % (355643)CaDiCaL version: 2.1.3
% 10.96/2.14 % (355643)Termination reason: Instruction limit
% 10.96/2.14 % (355643)Termination phase: SInE selection
% 10.96/2.14 % (355643)Time elapsed: 0.073 s
% 10.96/2.14 % (355643)Peak memory usage: 94 MB
% 10.96/2.14 % (355643)Instructions burned: 140 (million)
% 10.96/2.14 % (355652)lrs+10_1_sil=8000:sp=occurrence:random_seed=3531828128:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.96/2.14 % (355652)Instruction limit reached!
% 10.96/2.14 % (355652)------------------------------
% 10.96/2.14 % (355652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.14 % (355652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.14 % (355652)CaDiCaL version: 2.1.3
% 10.96/2.14 % (355652)Termination reason: Instruction limit
% 10.96/2.14 % (355652)Termination phase: Saturation
% 10.96/2.14 % (355652)Time elapsed: 0.086 s
% 10.96/2.14 % (355652)Peak memory usage: 100 MB
% 10.96/2.14 % (355652)Instructions burned: 285 (million)
% 10.96/2.14 % (355653)lrs+10_1_sil=32000:urr=on:br=off:random_seed=75988758:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.96/2.17 % (355654)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1205556912:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 10.96/2.17 % (355654)Refutation not found, incomplete strategy
% 10.96/2.17 % (355654)------------------------------
% 10.96/2.17 % (355654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355654)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355654)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.17 % (355654)Time elapsed: 0.032 s
% 10.96/2.17 % (355654)Peak memory usage: 97 MB
% 10.96/2.17 % (355654)Instructions burned: 58 (million)
% 10.96/2.17 % (355641)------------------------------
% 10.96/2.17 % (355641)------------------------------
% 10.96/2.17 % (355653)Refutation not found, incomplete strategy
% 10.96/2.17 % (355653)------------------------------
% 10.96/2.17 % (355653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355653)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355653)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.17 % (355653)Time elapsed: 0.057 s
% 10.96/2.17 % (355653)Peak memory usage: 97 MB
% 10.96/2.17 % (355653)Instructions burned: 127 (million)
% 10.96/2.17 % (355656)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=3002488958:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 10.96/2.17 % (355656)Instruction limit reached!
% 10.96/2.17 % (355656)------------------------------
% 10.96/2.17 % (355656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355656)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355656)Termination reason: Instruction limit
% 10.96/2.17 % (355656)Termination phase: Clausification
% 10.96/2.17 % (355656)Time elapsed: 0.070 s
% 10.96/2.17 % (355656)Peak memory usage: 98 MB
% 10.96/2.17 % (355656)Instructions burned: 251 (million)
% 10.96/2.17 % (355659)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=997172783:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 10.96/2.17 % (355654)------------------------------
% 10.96/2.17 % (355654)------------------------------
% 10.96/2.17 % (355659)Refutation not found, incomplete strategy
% 10.96/2.17 % (355659)------------------------------
% 10.96/2.17 % (355659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355659)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355659)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.17 % (355659)Time elapsed: 0.046 s
% 10.96/2.17 % (355659)Peak memory usage: 98 MB
% 10.96/2.17 % (355659)Instructions burned: 91 (million)
% 10.96/2.17 % (355653)------------------------------
% 10.96/2.17 % (355653)------------------------------
% 10.96/2.17 % (355661)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2892250371:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 10.96/2.17 % (355663)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4269501362:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 10.96/2.17 % (355664)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1422982584:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 10.96/2.17 % (355663)Instruction limit reached!
% 10.96/2.17 % (355663)------------------------------
% 10.96/2.17 % (355663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355663)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355663)Termination reason: Instruction limit
% 10.96/2.17 % (355663)Termination phase: Saturation
% 10.96/2.17 % (355663)Time elapsed: 0.062 s
% 10.96/2.17 % (355663)Peak memory usage: 97 MB
% 10.96/2.17 % (355663)Instructions burned: 114 (million)
% 10.96/2.17 % (355640)Refutation not found, incomplete strategy
% 10.96/2.17 % (355640)------------------------------
% 10.96/2.17 % (355640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355640)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355640)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.17 % (355640)Time elapsed: 0.759 s
% 10.96/2.17 % (355640)Peak memory usage: 150 MB
% 10.96/2.17 % (355640)Instructions burned: 1172 (million)
% 10.96/2.17 % (355659)------------------------------
% 10.96/2.17 % (355659)------------------------------
% 10.96/2.17 % (355664)Instruction limit reached!
% 10.96/2.17 % (355664)------------------------------
% 10.96/2.17 % (355664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355664)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355664)Termination reason: Instruction limit
% 10.96/2.17 % (355664)Termination phase: Property scanning
% 10.96/2.17 % (355664)Time elapsed: 0.078 s
% 10.96/2.17 % (355664)Peak memory usage: 100 MB
% 10.96/2.17 % (355664)Instructions burned: 128 (million)
% 10.96/2.17 % (355668)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4243845532:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 10.96/2.17 % (355669)lrs+10_1_sil=8000:sp=occurrence:random_seed=530455306:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 10.96/2.17 % (355670)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3008793682:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 10.96/2.17 % (355668)Instruction limit reached!
% 10.96/2.17 % (355668)------------------------------
% 10.96/2.17 % (355668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355668)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355668)Termination reason: Instruction limit
% 10.96/2.17 % (355668)Termination phase: Property scanning
% 10.96/2.17 % (355668)Time elapsed: 0.052 s
% 10.96/2.17 % (355668)Peak memory usage: 93 MB
% 10.96/2.17 % (355668)Instructions burned: 115 (million)
% 10.96/2.17 % (355670)Refutation not found, incomplete strategy
% 10.96/2.17 % (355670)------------------------------
% 10.96/2.17 % (355670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355670)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355670)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.17 % (355670)Time elapsed: 0.041 s
% 10.96/2.17 % (355670)Peak memory usage: 98 MB
% 10.96/2.17 % (355670)Instructions burned: 80 (million)
% 10.96/2.17 % (355640)------------------------------
% 10.96/2.17 % (355640)------------------------------
% 10.96/2.17 % (355674)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2369759232:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 10.96/2.17 % (355669)First to succeed.
% 10.96/2.17 % (355669)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-355633"
% 10.96/2.17 % (355675)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4012604919:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 10.96/2.17 % (355670)------------------------------
% 10.96/2.17 % (355670)------------------------------
% 10.96/2.17 % (355675)Instruction limit reached!
% 10.96/2.17 % (355675)------------------------------
% 10.96/2.17 % (355675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355675)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355675)Termination reason: Instruction limit
% 10.96/2.17 % (355675)Termination phase: Saturation
% 10.96/2.17 % (355675)Time elapsed: 0.072 s
% 10.96/2.17 % (355675)Peak memory usage: 98 MB
% 10.96/2.17 % (355675)Instructions burned: 136 (million)
% 10.96/2.17 % (355678)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2407030083:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 10.96/2.17 % (355661)Instruction limit reached!
% 10.96/2.17 % (355661)------------------------------
% 10.96/2.17 % (355661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.17 % (355661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.17 % (355661)CaDiCaL version: 2.1.3
% 10.96/2.17 % (355661)Termination reason: Instruction limit
% 10.96/2.17 % (355661)Termination phase: Saturation
% 10.96/2.17 % (355661)Time elapsed: 0.859 s
% 10.96/2.17 % (355661)Peak memory usage: 232 MB
% 10.96/2.17 % (355661)Instructions burned: 2352 (million)
% 10.96/2.17 % (355679)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3681278796:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 10.96/2.17 % (355669)Refutation found. Thanks to Tanya!
% 10.96/2.17 % SZS status Theorem for theBenchmark
% 10.96/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 11.97/2.37 % (355669)------------------------------
% 11.97/2.37 % (355669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.97/2.37 % (355669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.97/2.37 % (355669)CaDiCaL version: 2.1.3
% 11.97/2.37 % (355669)Termination reason: Refutation
% 11.97/2.37 % (355669)Time elapsed: 0.243 s
% 11.97/2.37 % (355669)Peak memory usage: 104 MB
% 11.97/2.37 % (355669)Instructions burned: 414 (million)
% 11.97/2.37 % (355669)------------------------------
% 11.97/2.37 % (355669)------------------------------
% 11.97/2.37 % (355633)Success in time 1.748 s
% 11.97/2.37 % Vampire exiting
%------------------------------------------------------------------------------