%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR109+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 10.89s 4.93s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 20
% Syntax : Number of formulae : 128 ( 22 unt; 14 def)
% Number of atoms : 454 ( 0 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 531 ( 205 ~; 200 |; 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 : 14 ( 14 usr; 14 con; 0-0 aty)
% Number of variables : 97 ( 0 sgn 57 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26456,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_26635) ).
fof(f26457,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/sandbox2/benchmark/theBenchmark.p',kb_SUMO_26636) ).
fof(f28279,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/sandbox2/benchmark/theBenchmark.p',kb_SUMO_28461) ).
fof(f115457,axiom,
s__subclass(s__Reptile,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_59871) ).
fof(f145103,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/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f145104,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f145105,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(negated_conjecture,[status(cth)],[f145104]) ).
fof(f145106,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(flattening,[],[f145105]) ).
fof(f145109,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,[],[f145103]) ).
fof(f145110,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,[],[f28279]) ).
fof(f145111,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,[],[f145110]) ).
fof(f145113,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,[],[f26457]) ).
fof(f145114,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,[],[f145113]) ).
fof(f145115,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f145201,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(f145202,plain,
( sP0
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(definition_folding,[],[f145109,f145201]) ).
fof(f145203,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,[],[f145201]) ).
fof(f145204,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)],[f145203]) ).
fof(f145214,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(cnf_transformation,[],[f145106]) ).
fof(f145220,plain,
s__subclass(s__Reptile,s__Animal),
inference(cnf_transformation,[],[f115457]) ).
fof(f145227,plain,
( s__instance(s__Creature50_1,sK1)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145228,plain,
( s__subclass(sK10,s__Reptile)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145229,plain,
( s__subclass(sK9,sK10)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145230,plain,
( s__subclass(sK8,sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145231,plain,
( s__subclass(sK7,sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145232,plain,
( s__subclass(sK6,sK7)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145233,plain,
( s__subclass(sK5,sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145234,plain,
( s__subclass(sK4,sK5)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145235,plain,
( s__subclass(sK3,sK4)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145236,plain,
( s__subclass(sK2,sK3)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145237,plain,
( s__subclass(sK1,sK2)
| ~ sP0 ),
inference(cnf_transformation,[],[f145204]) ).
fof(f145248,plain,
( sP0
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[],[f145202]) ).
fof(f145326,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,[],[f145111]) ).
fof(f145328,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,[],[f145114]) ).
fof(f145329,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f145115]) ).
fof(f145330,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f145115]) ).
fof(f145603,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,[],[f145328,f145329]) ).
fof(f145604,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,[],[f145326,f145329]) ).
fof(f145606,definition,
( spl14_1
<=> s__subclass(s__Reptile,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
fof(f145610,definition,
( spl14_2
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition]) ).
fof(f145613,plain,
( ~ spl14_1
| spl14_2 ),
inference(avatar_split_clause,[],[f145248,f145610,f145606]) ).
fof(f145615,definition,
( spl14_3
<=> s__instance(s__Creature50_1,sK1) ),
introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition]) ).
fof(f145617,plain,
( s__instance(s__Creature50_1,sK1)
| ~ spl14_3 ),
inference(avatar_component_clause,[],[f145615]) ).
fof(f145618,plain,
( ~ spl14_2
| spl14_3 ),
inference(avatar_split_clause,[],[f145227,f145615,f145610]) ).
fof(f145620,definition,
( spl14_4
<=> s__subclass(sK10,s__Reptile) ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
fof(f145622,plain,
( s__subclass(sK10,s__Reptile)
| ~ spl14_4 ),
inference(avatar_component_clause,[],[f145620]) ).
fof(f145623,plain,
( ~ spl14_2
| spl14_4 ),
inference(avatar_split_clause,[],[f145228,f145620,f145610]) ).
fof(f145625,definition,
( spl14_5
<=> s__subclass(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f145627,plain,
( s__subclass(sK9,sK10)
| ~ spl14_5 ),
inference(avatar_component_clause,[],[f145625]) ).
fof(f145628,plain,
( ~ spl14_2
| spl14_5 ),
inference(avatar_split_clause,[],[f145229,f145625,f145610]) ).
fof(f145630,definition,
( spl14_6
<=> s__subclass(sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
fof(f145632,plain,
( s__subclass(sK8,sK9)
| ~ spl14_6 ),
inference(avatar_component_clause,[],[f145630]) ).
fof(f145633,plain,
( ~ spl14_2
| spl14_6 ),
inference(avatar_split_clause,[],[f145230,f145630,f145610]) ).
fof(f145635,definition,
( spl14_7
<=> s__subclass(sK7,sK8) ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
fof(f145637,plain,
( s__subclass(sK7,sK8)
| ~ spl14_7 ),
inference(avatar_component_clause,[],[f145635]) ).
fof(f145638,plain,
( ~ spl14_2
| spl14_7 ),
inference(avatar_split_clause,[],[f145231,f145635,f145610]) ).
fof(f145640,definition,
( spl14_8
<=> s__subclass(sK6,sK7) ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
fof(f145642,plain,
( s__subclass(sK6,sK7)
| ~ spl14_8 ),
inference(avatar_component_clause,[],[f145640]) ).
fof(f145643,plain,
( ~ spl14_2
| spl14_8 ),
inference(avatar_split_clause,[],[f145232,f145640,f145610]) ).
fof(f145645,definition,
( spl14_9
<=> s__subclass(sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
fof(f145647,plain,
( s__subclass(sK5,sK6)
| ~ spl14_9 ),
inference(avatar_component_clause,[],[f145645]) ).
fof(f145648,plain,
( ~ spl14_2
| spl14_9 ),
inference(avatar_split_clause,[],[f145233,f145645,f145610]) ).
fof(f145650,definition,
( spl14_10
<=> s__subclass(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition]) ).
fof(f145652,plain,
( s__subclass(sK4,sK5)
| ~ spl14_10 ),
inference(avatar_component_clause,[],[f145650]) ).
fof(f145653,plain,
( ~ spl14_2
| spl14_10 ),
inference(avatar_split_clause,[],[f145234,f145650,f145610]) ).
fof(f145655,definition,
( spl14_11
<=> s__subclass(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition]) ).
fof(f145657,plain,
( s__subclass(sK3,sK4)
| ~ spl14_11 ),
inference(avatar_component_clause,[],[f145655]) ).
fof(f145658,plain,
( ~ spl14_2
| spl14_11 ),
inference(avatar_split_clause,[],[f145235,f145655,f145610]) ).
fof(f145660,definition,
( spl14_12
<=> s__subclass(sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
fof(f145662,plain,
( s__subclass(sK2,sK3)
| ~ spl14_12 ),
inference(avatar_component_clause,[],[f145660]) ).
fof(f145663,plain,
( ~ spl14_2
| spl14_12 ),
inference(avatar_split_clause,[],[f145236,f145660,f145610]) ).
fof(f145665,definition,
( spl14_13
<=> s__subclass(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
fof(f145667,plain,
( s__subclass(sK1,sK2)
| ~ spl14_13 ),
inference(avatar_component_clause,[],[f145665]) ).
fof(f145668,plain,
( ~ spl14_2
| spl14_13 ),
inference(avatar_split_clause,[],[f145237,f145665,f145610]) ).
fof(f145719,plain,
spl14_1,
inference(avatar_split_clause,[],[f145220,f145606]) ).
fof(f145721,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f145603,f145330]) ).
fof(f145722,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,[],[f145604,f145329]) ).
fof(f145723,plain,
! [X2,X0,X1] :
( ~ s__subclass(X1,X2)
| ~ s__subclass(X0,X1)
| s__subclass(X0,X2) ),
inference(forward_subsumption_resolution,[],[f145722,f145330]) ).
fof(f146269,plain,
( ! [X0] :
( ~ s__subclass(sK1,X0)
| s__instance(s__Creature50_1,X0) )
| ~ spl14_3 ),
inference(resolution,[],[f145721,f145617]) ).
fof(f146501,plain,
( ! [X0] :
( ~ s__subclass(X0,sK3)
| s__subclass(X0,sK4) )
| ~ spl14_11 ),
inference(resolution,[],[f145723,f145657]) ).
fof(f146503,plain,
( ! [X0] :
( ~ s__subclass(X0,sK4)
| s__subclass(X0,sK5) )
| ~ spl14_10 ),
inference(resolution,[],[f145723,f145652]) ).
fof(f146505,plain,
( ! [X0] :
( ~ s__subclass(X0,sK5)
| s__subclass(X0,sK6) )
| ~ spl14_9 ),
inference(resolution,[],[f145723,f145647]) ).
fof(f146507,plain,
( ! [X0] :
( ~ s__subclass(X0,sK6)
| s__subclass(X0,sK7) )
| ~ spl14_8 ),
inference(resolution,[],[f145723,f145642]) ).
fof(f146509,plain,
( ! [X0] :
( ~ s__subclass(X0,sK7)
| s__subclass(X0,sK8) )
| ~ spl14_7 ),
inference(resolution,[],[f145723,f145637]) ).
fof(f146511,plain,
( ! [X0] :
( ~ s__subclass(X0,sK8)
| s__subclass(X0,sK9) )
| ~ spl14_6 ),
inference(resolution,[],[f145723,f145632]) ).
fof(f146515,plain,
( ! [X0] :
( ~ s__subclass(X0,sK10)
| s__subclass(X0,s__Reptile) )
| ~ spl14_4 ),
inference(resolution,[],[f145723,f145622]) ).
fof(f147548,plain,
( s__instance(s__Creature50_1,sK2)
| ~ spl14_3
| ~ spl14_13 ),
inference(resolution,[],[f146269,f145667]) ).
fof(f147583,plain,
( ! [X0] :
( ~ s__subclass(sK2,X0)
| s__instance(s__Creature50_1,X0) )
| ~ spl14_3
| ~ spl14_13 ),
inference(resolution,[],[f147548,f145721]) ).
fof(f148652,plain,
( s__subclass(sK2,sK4)
| ~ spl14_11
| ~ spl14_12 ),
inference(resolution,[],[f146501,f145662]) ).
fof(f148661,plain,
( s__subclass(sK2,sK5)
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12 ),
inference(resolution,[],[f148652,f146503]) ).
fof(f148695,plain,
( s__subclass(sK9,s__Reptile)
| ~ spl14_4
| ~ spl14_5 ),
inference(resolution,[],[f146515,f145627]) ).
fof(f148714,plain,
( ! [X0] :
( ~ s__subclass(X0,sK9)
| s__subclass(X0,s__Reptile) )
| ~ spl14_4
| ~ spl14_5 ),
inference(resolution,[],[f148695,f145723]) ).
fof(f148726,plain,
( s__subclass(sK2,sK6)
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12 ),
inference(resolution,[],[f148661,f146505]) ).
fof(f148901,plain,
( s__subclass(sK2,sK7)
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12 ),
inference(resolution,[],[f148726,f146507]) ).
fof(f150504,plain,
( s__subclass(sK2,sK8)
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12 ),
inference(resolution,[],[f148901,f146509]) ).
fof(f154946,plain,
( s__subclass(sK2,sK9)
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12 ),
inference(resolution,[],[f150504,f146511]) ).
fof(f155441,plain,
( s__subclass(sK2,s__Reptile)
| ~ spl14_4
| ~ spl14_5
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12 ),
inference(resolution,[],[f154946,f148714]) ).
fof(f156379,plain,
( s__instance(s__Creature50_1,s__Reptile)
| ~ spl14_3
| ~ spl14_4
| ~ spl14_5
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13 ),
inference(resolution,[],[f155441,f147583]) ).
fof(f156408,plain,
( $false
| ~ spl14_3
| ~ spl14_4
| ~ spl14_5
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13 ),
inference(forward_subsumption_resolution,[],[f156379,f145214]) ).
fof(f156409,plain,
( ~ spl14_3
| ~ spl14_4
| ~ spl14_5
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13 ),
inference(avatar_contradiction_clause,[],[f156408]) ).
cnf(s1,plain,
( ~ spl14_1
| spl14_2 ),
inference(sat_conversion,[],[f145613]) ).
cnf(s2,plain,
( ~ spl14_2
| spl14_3 ),
inference(sat_conversion,[],[f145618]) ).
cnf(s3,plain,
( ~ spl14_2
| spl14_4 ),
inference(sat_conversion,[],[f145623]) ).
cnf(s4,plain,
( ~ spl14_2
| spl14_5 ),
inference(sat_conversion,[],[f145628]) ).
cnf(s5,plain,
( ~ spl14_2
| spl14_6 ),
inference(sat_conversion,[],[f145633]) ).
cnf(s6,plain,
( ~ spl14_2
| spl14_7 ),
inference(sat_conversion,[],[f145638]) ).
cnf(s7,plain,
( ~ spl14_2
| spl14_8 ),
inference(sat_conversion,[],[f145643]) ).
cnf(s8,plain,
( ~ spl14_2
| spl14_9 ),
inference(sat_conversion,[],[f145648]) ).
cnf(s9,plain,
( ~ spl14_2
| spl14_10 ),
inference(sat_conversion,[],[f145653]) ).
cnf(s10,plain,
( ~ spl14_2
| spl14_11 ),
inference(sat_conversion,[],[f145658]) ).
cnf(s11,plain,
( ~ spl14_2
| spl14_12 ),
inference(sat_conversion,[],[f145663]) ).
cnf(s12,plain,
( ~ spl14_2
| spl14_13 ),
inference(sat_conversion,[],[f145668]) ).
cnf(s23,plain,
spl14_1,
inference(sat_conversion,[],[f145719]) ).
cnf(s418,plain,
( ~ spl14_3
| ~ spl14_4
| ~ spl14_5
| ~ spl14_6
| ~ spl14_7
| ~ spl14_8
| ~ spl14_9
| ~ spl14_10
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13 ),
inference(sat_conversion,[],[f156409]) ).
cnf(s419,plain,
spl14_2,
inference(rat,[],[s1,s23]) ).
cnf(s430,plain,
spl14_13,
inference(rat,[],[s12,s419]) ).
cnf(s431,plain,
spl14_12,
inference(rat,[],[s11,s419]) ).
cnf(s432,plain,
spl14_11,
inference(rat,[],[s10,s419]) ).
cnf(s433,plain,
spl14_10,
inference(rat,[],[s9,s419]) ).
cnf(s434,plain,
spl14_9,
inference(rat,[],[s8,s419]) ).
cnf(s435,plain,
spl14_8,
inference(rat,[],[s7,s419]) ).
cnf(s436,plain,
spl14_7,
inference(rat,[],[s6,s419]) ).
cnf(s437,plain,
spl14_6,
inference(rat,[],[s5,s419]) ).
cnf(s438,plain,
spl14_5,
inference(rat,[],[s4,s419]) ).
cnf(s439,plain,
spl14_4,
inference(rat,[],[s3,s419]) ).
cnf(s440,plain,
spl14_3,
inference(rat,[],[s2,s419]) ).
cnf(s441,plain,
$false,
inference(rat,[],[s418,s430,s431,s432,s433,s434,s435,s436,s437,s438,s439,s440]) ).
fof(f156410,plain,
$false,
inference(avatar_sat_refutation,[],[s441]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 % Computer : n007.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:58:26 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running first-order theorem proving
% 0.10/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.89/4.93 % (2946363)Detected formulas, will run a generic FOF schedule.
% 10.89/4.93 % (2946372)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1821541873:i=119:av=off:ss=axioms_2971 on theBenchmark for (2971ds/119Mi)
% 10.89/4.93 % (2946368)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=2605299800:i=141193_2971 on theBenchmark for (2971ds/141193Mi)
% 10.89/4.93 % (2946369)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=3774105973:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2971 on theBenchmark for (2971ds/134677Mi)
% 10.89/4.93 % (2946370)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=3197196864:i=141695:sd=1:nm=32:gsp=on:ss=included_2971 on theBenchmark for (2971ds/141695Mi)
% 10.89/4.93 % (2946372)Instruction limit reached!
% 10.89/4.93 % (2946372)------------------------------
% 10.89/4.93 % (2946372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946372)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946372)Termination reason: Instruction limit
% 10.89/4.93 % (2946372)Termination phase: SInE selection
% 10.89/4.93 % (2946372)Time elapsed: 0.042 s
% 10.89/4.93 % (2946372)Peak memory usage: 165 MB
% 10.89/4.93 % (2946372)Instructions burned: 119 (million)
% 10.89/4.93 % (2946373)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4217795863:s2a=on:i=139:gtg=position_2971 on theBenchmark for (2971ds/139Mi)
% 10.89/4.93 % (2946374)dis-21_1_sil=8000:lcm=predicate:random_seed=3250642411:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2971 on theBenchmark for (2971ds/129Mi)
% 10.89/4.93 % (2946371)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1933214003:i=109:sd=1:ins=1:gsp=on:ss=axioms_2971 on theBenchmark for (2971ds/109Mi)
% 10.89/4.93 % (2946371)Instruction limit reached!
% 10.89/4.93 % (2946371)------------------------------
% 10.89/4.93 % (2946371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946371)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946371)Termination reason: Instruction limit
% 10.89/4.93 % (2946371)Termination phase: SInE selection
% 10.89/4.93 % (2946371)Time elapsed: 0.063 s
% 10.89/4.93 % (2946371)Peak memory usage: 164 MB
% 10.89/4.93 % (2946371)Instructions burned: 110 (million)
% 10.89/4.93 % (2946374)Instruction limit reached!
% 10.89/4.93 % (2946374)------------------------------
% 10.89/4.93 % (2946374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946374)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946374)Termination reason: Instruction limit
% 10.89/4.93 % (2946374)Termination phase: SInE selection
% 10.89/4.93 % (2946374)Time elapsed: 0.071 s
% 10.89/4.93 % (2946374)Peak memory usage: 164 MB
% 10.89/4.93 % (2946374)Instructions burned: 130 (million)
% 10.89/4.93 % (2946373)Instruction limit reached!
% 10.89/4.93 % (2946373)------------------------------
% 10.89/4.93 % (2946373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946373)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946373)Termination reason: Instruction limit
% 10.89/4.93 % (2946373)Termination phase: Property scanning
% 10.89/4.93 % (2946373)Time elapsed: 0.076 s
% 10.89/4.93 % (2946373)Peak memory usage: 165 MB
% 10.89/4.93 % (2946373)Instructions burned: 141 (million)
% 10.89/4.93 % (2946382)lrs+10_1_sil=8000:sp=occurrence:random_seed=3029115937:i=285:sd=3:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/285Mi)
% 10.89/4.93 % (2946382)Instruction limit reached!
% 10.89/4.93 % (2946382)------------------------------
% 10.89/4.93 % (2946382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946382)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946382)Termination reason: Instruction limit
% 10.89/4.93 % (2946382)Termination phase: SInE selection
% 10.89/4.93 % (2946382)Time elapsed: 0.091 s
% 10.89/4.93 % (2946382)Peak memory usage: 165 MB
% 10.89/4.93 % (2946382)Instructions burned: 286 (million)
% 10.89/4.93 % (2946384)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4210675194:i=325:sd=1:ss=axioms:sgt=32_2968 on theBenchmark for (2968ds/325Mi)
% 10.89/4.93 % (2946383)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1296817619:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/157Mi)
% 10.89/4.93 % (2946385)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=1156627659:s2a=on:i=248:s2at=1.23:gtg=position_2968 on theBenchmark for (2968ds/248Mi)
% 10.89/4.93 % (2946383)Instruction limit reached!
% 10.89/4.93 % (2946383)------------------------------
% 10.89/4.93 % (2946383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946383)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946383)Termination reason: Instruction limit
% 10.89/4.93 % (2946383)Termination phase: Property scanning
% 10.89/4.93 % (2946383)Time elapsed: 0.088 s
% 10.89/4.93 % (2946383)Peak memory usage: 165 MB
% 10.89/4.93 % (2946383)Instructions burned: 159 (million)
% 10.89/4.93 % (2946387)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=921696435:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2967 on theBenchmark for (2967ds/294Mi)
% 10.89/4.93 % (2946385)Instruction limit reached!
% 10.89/4.93 % (2946385)------------------------------
% 10.89/4.93 % (2946385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946385)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946385)Termination reason: Instruction limit
% 10.89/4.93 % (2946385)Termination phase: Property scanning
% 10.89/4.93 % (2946385)Time elapsed: 0.120 s
% 10.89/4.93 % (2946385)Peak memory usage: 165 MB
% 10.89/4.93 % (2946385)Instructions burned: 248 (million)
% 10.89/4.93 % (2946384)Instruction limit reached!
% 10.89/4.93 % (2946384)------------------------------
% 10.89/4.93 % (2946384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946384)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946384)Termination reason: Instruction limit
% 10.89/4.93 % (2946384)Termination phase: SInE selection
% 10.89/4.93 % (2946384)Time elapsed: 0.176 s
% 10.89/4.93 % (2946384)Peak memory usage: 164 MB
% 10.89/4.93 % (2946384)Instructions burned: 327 (million)
% 10.89/4.93 % (2946387)Instruction limit reached!
% 10.89/4.93 % (2946387)------------------------------
% 10.89/4.93 % (2946387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946387)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946387)Termination reason: Instruction limit
% 10.89/4.93 % (2946387)Termination phase: SInE selection
% 10.89/4.93 % (2946387)Time elapsed: 0.088 s
% 10.89/4.93 % (2946387)Peak memory usage: 165 MB
% 10.89/4.93 % (2946387)Instructions burned: 294 (million)
% 10.89/4.93 % (2946391)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3037759743:i=2350_2966 on theBenchmark for (2966ds/2350Mi)
% 10.89/4.93 % (2946393)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=189161191:cts=off:i=113:fsr=off:ss=included:sgt=4_2965 on theBenchmark for (2965ds/113Mi)
% 10.89/4.93 % (2946394)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3570578734:i=127:av=off:fsr=off:sup=off_2965 on theBenchmark for (2965ds/127Mi)
% 10.89/4.93 % (2946395)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3727777565:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2965 on theBenchmark for (2965ds/114Mi)
% 10.89/4.93 % (2946395)Instruction limit reached!
% 10.89/4.93 % (2946395)------------------------------
% 10.89/4.93 % (2946395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946395)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946395)Termination reason: Instruction limit
% 10.89/4.93 % (2946395)Termination phase: Property scanning
% 10.89/4.93 % (2946395)Time elapsed: 0.037 s
% 10.89/4.93 % (2946395)Peak memory usage: 165 MB
% 10.89/4.93 % (2946395)Instructions burned: 117 (million)
% 10.89/4.93 % (2946393)Instruction limit reached!
% 10.89/4.93 % (2946393)------------------------------
% 10.89/4.93 % (2946393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946393)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946393)Termination reason: Instruction limit
% 10.89/4.93 % (2946393)Termination phase: SInE selection
% 10.89/4.93 % (2946393)Time elapsed: 0.070 s
% 10.89/4.93 % (2946393)Peak memory usage: 165 MB
% 10.89/4.93 % (2946393)Instructions burned: 114 (million)
% 10.89/4.93 % (2946394)Instruction limit reached!
% 10.89/4.93 % (2946394)------------------------------
% 10.89/4.93 % (2946394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946394)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946394)Termination reason: Instruction limit
% 10.89/4.93 % (2946394)Termination phase: Preprocessing 1
% 10.89/4.93 % (2946394)Time elapsed: 0.084 s
% 10.89/4.93 % (2946394)Peak memory usage: 165 MB
% 10.89/4.93 % (2946394)Instructions burned: 127 (million)
% 10.89/4.93 % (2946400)lrs+10_1_sil=8000:sp=occurrence:random_seed=3418591843:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2963 on theBenchmark for (2963ds/907Mi)
% 10.89/4.93 % (2946401)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2005708886:i=437:sd=1:aac=none:ss=included_2963 on theBenchmark for (2963ds/437Mi)
% 10.89/4.93 % (2946402)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2176089888:i=5202:ss=axioms:sgt=16_2963 on theBenchmark for (2963ds/5202Mi)
% 10.89/4.93 % (2946400)First to succeed.
% 10.89/4.93 % (2946400)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2946363"
% 10.89/4.93 % (2946401)Instruction limit reached!
% 10.89/4.93 % (2946401)------------------------------
% 10.89/4.93 % (2946401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/4.93 % (2946401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/4.93 % (2946401)CaDiCaL version: 2.1.3
% 10.89/4.93 % (2946401)Termination reason: Instruction limit
% 10.89/4.93 % (2946401)Termination phase: Saturation
% 10.89/4.93 % (2946401)Time elapsed: 0.260 s
% 10.89/4.93 % (2946401)Peak memory usage: 169 MB
% 10.89/4.93 % (2946401)Instructions burned: 438 (million)
% 10.89/4.93 % (2946400)Refutation found. Thanks to Tanya!
% 10.89/4.93 % SZS status Theorem for theBenchmark
% 10.89/4.93 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/5.20 % (2946400)------------------------------
% 0.22/5.20 % (2946400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.22/5.20 % (2946400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/5.20 % (2946400)CaDiCaL version: 2.1.3
% 0.22/5.20 % (2946400)Termination reason: Refutation
% 0.22/5.20 % (2946400)Time elapsed: 0.268 s
% 0.22/5.20 % (2946400)Peak memory usage: 175 MB
% 0.22/5.20 % (2946400)Instructions burned: 799 (million)
% 0.22/5.20 % (2946400)------------------------------
% 0.22/5.20 % (2946400)------------------------------
% 0.22/5.20 % (2946363)Success in time 4.247 s
% 0.22/5.20 % Vampire exiting
%------------------------------------------------------------------------------