%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT025+4 : TPTP v9.3.1. Released v3.4.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:36:42 AM UTC 2026
% Result : Theorem 7.41s 3.28s
% Output : Refutation 8.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 14
% Syntax : Number of formulae : 140 ( 21 unt; 8 def)
% Number of atoms : 575 ( 0 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 807 ( 372 ~; 352 |; 58 &)
% ( 11 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 9 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 84 ( 0 sgn 73 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21181,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f25808,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& l1_cat_1(k12_nattra_1(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k12_nattra_1) ).
fof(f27592,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( r1_isocat_1(X0,X1)
<=> ? [X2] :
( m2_cat_1(X2,X0,X1)
& v8_cat_1(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_isocat_1) ).
fof(f29038,axiom,
! [X0,X1,X2] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1)
& v2_cat_1(X2)
& l1_cat_1(X2) )
=> m2_cat_1(k7_isocat_2(X0,X1,X2),k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_isocat_2) ).
fof(f29092,axiom,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> v8_cat_1(k7_isocat_2(X0,X1,X2),k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_isocat_2) ).
fof(f29093,conjecture,
! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> r1_isocat_1(k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_isocat_2) ).
fof(f29094,negated_conjecture,
~ ! [X0] :
( ( v2_cat_1(X0)
& l1_cat_1(X0) )
=> ! [X1] :
( ( v2_cat_1(X1)
& l1_cat_1(X1) )
=> ! [X2] :
( ( v2_cat_1(X2)
& l1_cat_1(X2) )
=> r1_isocat_1(k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2))) ) ) ),
inference(negated_conjecture,[status(cth)],[f29093]) ).
fof(f29098,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_isocat_1(k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2)))
& v2_cat_1(X2)
& l1_cat_1(X2) )
& v2_cat_1(X1)
& l1_cat_1(X1) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29094]) ).
fof(f29099,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_isocat_1(k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2)))
& v2_cat_1(X2)
& l1_cat_1(X2) )
& v2_cat_1(X1)
& l1_cat_1(X1) )
& v2_cat_1(X0)
& l1_cat_1(X0) ),
inference(flattening,[],[f29098]) ).
fof(f29116,plain,
! [X0] :
( ! [X1] :
( ( r1_isocat_1(X0,X1)
<=> ? [X2] :
( m2_cat_1(X2,X0,X1)
& v8_cat_1(X2,X0,X1) ) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f27592]) ).
fof(f29117,plain,
! [X0] :
( ! [X1] :
( ( r1_isocat_1(X0,X1)
<=> ? [X2] :
( m2_cat_1(X2,X0,X1)
& v8_cat_1(X2,X0,X1) ) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29116]) ).
fof(f29118,plain,
! [X0,X1] :
( ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f21181]) ).
fof(f29119,plain,
! [X0,X1] :
( ( v2_cat_1(k11_cat_2(X0,X1))
& l1_cat_1(k11_cat_2(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f29118]) ).
fof(f29124,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v8_cat_1(k7_isocat_2(X0,X1,X2),k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2)))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(ennf_transformation,[],[f29092]) ).
fof(f29125,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v8_cat_1(k7_isocat_2(X0,X1,X2),k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2)))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(flattening,[],[f29124]) ).
fof(f29158,plain,
! [X0,X1,X2] :
( m2_cat_1(k7_isocat_2(X0,X1,X2),k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2)))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) ),
inference(ennf_transformation,[],[f29038]) ).
fof(f29159,plain,
! [X0,X1,X2] :
( m2_cat_1(k7_isocat_2(X0,X1,X2),k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2)))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) ),
inference(flattening,[],[f29158]) ).
fof(f29166,plain,
! [X0,X1] :
( ( v1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& l1_cat_1(k12_nattra_1(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(ennf_transformation,[],[f25808]) ).
fof(f29167,plain,
! [X0,X1] :
( ( v1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& l1_cat_1(k12_nattra_1(X0,X1)) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(flattening,[],[f29166]) ).
fof(f29183,plain,
( ~ r1_isocat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
& v2_cat_1(sK6)
& l1_cat_1(sK6)
& v2_cat_1(sK5)
& l1_cat_1(sK5)
& v2_cat_1(sK4)
& l1_cat_1(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6)],[f29099]) ).
fof(f29186,plain,
! [X0] :
( ! [X1] :
( ( ( r1_isocat_1(X0,X1)
| ! [X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ v8_cat_1(X2,X0,X1) ) )
& ( ? [X2] :
( m2_cat_1(X2,X0,X1)
& v8_cat_1(X2,X0,X1) )
| ~ r1_isocat_1(X0,X1) ) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(nnf_transformation,[],[f29117]) ).
fof(f29187,plain,
! [X0] :
( ! [X1] :
( ( ( r1_isocat_1(X0,X1)
| ! [X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ v8_cat_1(X2,X0,X1) ) )
& ( ? [X3] :
( m2_cat_1(X3,X0,X1)
& v8_cat_1(X3,X0,X1) )
| ~ r1_isocat_1(X0,X1) ) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(rectify,[],[f29186]) ).
fof(f29188,plain,
! [X0] :
( ! [X1] :
( ( ( r1_isocat_1(X0,X1)
| ! [X2] :
( ~ m2_cat_1(X2,X0,X1)
| ~ v8_cat_1(X2,X0,X1) ) )
& ( ( m2_cat_1(sK9(X0,X1),X0,X1)
& v8_cat_1(sK9(X0,X1),X0,X1) )
| ~ r1_isocat_1(X0,X1) ) )
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) )
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1))],[f29187]) ).
fof(f29219,plain,
l1_cat_1(sK4),
inference(cnf_transformation,[],[f29183]) ).
fof(f29220,plain,
v2_cat_1(sK4),
inference(cnf_transformation,[],[f29183]) ).
fof(f29221,plain,
l1_cat_1(sK5),
inference(cnf_transformation,[],[f29183]) ).
fof(f29222,plain,
v2_cat_1(sK5),
inference(cnf_transformation,[],[f29183]) ).
fof(f29223,plain,
l1_cat_1(sK6),
inference(cnf_transformation,[],[f29183]) ).
fof(f29224,plain,
v2_cat_1(sK6),
inference(cnf_transformation,[],[f29183]) ).
fof(f29225,plain,
~ r1_isocat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6))),
inference(cnf_transformation,[],[f29183]) ).
fof(f29239,plain,
! [X2,X0,X1] :
( r1_isocat_1(X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| ~ v8_cat_1(X2,X0,X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29188]) ).
fof(f29240,plain,
! [X0,X1] :
( l1_cat_1(k11_cat_2(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f29119]) ).
fof(f29241,plain,
! [X0,X1] :
( v2_cat_1(k11_cat_2(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f29119]) ).
fof(f29244,plain,
! [X2,X0,X1] :
( v8_cat_1(k7_isocat_2(X0,X1,X2),k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2)))
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0) ),
inference(cnf_transformation,[],[f29125]) ).
fof(f29291,plain,
! [X2,X0,X1] :
( m2_cat_1(k7_isocat_2(X0,X1,X2),k12_nattra_1(k11_cat_2(X0,X1),X2),k12_nattra_1(X0,k12_nattra_1(X1,X2)))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X2) ),
inference(cnf_transformation,[],[f29159]) ).
fof(f29295,plain,
! [X0,X1] :
( l1_cat_1(k12_nattra_1(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f29167]) ).
fof(f29296,plain,
! [X0,X1] :
( v2_cat_1(k12_nattra_1(X0,X1))
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X1) ),
inference(cnf_transformation,[],[f29167]) ).
fof(f29366,definition,
( spl37_3
<=> l1_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6)) ),
introduced(definition,[new_symbols(definition,[spl37_3])],[avatar_definition]) ).
fof(f29367,plain,
( l1_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6))
| ~ spl37_3 ),
inference(avatar_component_clause,[],[f29366]) ).
fof(f29368,plain,
( ~ l1_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6))
| spl37_3 ),
inference(avatar_component_clause,[],[f29366]) ).
fof(f29370,definition,
( spl37_4
<=> v2_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6)) ),
introduced(definition,[new_symbols(definition,[spl37_4])],[avatar_definition]) ).
fof(f29371,plain,
( v2_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6))
| ~ spl37_4 ),
inference(avatar_component_clause,[],[f29370]) ).
fof(f29372,plain,
( ~ v2_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6))
| spl37_4 ),
inference(avatar_component_clause,[],[f29370]) ).
fof(f29374,definition,
( spl37_5
<=> l1_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6))) ),
introduced(definition,[new_symbols(definition,[spl37_5])],[avatar_definition]) ).
fof(f29375,plain,
( l1_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_5 ),
inference(avatar_component_clause,[],[f29374]) ).
fof(f29376,plain,
( ~ l1_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| spl37_5 ),
inference(avatar_component_clause,[],[f29374]) ).
fof(f29378,definition,
( spl37_6
<=> v2_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6))) ),
introduced(definition,[new_symbols(definition,[spl37_6])],[avatar_definition]) ).
fof(f29379,plain,
( v2_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_6 ),
inference(avatar_component_clause,[],[f29378]) ).
fof(f29380,plain,
( ~ v2_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| spl37_6 ),
inference(avatar_component_clause,[],[f29378]) ).
fof(f29386,plain,
( ~ v2_cat_1(k11_cat_2(sK4,sK5))
| ~ l1_cat_1(k11_cat_2(sK4,sK5))
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_3 ),
inference(resolution,[],[f29368,f29295]) ).
fof(f29387,plain,
( ~ v2_cat_1(k11_cat_2(sK4,sK5))
| ~ l1_cat_1(k11_cat_2(sK4,sK5))
| ~ l1_cat_1(sK6)
| spl37_3 ),
inference(forward_subsumption_resolution,[],[f29386,f29224]) ).
fof(f29388,plain,
( ~ v2_cat_1(k11_cat_2(sK4,sK5))
| ~ l1_cat_1(k11_cat_2(sK4,sK5))
| spl37_3 ),
inference(forward_subsumption_resolution,[],[f29387,f29223]) ).
fof(f29390,definition,
( spl37_8
<=> l1_cat_1(k11_cat_2(sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl37_8])],[avatar_definition]) ).
fof(f29391,plain,
( l1_cat_1(k11_cat_2(sK4,sK5))
| ~ spl37_8 ),
inference(avatar_component_clause,[],[f29390]) ).
fof(f29392,plain,
( ~ l1_cat_1(k11_cat_2(sK4,sK5))
| spl37_8 ),
inference(avatar_component_clause,[],[f29390]) ).
fof(f29394,definition,
( spl37_9
<=> v2_cat_1(k11_cat_2(sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl37_9])],[avatar_definition]) ).
fof(f29395,plain,
( v2_cat_1(k11_cat_2(sK4,sK5))
| ~ spl37_9 ),
inference(avatar_component_clause,[],[f29394]) ).
fof(f29396,plain,
( ~ v2_cat_1(k11_cat_2(sK4,sK5))
| spl37_9 ),
inference(avatar_component_clause,[],[f29394]) ).
fof(f29397,plain,
( ~ spl37_8
| ~ spl37_9
| spl37_3 ),
inference(avatar_split_clause,[],[f29388,f29366,f29394,f29390]) ).
fof(f29398,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| spl37_8 ),
inference(resolution,[],[f29392,f29240]) ).
fof(f29399,plain,
( ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| spl37_8 ),
inference(forward_subsumption_resolution,[],[f29398,f29220]) ).
fof(f29400,plain,
( ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| spl37_8 ),
inference(forward_subsumption_resolution,[],[f29399,f29219]) ).
fof(f29401,plain,
( ~ l1_cat_1(sK5)
| spl37_8 ),
inference(forward_subsumption_resolution,[],[f29400,f29222]) ).
fof(f29402,plain,
( $false
| spl37_8 ),
inference(forward_subsumption_resolution,[],[f29401,f29221]) ).
fof(f29403,plain,
spl37_8,
inference(avatar_contradiction_clause,[],[f29402]) ).
fof(f29404,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| spl37_9 ),
inference(resolution,[],[f29396,f29241]) ).
fof(f29405,plain,
( ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f29404,f29220]) ).
fof(f29406,plain,
( ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f29405,f29219]) ).
fof(f29407,plain,
( ~ l1_cat_1(sK5)
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f29406,f29222]) ).
fof(f29408,plain,
( $false
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f29407,f29221]) ).
fof(f29409,plain,
spl37_9,
inference(avatar_contradiction_clause,[],[f29408]) ).
fof(f29410,plain,
( ~ v2_cat_1(k11_cat_2(sK4,sK5))
| ~ l1_cat_1(k11_cat_2(sK4,sK5))
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_4 ),
inference(resolution,[],[f29372,f29296]) ).
fof(f29411,plain,
( ~ l1_cat_1(k11_cat_2(sK4,sK5))
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_4
| ~ spl37_9 ),
inference(forward_subsumption_resolution,[],[f29410,f29395]) ).
fof(f29412,plain,
( ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_4
| ~ spl37_8
| ~ spl37_9 ),
inference(forward_subsumption_resolution,[],[f29411,f29391]) ).
fof(f29413,plain,
( ~ l1_cat_1(sK6)
| spl37_4
| ~ spl37_8
| ~ spl37_9 ),
inference(forward_subsumption_resolution,[],[f29412,f29224]) ).
fof(f29414,plain,
( $false
| spl37_4
| ~ spl37_8
| ~ spl37_9 ),
inference(forward_subsumption_resolution,[],[f29413,f29223]) ).
fof(f29415,plain,
( spl37_4
| ~ spl37_8
| ~ spl37_9 ),
inference(avatar_contradiction_clause,[],[f29414]) ).
fof(f29416,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(k12_nattra_1(sK5,sK6))
| ~ l1_cat_1(k12_nattra_1(sK5,sK6))
| spl37_5 ),
inference(resolution,[],[f29376,f29295]) ).
fof(f29417,plain,
( ~ l1_cat_1(sK4)
| ~ v2_cat_1(k12_nattra_1(sK5,sK6))
| ~ l1_cat_1(k12_nattra_1(sK5,sK6))
| spl37_5 ),
inference(forward_subsumption_resolution,[],[f29416,f29220]) ).
fof(f29418,plain,
( ~ v2_cat_1(k12_nattra_1(sK5,sK6))
| ~ l1_cat_1(k12_nattra_1(sK5,sK6))
| spl37_5 ),
inference(forward_subsumption_resolution,[],[f29417,f29219]) ).
fof(f29420,definition,
( spl37_10
<=> l1_cat_1(k12_nattra_1(sK5,sK6)) ),
introduced(definition,[new_symbols(definition,[spl37_10])],[avatar_definition]) ).
fof(f29421,plain,
( l1_cat_1(k12_nattra_1(sK5,sK6))
| ~ spl37_10 ),
inference(avatar_component_clause,[],[f29420]) ).
fof(f29422,plain,
( ~ l1_cat_1(k12_nattra_1(sK5,sK6))
| spl37_10 ),
inference(avatar_component_clause,[],[f29420]) ).
fof(f29424,definition,
( spl37_11
<=> v2_cat_1(k12_nattra_1(sK5,sK6)) ),
introduced(definition,[new_symbols(definition,[spl37_11])],[avatar_definition]) ).
fof(f29425,plain,
( v2_cat_1(k12_nattra_1(sK5,sK6))
| ~ spl37_11 ),
inference(avatar_component_clause,[],[f29424]) ).
fof(f29426,plain,
( ~ v2_cat_1(k12_nattra_1(sK5,sK6))
| spl37_11 ),
inference(avatar_component_clause,[],[f29424]) ).
fof(f29427,plain,
( ~ spl37_10
| ~ spl37_11
| spl37_5 ),
inference(avatar_split_clause,[],[f29418,f29374,f29424,f29420]) ).
fof(f29431,plain,
( ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_10 ),
inference(resolution,[],[f29422,f29295]) ).
fof(f29432,plain,
( ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_10 ),
inference(forward_subsumption_resolution,[],[f29431,f29222]) ).
fof(f29433,plain,
( ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_10 ),
inference(forward_subsumption_resolution,[],[f29432,f29221]) ).
fof(f29434,plain,
( ~ l1_cat_1(sK6)
| spl37_10 ),
inference(forward_subsumption_resolution,[],[f29433,f29224]) ).
fof(f29435,plain,
( $false
| spl37_10 ),
inference(forward_subsumption_resolution,[],[f29434,f29223]) ).
fof(f29436,plain,
spl37_10,
inference(avatar_contradiction_clause,[],[f29435]) ).
fof(f29437,plain,
! [X0] :
( ~ m2_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ v8_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ v2_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ l1_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ v2_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6))
| ~ l1_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6)) ),
inference(resolution,[],[f29239,f29225]) ).
fof(f29438,plain,
( ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_11 ),
inference(resolution,[],[f29426,f29296]) ).
fof(f29439,plain,
( ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_11 ),
inference(forward_subsumption_resolution,[],[f29438,f29222]) ).
fof(f29440,plain,
( ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl37_11 ),
inference(forward_subsumption_resolution,[],[f29439,f29221]) ).
fof(f29441,plain,
( ~ l1_cat_1(sK6)
| spl37_11 ),
inference(forward_subsumption_resolution,[],[f29440,f29224]) ).
fof(f29442,plain,
( $false
| spl37_11 ),
inference(forward_subsumption_resolution,[],[f29441,f29223]) ).
fof(f29443,plain,
spl37_11,
inference(avatar_contradiction_clause,[],[f29442]) ).
fof(f29445,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(k12_nattra_1(sK5,sK6))
| ~ l1_cat_1(k12_nattra_1(sK5,sK6))
| spl37_6 ),
inference(resolution,[],[f29380,f29296]) ).
fof(f29446,plain,
( ~ l1_cat_1(sK4)
| ~ v2_cat_1(k12_nattra_1(sK5,sK6))
| ~ l1_cat_1(k12_nattra_1(sK5,sK6))
| spl37_6 ),
inference(forward_subsumption_resolution,[],[f29445,f29220]) ).
fof(f29447,plain,
( ~ v2_cat_1(k12_nattra_1(sK5,sK6))
| ~ l1_cat_1(k12_nattra_1(sK5,sK6))
| spl37_6 ),
inference(forward_subsumption_resolution,[],[f29446,f29219]) ).
fof(f29448,plain,
( ~ l1_cat_1(k12_nattra_1(sK5,sK6))
| spl37_6
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f29447,f29425]) ).
fof(f29449,plain,
( $false
| spl37_6
| ~ spl37_10
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f29448,f29421]) ).
fof(f29450,plain,
( spl37_6
| ~ spl37_10
| ~ spl37_11 ),
inference(avatar_contradiction_clause,[],[f29449]) ).
fof(f29451,plain,
( ! [X0] :
( ~ m2_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ v8_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ l1_cat_1(k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ v2_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6))
| ~ l1_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6)) )
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29437,f29379]) ).
fof(f29453,plain,
( ! [X0] :
( ~ m2_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ v8_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ v2_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6))
| ~ l1_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6)) )
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29451,f29375]) ).
fof(f29455,plain,
( ! [X0] :
( ~ m2_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ v8_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ l1_cat_1(k12_nattra_1(k11_cat_2(sK4,sK5),sK6)) )
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29453,f29371]) ).
fof(f29457,plain,
( ! [X0] :
( ~ v8_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ m2_cat_1(X0,k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6))) )
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29455,f29367]) ).
fof(f29519,plain,
( ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ m2_cat_1(k7_isocat_2(sK4,sK5,sK6),k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(resolution,[],[f29244,f29457]) ).
fof(f29520,plain,
( ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ m2_cat_1(k7_isocat_2(sK4,sK5,sK6),k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29519,f29224]) ).
fof(f29521,plain,
( ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ m2_cat_1(k7_isocat_2(sK4,sK5,sK6),k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29520,f29223]) ).
fof(f29522,plain,
( ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ m2_cat_1(k7_isocat_2(sK4,sK5,sK6),k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29521,f29222]) ).
fof(f29523,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ m2_cat_1(k7_isocat_2(sK4,sK5,sK6),k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29522,f29221]) ).
fof(f29524,plain,
( ~ l1_cat_1(sK4)
| ~ m2_cat_1(k7_isocat_2(sK4,sK5,sK6),k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29523,f29220]) ).
fof(f29525,plain,
( ~ m2_cat_1(k7_isocat_2(sK4,sK5,sK6),k12_nattra_1(k11_cat_2(sK4,sK5),sK6),k12_nattra_1(sK4,k12_nattra_1(sK5,sK6)))
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29524,f29219]) ).
fof(f29531,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(resolution,[],[f29291,f29525]) ).
fof(f29532,plain,
( ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29531,f29220]) ).
fof(f29533,plain,
( ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29532,f29219]) ).
fof(f29534,plain,
( ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29533,f29222]) ).
fof(f29535,plain,
( ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29534,f29221]) ).
fof(f29536,plain,
( ~ l1_cat_1(sK6)
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29535,f29224]) ).
fof(f29537,plain,
( $false
| ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f29536,f29223]) ).
fof(f29538,plain,
( ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(avatar_contradiction_clause,[],[f29537]) ).
cnf(s3,plain,
( spl37_3
| ~ spl37_8
| ~ spl37_9 ),
inference(sat_conversion,[],[f29397]) ).
cnf(s4,plain,
spl37_8,
inference(sat_conversion,[],[f29403]) ).
cnf(s5,plain,
spl37_9,
inference(sat_conversion,[],[f29409]) ).
cnf(s6,plain,
( spl37_4
| ~ spl37_8
| ~ spl37_9 ),
inference(sat_conversion,[],[f29415]) ).
cnf(s7,plain,
( spl37_5
| ~ spl37_10
| ~ spl37_11 ),
inference(sat_conversion,[],[f29427]) ).
cnf(s8,plain,
spl37_10,
inference(sat_conversion,[],[f29436]) ).
cnf(s9,plain,
spl37_11,
inference(sat_conversion,[],[f29443]) ).
cnf(s10,plain,
( spl37_6
| ~ spl37_10
| ~ spl37_11 ),
inference(sat_conversion,[],[f29450]) ).
cnf(s11,plain,
( ~ spl37_3
| ~ spl37_4
| ~ spl37_5
| ~ spl37_6 ),
inference(sat_conversion,[],[f29538]) ).
cnf(s12,plain,
spl37_6,
inference(rat,[],[s10,s9,s8]) ).
cnf(s13,plain,
spl37_5,
inference(rat,[],[s7,s9,s8]) ).
cnf(s14,plain,
spl37_4,
inference(rat,[],[s6,s5,s4]) ).
cnf(s15,plain,
~ spl37_3,
inference(rat,[],[s11,s12,s13,s14]) ).
cnf(s16,plain,
$false,
inference(rat,[],[s3,s5,s4,s15]) ).
fof(f29539,plain,
$false,
inference(avatar_sat_refutation,[],[s16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT025+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n007.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 21:15:34 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 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
% 7.41/3.28 % (2839309)Detected formulas, will run a generic FOF schedule.
% 7.41/3.28 % (2839320)dis-21_1_sil=8000:lcm=predicate:random_seed=2303932510:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2982 on theBenchmark for (2982ds/129Mi)
% 7.41/3.28 % (2839315)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=1248249023:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2982 on theBenchmark for (2982ds/134677Mi)
% 7.41/3.28 % (2839317)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4190056354:i=109:sd=1:ins=1:gsp=on:ss=axioms_2982 on theBenchmark for (2982ds/109Mi)
% 7.41/3.28 % (2839316)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=1053268443:i=141695:sd=1:nm=32:gsp=on:ss=included_2982 on theBenchmark for (2982ds/141695Mi)
% 7.41/3.28 % (2839318)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3096068960:i=119:av=off:ss=axioms_2982 on theBenchmark for (2982ds/119Mi)
% 7.41/3.28 % (2839319)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=150212507:s2a=on:i=139:gtg=position_2982 on theBenchmark for (2982ds/139Mi)
% 7.41/3.28 % (2839314)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=519298692:i=141193_2982 on theBenchmark for (2982ds/141193Mi)
% 7.41/3.28 % (2839320)Instruction limit reached!
% 7.41/3.28 % (2839320)------------------------------
% 7.41/3.28 % (2839320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839320)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839320)Termination reason: Instruction limit
% 7.41/3.28 % (2839320)Termination phase: SInE selection
% 7.41/3.28 % (2839320)Time elapsed: 0.054 s
% 7.41/3.28 % (2839320)Peak memory usage: 127 MB
% 7.41/3.28 % (2839320)Instructions burned: 130 (million)
% 7.41/3.28 % (2839319)Instruction limit reached!
% 7.41/3.28 % (2839319)------------------------------
% 7.41/3.28 % (2839319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839319)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839319)Termination reason: Instruction limit
% 7.41/3.28 % (2839319)Termination phase: Property scanning
% 7.41/3.28 % (2839319)Time elapsed: 0.060 s
% 7.41/3.28 % (2839319)Peak memory usage: 126 MB
% 7.41/3.28 % (2839319)Instructions burned: 139 (million)
% 7.41/3.28 % (2839317)Instruction limit reached!
% 7.41/3.28 % (2839317)------------------------------
% 7.41/3.28 % (2839317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839317)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839317)Termination reason: Instruction limit
% 7.41/3.28 % (2839317)Termination phase: SInE selection
% 7.41/3.28 % (2839317)Time elapsed: 0.079 s
% 7.41/3.28 % (2839317)Peak memory usage: 126 MB
% 7.41/3.28 % (2839317)Instructions burned: 109 (million)
% 7.41/3.28 % (2839318)Instruction limit reached!
% 7.41/3.28 % (2839318)------------------------------
% 7.41/3.28 % (2839318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839318)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839318)Termination reason: Instruction limit
% 7.41/3.28 % (2839318)Termination phase: SInE selection
% 7.41/3.28 % (2839318)Time elapsed: 0.088 s
% 7.41/3.28 % (2839318)Peak memory usage: 126 MB
% 7.41/3.28 % (2839318)Instructions burned: 120 (million)
% 7.41/3.28 % (2839328)lrs+10_1_sil=8000:sp=occurrence:random_seed=2456232992:i=285:sd=3:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/285Mi)
% 7.41/3.28 % (2839329)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2736963841:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/157Mi)
% 7.41/3.28 % (2839330)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1012619179:i=325:sd=1:ss=axioms:sgt=32_2980 on theBenchmark for (2980ds/325Mi)
% 7.41/3.28 % (2839331)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=1711085622:s2a=on:i=248:s2at=1.23:gtg=position_2979 on theBenchmark for (2979ds/248Mi)
% 7.41/3.28 % (2839329)Instruction limit reached!
% 7.41/3.28 % (2839329)------------------------------
% 7.41/3.28 % (2839329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839329)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839329)Termination reason: Instruction limit
% 7.41/3.28 % (2839329)Termination phase: Property scanning
% 7.41/3.28 % (2839329)Time elapsed: 0.068 s
% 7.41/3.28 % (2839329)Peak memory usage: 127 MB
% 7.41/3.28 % (2839329)Instructions burned: 159 (million)
% 7.41/3.28 % (2839331)Instruction limit reached!
% 7.41/3.28 % (2839331)------------------------------
% 7.41/3.28 % (2839331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839331)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839331)Termination reason: Instruction limit
% 7.41/3.28 % (2839331)Termination phase: Property scanning
% 7.41/3.28 % (2839331)Time elapsed: 0.104 s
% 7.41/3.28 % (2839331)Peak memory usage: 127 MB
% 7.41/3.28 % (2839331)Instructions burned: 248 (million)
% 7.41/3.28 % (2839330)First to succeed.
% 7.41/3.28 % (2839330)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2839309"
% 7.41/3.28 % (2839328)Instruction limit reached!
% 7.41/3.28 % (2839328)------------------------------
% 7.41/3.28 % (2839328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839328)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839328)Termination reason: Instruction limit
% 7.41/3.28 % (2839328)Termination phase: Saturation
% 7.41/3.28 % (2839328)Time elapsed: 0.222 s
% 7.41/3.28 % (2839328)Peak memory usage: 133 MB
% 7.41/3.28 % (2839328)Instructions burned: 285 (million)
% 7.41/3.28 % (2839336)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1644455349:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2978 on theBenchmark for (2978ds/294Mi)
% 7.41/3.28 % (2839337)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2918812620:i=2350_2977 on theBenchmark for (2977ds/2350Mi)
% 7.41/3.28 % (2839336)Instruction limit reached!
% 7.41/3.28 % (2839336)------------------------------
% 7.41/3.28 % (2839336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839336)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839336)Termination reason: Instruction limit
% 7.41/3.28 % (2839336)Termination phase: Property scanning
% 7.41/3.28 % (2839336)Time elapsed: 0.124 s
% 7.41/3.28 % (2839336)Peak memory usage: 130 MB
% 7.41/3.28 % (2839336)Instructions burned: 295 (million)
% 7.41/3.28 % (2839338)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2962182904:cts=off:i=113:fsr=off:ss=included:sgt=4_2976 on theBenchmark for (2976ds/113Mi)
% 7.41/3.28 % (2839338)Instruction limit reached!
% 7.41/3.28 % (2839338)------------------------------
% 7.41/3.28 % (2839338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.28 % (2839338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.28 % (2839338)CaDiCaL version: 2.1.3
% 7.41/3.28 % (2839338)Termination reason: Instruction limit
% 7.41/3.28 % (2839338)Termination phase: SInE selection
% 7.41/3.28 % (2839338)Time elapsed: 0.091 s
% 7.41/3.28 % (2839338)Peak memory usage: 127 MB
% 7.41/3.28 % (2839338)Instructions burned: 114 (million)
% 7.41/3.28 % (2839330)Refutation found. Thanks to Tanya!
% 7.41/3.28 % SZS status Theorem for theBenchmark
% 7.41/3.28 % SZS output start Proof for theBenchmark
% See solution above
% 8.45/3.53 % (2839330)------------------------------
% 8.45/3.53 % (2839330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.45/3.53 % (2839330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.45/3.53 % (2839330)CaDiCaL version: 2.1.3
% 8.45/3.53 % (2839330)Termination reason: Refutation
% 8.45/3.53 % (2839330)Time elapsed: 0.167 s
% 8.45/3.53 % (2839330)Peak memory usage: 133 MB
% 8.45/3.53 % (2839330)Instructions burned: 208 (million)
% 8.45/3.53 % (2839330)------------------------------
% 8.45/3.53 % (2839330)------------------------------
% 8.45/3.53 % (2839309)Success in time 2.602 s
% 8.45/3.53 % Vampire exiting
%------------------------------------------------------------------------------