%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR109+4 : 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 : n017.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:43:08 AM UTC 2026
% Result : Theorem 2.59s 1.37s
% Output : Refutation 4.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 22
% Syntax : Number of formulae : 138 ( 28 unt; 14 def)
% Number of atoms : 462 ( 0 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 526 ( 202 ~; 198 |; 107 &)
% ( 13 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 17 ( 16 usr; 15 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 16 con; 0-0 aty)
% Number of variables : 99 ( 0 sgn 59 !; 40 ?)
% 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(f1291,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__subclass(X1,X2) )
=> s__subclass(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_1294) ).
fof(f5923,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_5997) ).
fof(f5952,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_6026) ).
fof(f6026,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_6100) ).
fof(f7219,axiom,
( s__subclass(s__Reptile,s__Animal)
=> ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f7220,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f7221,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(negated_conjecture,[status(cth)],[f7220]) ).
fof(f7223,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(flattening,[],[f7221]) ).
fof(f7235,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(ennf_transformation,[],[f7219]) ).
fof(f7236,plain,
! [X0,X1,X2] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f1291]) ).
fof(f7237,plain,
! [X0,X1,X2] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f7236]) ).
fof(f7239,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(f7240,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,[],[f7239]) ).
fof(f7241,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f7297,definition,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f7298,plain,
( sP0
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(definition_folding,[],[f7235,f7297]) ).
fof(f7299,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) )
| ~ sP0 ),
inference(nnf_transformation,[],[f7297]) ).
fof(f7300,plain,
( ( s__instance(sK1,s__SetOrClass)
& s__instance(sK2,s__SetOrClass)
& s__instance(sK3,s__SetOrClass)
& s__instance(sK4,s__SetOrClass)
& s__instance(sK5,s__SetOrClass)
& s__instance(sK6,s__SetOrClass)
& s__instance(sK7,s__SetOrClass)
& s__instance(sK8,s__SetOrClass)
& s__instance(sK9,s__SetOrClass)
& s__instance(sK10,s__SetOrClass)
& s__subclass(sK1,sK2)
& s__subclass(sK2,sK3)
& s__subclass(sK3,sK4)
& s__subclass(sK4,sK5)
& s__subclass(sK5,sK6)
& s__subclass(sK6,sK7)
& s__subclass(sK7,sK8)
& s__subclass(sK8,sK9)
& s__subclass(sK9,sK10)
& s__subclass(sK10,s__Reptile)
& s__instance(s__Creature50_1,sK1) )
| ~ sP0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X4,sK5),skolemize(X5,sK6),skolemize(X6,sK7),skolemize(X7,sK8),skolemize(X8,sK9),skolemize(X9,sK10)],[f7299]) ).
fof(f7310,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(cnf_transformation,[],[f7223]) ).
fof(f7311,plain,
( s__instance(s__Creature50_1,sK1)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7312,plain,
( s__subclass(sK10,s__Reptile)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7313,plain,
( s__subclass(sK9,sK10)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7314,plain,
( s__subclass(sK8,sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7315,plain,
( s__subclass(sK7,sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7316,plain,
( s__subclass(sK6,sK7)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7317,plain,
( s__subclass(sK5,sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7318,plain,
( s__subclass(sK4,sK5)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7319,plain,
( s__subclass(sK3,sK4)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7320,plain,
( s__subclass(sK2,sK3)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7321,plain,
( s__subclass(sK1,sK2)
| ~ sP0 ),
inference(cnf_transformation,[],[f7300]) ).
fof(f7332,plain,
( sP0
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[],[f7298]) ).
fof(f7333,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(cnf_transformation,[],[f6026]) ).
fof(f7336,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f7237]) ).
fof(f7338,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,[],[f7240]) ).
fof(f7339,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f7241]) ).
fof(f7340,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f7241]) ).
fof(f7345,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f5952]) ).
fof(f7369,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[],[f5923]) ).
fof(f7436,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,[],[f7338,f7339]) ).
fof(f7437,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f7336,f7339]) ).
fof(f7439,definition,
( spl14_4
<=> s__subclass(s__Reptile,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
fof(f7441,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| spl14_4 ),
inference(avatar_component_clause,[],[f7439]) ).
fof(f7443,definition,
( spl14_5
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f7446,plain,
( ~ spl14_4
| spl14_5 ),
inference(avatar_split_clause,[],[f7332,f7443,f7439]) ).
fof(f7448,definition,
( spl14_6
<=> s__instance(s__Creature50_1,sK1) ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
fof(f7450,plain,
( s__instance(s__Creature50_1,sK1)
| ~ spl14_6 ),
inference(avatar_component_clause,[],[f7448]) ).
fof(f7451,plain,
( ~ spl14_5
| spl14_6 ),
inference(avatar_split_clause,[],[f7311,f7448,f7443]) ).
fof(f7453,definition,
( spl14_7
<=> s__subclass(sK10,s__Reptile) ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
fof(f7455,plain,
( s__subclass(sK10,s__Reptile)
| ~ spl14_7 ),
inference(avatar_component_clause,[],[f7453]) ).
fof(f7456,plain,
( ~ spl14_5
| spl14_7 ),
inference(avatar_split_clause,[],[f7312,f7453,f7443]) ).
fof(f7458,definition,
( spl14_8
<=> s__subclass(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
fof(f7460,plain,
( s__subclass(sK9,sK10)
| ~ spl14_8 ),
inference(avatar_component_clause,[],[f7458]) ).
fof(f7461,plain,
( ~ spl14_5
| spl14_8 ),
inference(avatar_split_clause,[],[f7313,f7458,f7443]) ).
fof(f7463,definition,
( spl14_9
<=> s__subclass(sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
fof(f7465,plain,
( s__subclass(sK8,sK9)
| ~ spl14_9 ),
inference(avatar_component_clause,[],[f7463]) ).
fof(f7466,plain,
( ~ spl14_5
| spl14_9 ),
inference(avatar_split_clause,[],[f7314,f7463,f7443]) ).
fof(f7468,definition,
( spl14_10
<=> s__subclass(sK7,sK8) ),
introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition]) ).
fof(f7470,plain,
( s__subclass(sK7,sK8)
| ~ spl14_10 ),
inference(avatar_component_clause,[],[f7468]) ).
fof(f7471,plain,
( ~ spl14_5
| spl14_10 ),
inference(avatar_split_clause,[],[f7315,f7468,f7443]) ).
fof(f7473,definition,
( spl14_11
<=> s__subclass(sK6,sK7) ),
introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition]) ).
fof(f7475,plain,
( s__subclass(sK6,sK7)
| ~ spl14_11 ),
inference(avatar_component_clause,[],[f7473]) ).
fof(f7476,plain,
( ~ spl14_5
| spl14_11 ),
inference(avatar_split_clause,[],[f7316,f7473,f7443]) ).
fof(f7478,definition,
( spl14_12
<=> s__subclass(sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
fof(f7480,plain,
( s__subclass(sK5,sK6)
| ~ spl14_12 ),
inference(avatar_component_clause,[],[f7478]) ).
fof(f7481,plain,
( ~ spl14_5
| spl14_12 ),
inference(avatar_split_clause,[],[f7317,f7478,f7443]) ).
fof(f7483,definition,
( spl14_13
<=> s__subclass(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
fof(f7485,plain,
( s__subclass(sK4,sK5)
| ~ spl14_13 ),
inference(avatar_component_clause,[],[f7483]) ).
fof(f7486,plain,
( ~ spl14_5
| spl14_13 ),
inference(avatar_split_clause,[],[f7318,f7483,f7443]) ).
fof(f7488,definition,
( spl14_14
<=> s__subclass(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl14_14])],[avatar_definition]) ).
fof(f7490,plain,
( s__subclass(sK3,sK4)
| ~ spl14_14 ),
inference(avatar_component_clause,[],[f7488]) ).
fof(f7491,plain,
( ~ spl14_5
| spl14_14 ),
inference(avatar_split_clause,[],[f7319,f7488,f7443]) ).
fof(f7493,definition,
( spl14_15
<=> s__subclass(sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl14_15])],[avatar_definition]) ).
fof(f7495,plain,
( s__subclass(sK2,sK3)
| ~ spl14_15 ),
inference(avatar_component_clause,[],[f7493]) ).
fof(f7496,plain,
( ~ spl14_5
| spl14_15 ),
inference(avatar_split_clause,[],[f7320,f7493,f7443]) ).
fof(f7498,definition,
( spl14_16
<=> s__subclass(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl14_16])],[avatar_definition]) ).
fof(f7500,plain,
( s__subclass(sK1,sK2)
| ~ spl14_16 ),
inference(avatar_component_clause,[],[f7498]) ).
fof(f7501,plain,
( ~ spl14_5
| spl14_16 ),
inference(avatar_split_clause,[],[f7321,f7498,f7443]) ).
fof(f7556,plain,
! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X2,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f7436,f7340]) ).
fof(f7557,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f7437,f7339]) ).
fof(f7558,plain,
! [X2,X0,X1] :
( ~ s__subclass(X1,X2)
| ~ s__subclass(X0,X1)
| s__subclass(X0,X2) ),
inference(forward_subsumption_resolution,[],[f7557,f7340]) ).
fof(f7608,plain,
! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| s__subclass(X0,s__Animal) ),
inference(resolution,[],[f7558,f7369]) ).
fof(f7609,plain,
! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| s__subclass(X0,s__Vertebrate) ),
inference(resolution,[],[f7558,f7345]) ).
fof(f7972,plain,
s__subclass(s__Reptile,s__Vertebrate),
inference(resolution,[],[f7609,f7333]) ).
fof(f8027,plain,
s__subclass(s__Reptile,s__Animal),
inference(resolution,[],[f7972,f7608]) ).
fof(f8034,plain,
( $false
| spl14_4 ),
inference(forward_subsumption_resolution,[],[f8027,f7441]) ).
fof(f8035,plain,
spl14_4,
inference(avatar_contradiction_clause,[],[f8034]) ).
fof(f8065,plain,
( ! [X0] :
( ~ s__subclass(X0,sK10)
| s__subclass(X0,s__Reptile) )
| ~ spl14_7 ),
inference(resolution,[],[f7455,f7558]) ).
fof(f8081,plain,
( ! [X0] :
( ~ s__subclass(X0,sK9)
| s__subclass(X0,sK10) )
| ~ spl14_8 ),
inference(resolution,[],[f7460,f7558]) ).
fof(f8113,plain,
( ! [X0] :
( ~ s__subclass(X0,sK7)
| s__subclass(X0,sK8) )
| ~ spl14_10 ),
inference(resolution,[],[f7470,f7558]) ).
fof(f8145,plain,
( ! [X0] :
( ~ s__subclass(X0,sK5)
| s__subclass(X0,sK6) )
| ~ spl14_12 ),
inference(resolution,[],[f7480,f7558]) ).
fof(f8178,plain,
( ! [X0] :
( ~ s__instance(X0,sK3)
| s__instance(X0,sK4) )
| ~ spl14_14 ),
inference(resolution,[],[f7490,f7556]) ).
fof(f8194,plain,
( ! [X0] :
( ~ s__instance(X0,sK2)
| s__instance(X0,sK3) )
| ~ spl14_15 ),
inference(resolution,[],[f7495,f7556]) ).
fof(f8210,plain,
( ! [X0] :
( ~ s__instance(X0,sK1)
| s__instance(X0,sK2) )
| ~ spl14_16 ),
inference(resolution,[],[f7500,f7556]) ).
fof(f8426,plain,
( s__subclass(sK8,sK10)
| ~ spl14_8
| ~ spl14_9 ),
inference(resolution,[],[f8081,f7465]) ).
fof(f8428,plain,
( s__subclass(sK8,s__Reptile)
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9 ),
inference(resolution,[],[f8426,f8065]) ).
fof(f8485,plain,
( s__subclass(sK6,sK8)
| ~ spl14_10
| ~ spl14_11 ),
inference(resolution,[],[f8113,f7475]) ).
fof(f8490,plain,
( ! [X0] :
( ~ s__instance(X0,sK6)
| s__instance(X0,sK8) )
| ~ spl14_10
| ~ spl14_11 ),
inference(resolution,[],[f8485,f7556]) ).
fof(f8544,plain,
( s__subclass(sK4,sK6)
| ~ spl14_12
| ~ spl14_13 ),
inference(resolution,[],[f8145,f7485]) ).
fof(f8549,plain,
( ! [X0] :
( ~ s__instance(X0,sK4)
| s__instance(X0,sK6) )
| ~ spl14_12
| ~ spl14_13 ),
inference(resolution,[],[f8544,f7556]) ).
fof(f8663,plain,
( s__instance(s__Creature50_1,sK2)
| ~ spl14_6
| ~ spl14_16 ),
inference(resolution,[],[f8210,f7450]) ).
fof(f8666,plain,
( s__instance(s__Creature50_1,sK3)
| ~ spl14_6
| ~ spl14_15
| ~ spl14_16 ),
inference(resolution,[],[f8663,f8194]) ).
fof(f8836,plain,
( ! [X0] :
( ~ s__instance(X0,sK8)
| s__instance(X0,s__Reptile) )
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9 ),
inference(resolution,[],[f8428,f7556]) ).
fof(f8986,plain,
( s__instance(s__Creature50_1,sK4)
| ~ spl14_6
| ~ spl14_14
| ~ spl14_15
| ~ spl14_16 ),
inference(resolution,[],[f8666,f8178]) ).
fof(f9733,plain,
( s__instance(s__Creature50_1,sK6)
| ~ spl14_6
| ~ spl14_12
| ~ spl14_13
| ~ spl14_14
| ~ spl14_15
| ~ spl14_16 ),
inference(resolution,[],[f8549,f8986]) ).
fof(f10180,plain,
( s__instance(s__Creature50_1,sK8)
| ~ spl14_6
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_14
| ~ spl14_15
| ~ spl14_16 ),
inference(resolution,[],[f9733,f8490]) ).
fof(f10823,plain,
( s__instance(s__Creature50_1,s__Reptile)
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_14
| ~ spl14_15
| ~ spl14_16 ),
inference(resolution,[],[f10180,f8836]) ).
fof(f10826,plain,
( $false
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_14
| ~ spl14_15
| ~ spl14_16 ),
inference(forward_subsumption_resolution,[],[f10823,f7310]) ).
fof(f10827,plain,
( ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_14
| ~ spl14_15
| ~ spl14_16 ),
inference(avatar_contradiction_clause,[],[f10826]) ).
cnf(s3,plain,
( ~ spl14_4
| spl14_5 ),
inference(sat_conversion,[],[f7446]) ).
cnf(s4,plain,
( ~ spl14_5
| spl14_6 ),
inference(sat_conversion,[],[f7451]) ).
cnf(s5,plain,
( ~ spl14_5
| spl14_7 ),
inference(sat_conversion,[],[f7456]) ).
cnf(s6,plain,
( ~ spl14_5
| spl14_8 ),
inference(sat_conversion,[],[f7461]) ).
cnf(s7,plain,
( ~ spl14_5
| spl14_9 ),
inference(sat_conversion,[],[f7466]) ).
cnf(s8,plain,
( ~ spl14_5
| spl14_10 ),
inference(sat_conversion,[],[f7471]) ).
cnf(s9,plain,
( ~ spl14_5
| spl14_11 ),
inference(sat_conversion,[],[f7476]) ).
cnf(s10,plain,
( ~ spl14_5
| spl14_12 ),
inference(sat_conversion,[],[f7481]) ).
cnf(s11,plain,
( ~ spl14_5
| spl14_13 ),
inference(sat_conversion,[],[f7486]) ).
cnf(s12,plain,
( ~ spl14_5
| spl14_14 ),
inference(sat_conversion,[],[f7491]) ).
cnf(s13,plain,
( ~ spl14_5
| spl14_15 ),
inference(sat_conversion,[],[f7496]) ).
cnf(s14,plain,
( ~ spl14_5
| spl14_16 ),
inference(sat_conversion,[],[f7501]) ).
cnf(s43,plain,
spl14_4,
inference(sat_conversion,[],[f8035]) ).
cnf(s153,plain,
( ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_14
| ~ spl14_15
| ~ spl14_16 ),
inference(sat_conversion,[],[f10827]) ).
cnf(s154,plain,
spl14_5,
inference(rat,[],[s3,s43]) ).
cnf(s165,plain,
spl14_16,
inference(rat,[],[s14,s154]) ).
cnf(s166,plain,
spl14_15,
inference(rat,[],[s13,s154]) ).
cnf(s167,plain,
spl14_14,
inference(rat,[],[s12,s154]) ).
cnf(s168,plain,
spl14_13,
inference(rat,[],[s11,s154]) ).
cnf(s169,plain,
spl14_12,
inference(rat,[],[s10,s154]) ).
cnf(s170,plain,
spl14_11,
inference(rat,[],[s9,s154]) ).
cnf(s171,plain,
spl14_10,
inference(rat,[],[s8,s154]) ).
cnf(s172,plain,
spl14_9,
inference(rat,[],[s7,s154]) ).
cnf(s173,plain,
spl14_8,
inference(rat,[],[s6,s154]) ).
cnf(s174,plain,
spl14_7,
inference(rat,[],[s5,s154]) ).
cnf(s175,plain,
spl14_6,
inference(rat,[],[s4,s154]) ).
cnf(s176,plain,
$false,
inference(rat,[],[s153,s165,s166,s167,s168,s169,s170,s171,s172,s173,s174,s175]) ).
fof(f10828,plain,
$false,
inference(avatar_sat_refutation,[],[s176]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 % Computer : n017.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 22:56:07 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running first-order theorem proving
% 0.10/0.24 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
% 2.59/1.37 % (4120974)Detected formulas, will run a generic FOF schedule.
% 2.59/1.37 % (4120983)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2268948728:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 2.59/1.37 % (4120981)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=1242564963:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 2.59/1.37 % (4120985)dis-21_1_sil=8000:lcm=predicate:random_seed=63385931: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)
% 2.59/1.37 % (4120982)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2499980198:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 2.59/1.37 % (4120979)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=3551438253:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 2.59/1.37 % (4120980)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=833374669:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 2.59/1.37 % (4120984)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3487930864:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 2.59/1.37 % (4120983)Instruction limit reached!
% 2.59/1.37 % (4120983)------------------------------
% 2.59/1.37 % (4120983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.59/1.37 % (4120983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/1.37 % (4120983)CaDiCaL version: 2.1.3
% 2.59/1.37 % (4120983)Termination reason: Instruction limit
% 2.59/1.37 % (4120983)Termination phase: Saturation
% 2.59/1.37 % (4120983)Time elapsed: 0.032 s
% 2.59/1.37 % (4120983)Peak memory usage: 94 MB
% 2.59/1.37 % (4120983)Instructions burned: 122 (million)
% 2.59/1.37 % (4120982)Refutation not found, incomplete strategy
% 2.59/1.37 % (4120982)------------------------------
% 2.59/1.37 % (4120982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.59/1.37 % (4120982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/1.37 % (4120982)CaDiCaL version: 2.1.3
% 2.59/1.37 % (4120982)Termination reason: Refutation not found, incomplete strategy
% 2.59/1.37 % (4120982)Time elapsed: 0.021 s
% 2.59/1.37 % (4120982)Peak memory usage: 94 MB
% 2.59/1.37 % (4120982)Instructions burned: 38 (million)
% 2.59/1.37 % (4120985)Instruction limit reached!
% 2.59/1.37 % (4120985)------------------------------
% 2.59/1.37 % (4120985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.59/1.37 % (4120985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/1.37 % (4120985)CaDiCaL version: 2.1.3
% 2.59/1.37 % (4120985)Termination reason: Instruction limit
% 2.59/1.37 % (4120985)Termination phase: Equality proxy
% 2.59/1.37 % (4120985)Time elapsed: 0.071 s
% 2.59/1.37 % (4120985)Peak memory usage: 94 MB
% 2.59/1.37 % (4120985)Instructions burned: 130 (million)
% 2.59/1.37 % (4120984)Instruction limit reached!
% 2.59/1.37 % (4120984)------------------------------
% 2.59/1.37 % (4120984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.59/1.37 % (4120984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/1.37 % (4120984)CaDiCaL version: 2.1.3
% 2.59/1.37 % (4120984)Termination reason: Instruction limit
% 2.59/1.37 % (4120984)Termination phase: Preprocessing 3
% 2.59/1.37 % (4120984)Time elapsed: 0.080 s
% 2.59/1.37 % (4120984)Peak memory usage: 94 MB
% 2.59/1.37 % (4120984)Instructions burned: 140 (million)
% 2.59/1.37 % (4120993)lrs+10_1_sil=8000:sp=occurrence:random_seed=3815136215:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 2.59/1.37 % (4120993)First to succeed.
% 2.59/1.37 % (4120993)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4120974"
% 2.59/1.37 % (4120994)lrs+10_1_sil=32000:urr=on:br=off:random_seed=574166580:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 2.59/1.37 % (4120995)lrs+1011_1_sil=32000:sp=occurrence:random_seed=166956937:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 2.59/1.37 % (4120995)Refutation not found, incomplete strategy
% 2.59/1.37 % (4120995)------------------------------
% 2.59/1.37 % (4120995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.59/1.37 % (4120995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/1.37 % (4120995)CaDiCaL version: 2.1.3
% 2.59/1.37 % (4120995)Termination reason: Refutation not found, incomplete strategy
% 2.59/1.37 % (4120995)Time elapsed: 0.021 s
% 2.59/1.37 % (4120995)Peak memory usage: 95 MB
% 2.59/1.37 % (4120995)Instructions burned: 35 (million)
% 2.59/1.37 % (4120994)Refutation not found, incomplete strategy
% 2.59/1.37 % (4120994)------------------------------
% 2.59/1.37 % (4120994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.59/1.37 % (4120994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/1.37 % (4120994)CaDiCaL version: 2.1.3
% 2.59/1.37 % (4120994)Termination reason: Refutation not found, incomplete strategy
% 2.59/1.37 % (4120994)Time elapsed: 0.040 s
% 2.59/1.37 % (4120994)Peak memory usage: 95 MB
% 2.59/1.37 % (4120994)Instructions burned: 83 (million)
% 2.59/1.37 % (4120982)------------------------------
% 2.59/1.37 % (4120982)------------------------------
% 2.59/1.37 % (4120993)Refutation found. Thanks to Tanya!
% 2.59/1.37 % SZS status Theorem for theBenchmark
% 2.59/1.37 % SZS output start Proof for theBenchmark
% See solution above
% 4.20/1.47 % (4120993)------------------------------
% 4.20/1.47 % (4120993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.47 % (4120993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.47 % (4120993)CaDiCaL version: 2.1.3
% 4.20/1.47 % (4120993)Termination reason: Refutation
% 4.20/1.47 % (4120993)Time elapsed: 0.043 s
% 4.20/1.47 % (4120993)Peak memory usage: 97 MB
% 4.20/1.47 % (4120993)Instructions burned: 114 (million)
% 4.20/1.47 % (4120993)------------------------------
% 4.20/1.47 % (4120993)------------------------------
% 4.20/1.47 % (4120974)Success in time 0.689 s
% 4.20/1.47 % Vampire exiting
%------------------------------------------------------------------------------