%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR109+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:20 AM UTC 2026
% Result : Theorem 7.64s 1.84s
% Output : Refutation 7.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 17
% Syntax : Number of formulae : 117 ( 22 unt; 12 def)
% Number of atoms : 390 ( 0 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 490 ( 217 ~; 213 |; 44 &)
% ( 12 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 13 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 14 con; 0-0 aty)
% Number of variables : 63 ( 0 sgn 43 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f14492,axiom,
s__subclass(s__Reptile,s__Animal),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+3.ax',kb_SUMOcache_7275) ).
fof(f14789,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(f14790,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f14791,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(negated_conjecture,[status(cth)],[f14790]) ).
fof(f14795,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(flattening,[],[f14791]) ).
fof(f14886,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f14887,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(f14888,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,[],[f14887]) ).
fof(f19980,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,[],[f14789]) ).
fof(f21285,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f14886]) ).
fof(f21286,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f14886]) ).
fof(f21287,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(cnf_transformation,[],[f14888]) ).
fof(f36825,plain,
s__subclass(s__Reptile,s__Animal),
inference(cnf_transformation,[],[f14492]) ).
fof(f37122,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__instance(s__Creature50_1,sK478) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37123,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK487,s__Reptile) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37124,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK486,sK487) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37125,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK485,sK486) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37126,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK484,sK485) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37127,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK483,sK484) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37128,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK482,sK483) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37129,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK481,sK482) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37130,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK480,sK481) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37131,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK479,sK480) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37132,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK478,sK479) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f37143,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(cnf_transformation,[],[f14795]) ).
fof(f37539,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| ~ s__instance(X0,s__SetOrClass) ),
inference(consistent_polarity_flipping,[],[f21286]) ).
fof(f37540,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| ~ s__instance(X1,s__SetOrClass) ),
inference(consistent_polarity_flipping,[],[f21285]) ).
fof(f37541,plain,
! [X2,X0,X1] :
( s__instance(X0,s__SetOrClass)
| s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(consistent_polarity_flipping,[],[f21287]) ).
fof(f47159,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| ~ s__instance(s__Creature50_1,sK478) ),
inference(consistent_polarity_flipping,[],[f37122]) ).
fof(f47160,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(consistent_polarity_flipping,[],[f37143]) ).
fof(f47170,definition,
( spl488_1
<=> s__instance(s__Creature50_1,sK478) ),
introduced(definition,[new_symbols(definition,[spl488_1])],[avatar_definition]) ).
fof(f47172,plain,
( ~ s__instance(s__Creature50_1,sK478)
| spl488_1 ),
inference(avatar_component_clause,[],[f47170]) ).
fof(f47174,definition,
( spl488_2
<=> s__subclass(s__Reptile,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl488_2])],[avatar_definition]) ).
fof(f47177,plain,
( ~ spl488_1
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f47159,f47174,f47170]) ).
fof(f47179,definition,
( spl488_3
<=> s__subclass(sK487,s__Reptile) ),
introduced(definition,[new_symbols(definition,[spl488_3])],[avatar_definition]) ).
fof(f47181,plain,
( s__subclass(sK487,s__Reptile)
| ~ spl488_3 ),
inference(avatar_component_clause,[],[f47179]) ).
fof(f47182,plain,
( spl488_3
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37123,f47174,f47179]) ).
fof(f47184,definition,
( spl488_4
<=> s__subclass(sK486,sK487) ),
introduced(definition,[new_symbols(definition,[spl488_4])],[avatar_definition]) ).
fof(f47186,plain,
( s__subclass(sK486,sK487)
| ~ spl488_4 ),
inference(avatar_component_clause,[],[f47184]) ).
fof(f47187,plain,
( spl488_4
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37124,f47174,f47184]) ).
fof(f47189,definition,
( spl488_5
<=> s__subclass(sK485,sK486) ),
introduced(definition,[new_symbols(definition,[spl488_5])],[avatar_definition]) ).
fof(f47191,plain,
( s__subclass(sK485,sK486)
| ~ spl488_5 ),
inference(avatar_component_clause,[],[f47189]) ).
fof(f47192,plain,
( spl488_5
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37125,f47174,f47189]) ).
fof(f47194,definition,
( spl488_6
<=> s__subclass(sK484,sK485) ),
introduced(definition,[new_symbols(definition,[spl488_6])],[avatar_definition]) ).
fof(f47196,plain,
( s__subclass(sK484,sK485)
| ~ spl488_6 ),
inference(avatar_component_clause,[],[f47194]) ).
fof(f47197,plain,
( spl488_6
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37126,f47174,f47194]) ).
fof(f47199,definition,
( spl488_7
<=> s__subclass(sK483,sK484) ),
introduced(definition,[new_symbols(definition,[spl488_7])],[avatar_definition]) ).
fof(f47201,plain,
( s__subclass(sK483,sK484)
| ~ spl488_7 ),
inference(avatar_component_clause,[],[f47199]) ).
fof(f47202,plain,
( spl488_7
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37127,f47174,f47199]) ).
fof(f47204,definition,
( spl488_8
<=> s__subclass(sK482,sK483) ),
introduced(definition,[new_symbols(definition,[spl488_8])],[avatar_definition]) ).
fof(f47206,plain,
( s__subclass(sK482,sK483)
| ~ spl488_8 ),
inference(avatar_component_clause,[],[f47204]) ).
fof(f47207,plain,
( spl488_8
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37128,f47174,f47204]) ).
fof(f47209,definition,
( spl488_9
<=> s__subclass(sK481,sK482) ),
introduced(definition,[new_symbols(definition,[spl488_9])],[avatar_definition]) ).
fof(f47211,plain,
( s__subclass(sK481,sK482)
| ~ spl488_9 ),
inference(avatar_component_clause,[],[f47209]) ).
fof(f47212,plain,
( spl488_9
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37129,f47174,f47209]) ).
fof(f47214,definition,
( spl488_10
<=> s__subclass(sK480,sK481) ),
introduced(definition,[new_symbols(definition,[spl488_10])],[avatar_definition]) ).
fof(f47216,plain,
( s__subclass(sK480,sK481)
| ~ spl488_10 ),
inference(avatar_component_clause,[],[f47214]) ).
fof(f47217,plain,
( spl488_10
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37130,f47174,f47214]) ).
fof(f47219,definition,
( spl488_11
<=> s__subclass(sK479,sK480) ),
introduced(definition,[new_symbols(definition,[spl488_11])],[avatar_definition]) ).
fof(f47221,plain,
( s__subclass(sK479,sK480)
| ~ spl488_11 ),
inference(avatar_component_clause,[],[f47219]) ).
fof(f47222,plain,
( spl488_11
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37131,f47174,f47219]) ).
fof(f47224,definition,
( spl488_12
<=> s__subclass(sK478,sK479) ),
introduced(definition,[new_symbols(definition,[spl488_12])],[avatar_definition]) ).
fof(f47226,plain,
( s__subclass(sK478,sK479)
| ~ spl488_12 ),
inference(avatar_component_clause,[],[f47224]) ).
fof(f47227,plain,
( spl488_12
| ~ spl488_2 ),
inference(avatar_split_clause,[],[f37132,f47174,f47224]) ).
fof(f47278,plain,
spl488_2,
inference(avatar_split_clause,[],[f36825,f47174]) ).
fof(f93374,plain,
! [X2,X0,X1] :
( s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f37541,f37539]) ).
fof(f93375,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f93374,f37540]) ).
fof(f93433,plain,
! [X0] :
( ~ s__subclass(X0,s__Reptile)
| s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f93375,f47160]) ).
fof(f97312,plain,
( s__instance(s__Creature50_1,sK487)
| ~ spl488_3 ),
inference(resolution,[],[f93433,f47181]) ).
fof(f97348,plain,
( ! [X0] :
( ~ s__subclass(X0,sK487)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3 ),
inference(resolution,[],[f97312,f93375]) ).
fof(f97350,plain,
( s__instance(s__Creature50_1,sK486)
| ~ spl488_3
| ~ spl488_4 ),
inference(resolution,[],[f97348,f47186]) ).
fof(f97351,plain,
( ! [X0] :
( ~ s__subclass(X0,sK486)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3
| ~ spl488_4 ),
inference(resolution,[],[f97350,f93375]) ).
fof(f97353,plain,
( s__instance(s__Creature50_1,sK485)
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5 ),
inference(resolution,[],[f97351,f47191]) ).
fof(f97364,plain,
( ! [X0] :
( ~ s__subclass(X0,sK485)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5 ),
inference(resolution,[],[f97353,f93375]) ).
fof(f97376,plain,
( s__instance(s__Creature50_1,sK484)
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6 ),
inference(resolution,[],[f97364,f47196]) ).
fof(f97386,plain,
( ! [X0] :
( ~ s__subclass(X0,sK484)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6 ),
inference(resolution,[],[f97376,f93375]) ).
fof(f97432,plain,
( s__instance(s__Creature50_1,sK483)
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7 ),
inference(resolution,[],[f97386,f47201]) ).
fof(f97476,plain,
( ! [X0] :
( ~ s__subclass(X0,sK483)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7 ),
inference(resolution,[],[f97432,f93375]) ).
fof(f97565,plain,
( s__instance(s__Creature50_1,sK482)
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8 ),
inference(resolution,[],[f97476,f47206]) ).
fof(f97580,plain,
( ! [X0] :
( ~ s__subclass(X0,sK482)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8 ),
inference(resolution,[],[f97565,f93375]) ).
fof(f97605,plain,
( s__instance(s__Creature50_1,sK481)
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9 ),
inference(resolution,[],[f97580,f47211]) ).
fof(f97649,plain,
( ! [X0] :
( ~ s__subclass(X0,sK481)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9 ),
inference(resolution,[],[f97605,f93375]) ).
fof(f97651,plain,
( s__instance(s__Creature50_1,sK480)
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9
| ~ spl488_10 ),
inference(resolution,[],[f97649,f47216]) ).
fof(f97652,plain,
( ! [X0] :
( ~ s__subclass(X0,sK480)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9
| ~ spl488_10 ),
inference(resolution,[],[f97651,f93375]) ).
fof(f97669,plain,
( s__instance(s__Creature50_1,sK479)
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9
| ~ spl488_10
| ~ spl488_11 ),
inference(resolution,[],[f97652,f47221]) ).
fof(f97684,plain,
( ! [X0] :
( ~ s__subclass(X0,sK479)
| s__instance(s__Creature50_1,X0) )
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9
| ~ spl488_10
| ~ spl488_11 ),
inference(resolution,[],[f97669,f93375]) ).
fof(f97686,plain,
( s__instance(s__Creature50_1,sK478)
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9
| ~ spl488_10
| ~ spl488_11
| ~ spl488_12 ),
inference(resolution,[],[f97684,f47226]) ).
fof(f97687,plain,
( $false
| spl488_1
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9
| ~ spl488_10
| ~ spl488_11
| ~ spl488_12 ),
inference(forward_subsumption_resolution,[],[f97686,f47172]) ).
fof(f97688,plain,
( spl488_1
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9
| ~ spl488_10
| ~ spl488_11
| ~ spl488_12 ),
inference(avatar_contradiction_clause,[],[f97687]) ).
cnf(s1,plain,
( ~ spl488_1
| ~ spl488_2 ),
inference(sat_conversion,[],[f47177]) ).
cnf(s2,plain,
( ~ spl488_2
| spl488_3 ),
inference(sat_conversion,[],[f47182]) ).
cnf(s3,plain,
( ~ spl488_2
| spl488_4 ),
inference(sat_conversion,[],[f47187]) ).
cnf(s4,plain,
( ~ spl488_2
| spl488_5 ),
inference(sat_conversion,[],[f47192]) ).
cnf(s5,plain,
( ~ spl488_2
| spl488_6 ),
inference(sat_conversion,[],[f47197]) ).
cnf(s6,plain,
( ~ spl488_2
| spl488_7 ),
inference(sat_conversion,[],[f47202]) ).
cnf(s7,plain,
( ~ spl488_2
| spl488_8 ),
inference(sat_conversion,[],[f47207]) ).
cnf(s8,plain,
( ~ spl488_2
| spl488_9 ),
inference(sat_conversion,[],[f47212]) ).
cnf(s9,plain,
( ~ spl488_2
| spl488_10 ),
inference(sat_conversion,[],[f47217]) ).
cnf(s10,plain,
( ~ spl488_2
| spl488_11 ),
inference(sat_conversion,[],[f47222]) ).
cnf(s11,plain,
( ~ spl488_2
| spl488_12 ),
inference(sat_conversion,[],[f47227]) ).
cnf(s22,plain,
spl488_2,
inference(sat_conversion,[],[f47278]) ).
cnf(s7732,plain,
( spl488_1
| ~ spl488_3
| ~ spl488_4
| ~ spl488_5
| ~ spl488_6
| ~ spl488_7
| ~ spl488_8
| ~ spl488_9
| ~ spl488_10
| ~ spl488_11
| ~ spl488_12 ),
inference(sat_conversion,[],[f97688]) ).
cnf(s10185,plain,
spl488_12,
inference(rat,[],[s11,s22]) ).
cnf(s10186,plain,
spl488_11,
inference(rat,[],[s10,s22]) ).
cnf(s10187,plain,
spl488_10,
inference(rat,[],[s9,s22]) ).
cnf(s10188,plain,
spl488_9,
inference(rat,[],[s8,s22]) ).
cnf(s10189,plain,
spl488_8,
inference(rat,[],[s7,s22]) ).
cnf(s10190,plain,
spl488_7,
inference(rat,[],[s6,s22]) ).
cnf(s10191,plain,
spl488_6,
inference(rat,[],[s5,s22]) ).
cnf(s10192,plain,
spl488_5,
inference(rat,[],[s4,s22]) ).
cnf(s10193,plain,
spl488_4,
inference(rat,[],[s3,s22]) ).
cnf(s10194,plain,
spl488_3,
inference(rat,[],[s2,s22]) ).
cnf(s10195,plain,
spl488_1,
inference(rat,[],[s7732,s10185,s10186,s10187,s10188,s10189,s10190,s10191,s10192,s10193,s10194]) ).
cnf(s10196,plain,
$false,
inference(rat,[],[s1,s22,s10195]) ).
fof(f97689,plain,
$false,
inference(avatar_sat_refutation,[],[s10196]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n005.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 23:00:17 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.64/1.82 % (1267713)Will run a generic schedule for satisfiability detection.
% 7.64/1.82 % (1267721)dis+10_1_sil=32000:sp=arity:random_seed=1896132013:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 7.64/1.82 % (1267719)% WARNING: option uhcvi not known.
% 7.64/1.82 % (1267718)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4165921237_2997 on theBenchmark for (2997ds/0Mi)
% 7.64/1.82 % (1267719)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3620146898:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 7.64/1.82 % (1267720)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=206315742:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 7.64/1.82 % (1267722)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3383305767:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 7.64/1.82 % (1267723)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2832755546:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 7.64/1.82 % (1267724)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2403671127:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 7.64/1.82 % (1267721)Instruction limit reached!
% 7.64/1.82 % (1267721)------------------------------
% 7.64/1.82 % (1267721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.82 % (1267721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.82 % (1267721)CaDiCaL version: 2.1.3
% 7.64/1.82 % (1267721)Termination reason: Instruction limit
% 7.64/1.82 % (1267721)Termination phase: Preprocessing 3
% 7.64/1.82 % (1267721)Time elapsed: 0.039 s
% 7.64/1.82 % (1267721)Peak memory usage: 29 MB
% 7.64/1.82 % (1267721)Instructions burned: 103 (million)
% 7.64/1.82 % (1267732)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=645513849:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 7.64/1.82 % (1267722)Instruction limit reached!
% 7.64/1.82 % (1267722)------------------------------
% 7.64/1.82 % (1267722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.82 % (1267722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.82 % (1267722)CaDiCaL version: 2.1.3
% 7.64/1.82 % (1267722)Termination reason: Instruction limit
% 7.64/1.82 % (1267722)Termination phase: NewCNF
% 7.64/1.82 % (1267722)Time elapsed: 0.078 s
% 7.64/1.82 % (1267722)Peak memory usage: 32 MB
% 7.64/1.82 % (1267722)Instructions burned: 116 (million)
% 7.64/1.82 % (1267723)Instruction limit reached!
% 7.64/1.82 % (1267723)------------------------------
% 7.64/1.82 % (1267723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.82 % (1267723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.82 % (1267723)CaDiCaL version: 2.1.3
% 7.64/1.82 % (1267723)Termination reason: Instruction limit
% 7.64/1.82 % (1267723)Termination phase: Clausification
% 7.64/1.82 % (1267723)Time elapsed: 0.080 s
% 7.64/1.82 % (1267723)Peak memory usage: 31 MB
% 7.64/1.82 % (1267723)Instructions burned: 131 (million)
% 7.64/1.82 % (1267734)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=489208727:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 7.64/1.82 % (1267735)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1732597036:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 7.64/1.82 % (1267724)Instruction limit reached!
% 7.64/1.82 % (1267724)------------------------------
% 7.64/1.82 % (1267724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.82 % (1267724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.82 % (1267724)CaDiCaL version: 2.1.3
% 7.64/1.82 % (1267724)Termination reason: Instruction limit
% 7.64/1.82 % (1267724)Termination phase: Property scanning
% 7.64/1.82 % (1267724)Time elapsed: 0.100 s
% 7.64/1.82 % (1267724)Peak memory usage: 31 MB
% 7.64/1.82 % (1267724)Instructions burned: 161 (million)
% 7.64/1.82 % (1267738)ott-21_1_sil=16000:fs=off:random_seed=1695471661:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 7.64/1.82 % (1267734)Instruction limit reached!
% 7.64/1.82 % (1267734)------------------------------
% 7.64/1.82 % (1267734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.82 % (1267734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.83 % (1267734)CaDiCaL version: 2.1.3
% 7.64/1.83 % (1267734)Termination reason: Instruction limit
% 7.64/1.83 % (1267734)Termination phase: Clausification
% 7.64/1.83 % (1267734)Time elapsed: 0.080 s
% 7.64/1.83 % (1267734)Peak memory usage: 31 MB
% 7.64/1.83 % (1267734)Instructions burned: 131 (million)
% 7.64/1.83 % (1267740)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1434199076:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 7.64/1.83 % (1267738)Instruction limit reached!
% 7.64/1.83 % (1267738)------------------------------
% 7.64/1.83 % (1267738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.83 % (1267738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.83 % (1267738)CaDiCaL version: 2.1.3
% 7.64/1.83 % (1267738)Termination reason: Instruction limit
% 7.64/1.83 % (1267738)Termination phase: Property scanning
% 7.64/1.83 % (1267738)Time elapsed: 0.101 s
% 7.64/1.83 % (1267738)Peak memory usage: 31 MB
% 7.64/1.83 % (1267738)Instructions burned: 181 (million)
% 7.64/1.83 % (1267732)Instruction limit reached!
% 7.64/1.83 % (1267732)------------------------------
% 7.64/1.83 % (1267732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.83 % (1267732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.83 % (1267732)CaDiCaL version: 2.1.3
% 7.64/1.83 % (1267732)Termination reason: Instruction limit
% 7.64/1.83 % (1267732)Termination phase: Finite model building preprocessing
% 7.64/1.83 % (1267732)Time elapsed: 0.195 s
% 7.64/1.83 % (1267732)Peak memory usage: 42 MB
% 7.64/1.83 % (1267732)Instructions burned: 717 (million)
% 7.64/1.83 % (1267742)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3106292962:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 7.64/1.83 % (1267743)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2833495978:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 7.64/1.83 % (1267740)Instruction limit reached!
% 7.64/1.83 % (1267740)------------------------------
% 7.64/1.83 % (1267740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.83 % (1267740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.83 % (1267740)CaDiCaL version: 2.1.3
% 7.64/1.83 % (1267740)Termination reason: Instruction limit
% 7.64/1.83 % (1267740)Termination phase: Saturation
% 7.64/1.83 % (1267740)Time elapsed: 0.237 s
% 7.64/1.83 % (1267740)Peak memory usage: 35 MB
% 7.64/1.83 % (1267740)Instructions burned: 477 (million)
% 7.64/1.83 % (1267735)Instruction limit reached!
% 7.64/1.83 % (1267735)------------------------------
% 7.64/1.83 % (1267735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.83 % (1267735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.83 % (1267735)CaDiCaL version: 2.1.3
% 7.64/1.83 % (1267735)Termination reason: Instruction limit
% 7.64/1.83 % (1267735)Termination phase: Saturation
% 7.64/1.83 % (1267735)Time elapsed: 0.339 s
% 7.64/1.83 % (1267735)Peak memory usage: 40 MB
% 7.64/1.83 % (1267735)Instructions burned: 685 (million)
% 7.64/1.83 % (1267746)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2981469395:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 7.64/1.83 % (1267747)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4113628153:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 7.64/1.83 % (1267743)Instruction limit reached!
% 7.64/1.83 % (1267743)------------------------------
% 7.64/1.83 % (1267743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.83 % (1267743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.83 % (1267743)CaDiCaL version: 2.1.3
% 7.64/1.83 % (1267743)Termination reason: Instruction limit
% 7.64/1.83 % (1267743)Termination phase: Saturation
% 7.64/1.83 % (1267743)Time elapsed: 0.335 s
% 7.64/1.83 % (1267743)Peak memory usage: 45 MB
% 7.64/1.83 % (1267743)Instructions burned: 1180 (million)
% 7.64/1.83 % (1267750)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=424683293:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 7.64/1.83 % (1267742)Instruction limit reached!
% 7.64/1.83 % (1267742)------------------------------
% 7.64/1.83 % (1267742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.83 % (1267742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.83 % (1267742)CaDiCaL version: 2.1.3
% 7.64/1.83 % (1267742)Termination reason: Instruction limit
% 7.64/1.83 % (1267742)Termination phase: Finite model building preprocessing
% 7.64/1.83 % (1267742)Time elapsed: 0.414 s
% 7.64/1.83 % (1267742)Peak memory usage: 47 MB
% 7.64/1.83 % (1267742)Instructions burned: 865 (million)
% 7.64/1.83 % (1267752)fmb+10_1_sil=64000:random_seed=1256332665:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 7.64/1.83 % (1267747)Instruction limit reached!
% 7.64/1.83 % (1267747)------------------------------
% 7.64/1.83 % (1267747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.83 % (1267747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.83 % (1267747)CaDiCaL version: 2.1.3
% 7.64/1.83 % (1267747)Termination reason: Instruction limit
% 7.64/1.83 % (1267747)Termination phase: Saturation
% 7.64/1.83 % (1267747)Time elapsed: 0.354 s
% 7.64/1.83 % (1267747)Peak memory usage: 42 MB
% 7.64/1.83 % (1267747)Instructions burned: 693 (million)
% 7.64/1.83 % (1267750)Instruction limit reached!
% 7.64/1.83 % (1267750)------------------------------
% 7.64/1.83 % (1267750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.84 % (1267754)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1395522963:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 7.64/1.84 % (1267750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.84 % (1267750)CaDiCaL version: 2.1.3
% 7.64/1.84 % (1267750)Termination reason: Instruction limit
% 7.64/1.84 % (1267750)Termination phase: Saturation
% 7.64/1.84 % (1267750)Time elapsed: 0.238 s
% 7.64/1.84 % (1267750)Peak memory usage: 45 MB
% 7.64/1.84 % (1267750)Instructions burned: 882 (million)
% 7.64/1.84 % (1267756)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3033730433:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 7.64/1.84 % Detected minimum model sizes of [51]
% 7.64/1.84 % Detected maximum model sizes of [max]
% 7.64/1.84 % (1267718)Cannot represent all propositional literals internally
% 7.64/1.84 % (1267718)Refutation not found, incomplete strategy
% 7.64/1.84 % (1267718)------------------------------
% 7.64/1.84 % (1267718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.84 % (1267718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.84 % (1267718)CaDiCaL version: 2.1.3
% 7.64/1.84 % (1267718)Termination reason: Refutation not found, incomplete strategy
% 7.64/1.84 % (1267718)Time elapsed: 0.897 s
% 7.64/1.84 % (1267718)Peak memory usage: 59 MB
% 7.64/1.84 % (1267718)Instructions burned: 1860 (million)
% 7.64/1.84 % (1267746)Instruction limit reached!
% 7.64/1.84 % (1267746)------------------------------
% 7.64/1.84 % (1267746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.84 % (1267746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.84 % (1267746)CaDiCaL version: 2.1.3
% 7.64/1.84 % (1267746)Termination reason: Instruction limit
% 7.64/1.84 % (1267746)Termination phase: Finite model building preprocessing
% 7.64/1.84 % (1267746)Time elapsed: 0.431 s
% 7.64/1.84 % (1267746)Peak memory usage: 47 MB
% 7.64/1.84 % (1267746)Instructions burned: 891 (million)
% 7.64/1.84 % (1267718)------------------------------
% 7.64/1.84 % (1267718)------------------------------
% 7.64/1.84 % (1267758)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4110566161:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 7.64/1.84 % (1267760)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2153044351:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 7.64/1.84 % (1267756)Instruction limit reached!
% 7.64/1.84 % (1267756)------------------------------
% 7.64/1.84 % (1267756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.84 % (1267756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.84 % (1267756)CaDiCaL version: 2.1.3
% 7.64/1.84 % (1267756)Termination reason: Instruction limit
% 7.64/1.84 % (1267756)Termination phase: Finite model building preprocessing
% 7.64/1.84 % (1267756)Time elapsed: 0.244 s
% 7.64/1.84 % (1267756)Peak memory usage: 47 MB
% 7.64/1.84 % (1267756)Instructions burned: 923 (million)
% 7.64/1.84 % (1267762)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3986802237:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 7.64/1.84 % (1267719) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1267713-1267719"...
% 7.64/1.84 % (1267719)...printing done.
% 7.64/1.84 % (1267719)Refutation found. Thanks to Tanya!
% 7.64/1.84 % SZS status Theorem for theBenchmark
% 7.64/1.84 % SZS output start Proof for theBenchmark
% See solution above
% 7.64/1.85 % (1267719)------------------------------
% 7.64/1.85 % (1267719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/1.85 % (1267719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/1.85 % (1267719)CaDiCaL version: 2.1.3
% 7.64/1.85 % (1267719)Termination reason: Refutation
% 7.64/1.85 % (1267719)Time elapsed: 1.271 s
% 7.64/1.85 % (1267719)Peak memory usage: 67 MB
% 7.64/1.85 % (1267719)Instructions burned: 2433 (million)
% 7.64/1.85 % (1267713)Success in time 1.607 s
% 7.64/1.85 % Vampire exiting
%------------------------------------------------------------------------------