%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT032+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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:36:47 AM UTC 2026
% Result : Theorem 17.79s 3.77s
% Output : Refutation 19.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 24
% Syntax : Number of formulae : 144 ( 33 unt; 18 def)
% Number of atoms : 538 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 702 ( 308 ~; 301 |; 58 &)
% ( 21 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 19 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 82 ( 0 sgn 71 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8397,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/sandbox/benchmark/theBenchmark.p',dt_k11_cat_2) ).
fof(f10548,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/sandbox/benchmark/theBenchmark.p',dt_k12_nattra_1) ).
fof(f11372,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/sandbox/benchmark/theBenchmark.p',d4_isocat_1) ).
fof(f11747,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(k17_isocat_2(X0,X1,X2),k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k17_isocat_2) ).
fof(f11813,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(k17_isocat_2(X0,X1,X2),k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,X2))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_isocat_2) ).
fof(f11814,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(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,X2))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t49_isocat_2) ).
fof(f11815,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(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,X2))) ) ) ),
inference(negated_conjecture,[status(cth)],[f11814]) ).
fof(f11819,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_isocat_1(k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,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,[],[f11815]) ).
fof(f11820,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_isocat_1(k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,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,[],[f11819]) ).
fof(f11839,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,[],[f11372]) ).
fof(f11840,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,[],[f11839]) ).
fof(f11841,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,[],[f8397]) ).
fof(f11842,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,[],[f11841]) ).
fof(f11843,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v8_cat_1(k17_isocat_2(X0,X1,X2),k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,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,[],[f11813]) ).
fof(f11844,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v8_cat_1(k17_isocat_2(X0,X1,X2),k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,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,[],[f11843]) ).
fof(f11879,plain,
! [X0,X1,X2] :
( m2_cat_1(k17_isocat_2(X0,X1,X2),k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,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,[],[f11747]) ).
fof(f11880,plain,
! [X0,X1,X2] :
( m2_cat_1(k17_isocat_2(X0,X1,X2),k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,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,[],[f11879]) ).
fof(f11889,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,[],[f10548]) ).
fof(f11890,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,[],[f11889]) ).
fof(f11906,plain,
( ~ r1_isocat_1(k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,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)],[f11820]) ).
fof(f11909,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,[],[f11840]) ).
fof(f11910,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,[],[f11909]) ).
fof(f11911,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))],[f11910]) ).
fof(f11945,plain,
l1_cat_1(sK4),
inference(cnf_transformation,[],[f11906]) ).
fof(f11946,plain,
v2_cat_1(sK4),
inference(cnf_transformation,[],[f11906]) ).
fof(f11947,plain,
l1_cat_1(sK5),
inference(cnf_transformation,[],[f11906]) ).
fof(f11948,plain,
v2_cat_1(sK5),
inference(cnf_transformation,[],[f11906]) ).
fof(f11949,plain,
l1_cat_1(sK6),
inference(cnf_transformation,[],[f11906]) ).
fof(f11950,plain,
v2_cat_1(sK6),
inference(cnf_transformation,[],[f11906]) ).
fof(f11951,plain,
~ r1_isocat_1(k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6))),
inference(cnf_transformation,[],[f11906]) ).
fof(f11966,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,[],[f11911]) ).
fof(f11967,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,[],[f11842]) ).
fof(f11968,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,[],[f11842]) ).
fof(f11969,plain,
! [X2,X0,X1] :
( v8_cat_1(k17_isocat_2(X0,X1,X2),k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,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,[],[f11844]) ).
fof(f12022,plain,
! [X2,X0,X1] :
( m2_cat_1(k17_isocat_2(X0,X1,X2),k12_nattra_1(X0,k11_cat_2(X1,X2)),k11_cat_2(k12_nattra_1(X0,X1),k12_nattra_1(X0,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,[],[f11880]) ).
fof(f12027,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,[],[f11890]) ).
fof(f12028,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,[],[f11890]) ).
fof(f12095,definition,
( spl40_3
<=> l1_cat_1(k12_nattra_1(sK4,k11_cat_2(sK5,sK6))) ),
introduced(definition,[new_symbols(definition,[spl40_3])],[avatar_definition]) ).
fof(f12097,plain,
( ~ l1_cat_1(k12_nattra_1(sK4,k11_cat_2(sK5,sK6)))
| spl40_3 ),
inference(avatar_component_clause,[],[f12095]) ).
fof(f12099,definition,
( spl40_4
<=> v2_cat_1(k12_nattra_1(sK4,k11_cat_2(sK5,sK6))) ),
introduced(definition,[new_symbols(definition,[spl40_4])],[avatar_definition]) ).
fof(f12101,plain,
( ~ v2_cat_1(k12_nattra_1(sK4,k11_cat_2(sK5,sK6)))
| spl40_4 ),
inference(avatar_component_clause,[],[f12099]) ).
fof(f12103,definition,
( spl40_5
<=> l1_cat_1(k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6))) ),
introduced(definition,[new_symbols(definition,[spl40_5])],[avatar_definition]) ).
fof(f12105,plain,
( ~ l1_cat_1(k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| spl40_5 ),
inference(avatar_component_clause,[],[f12103]) ).
fof(f12107,definition,
( spl40_6
<=> v2_cat_1(k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6))) ),
introduced(definition,[new_symbols(definition,[spl40_6])],[avatar_definition]) ).
fof(f12109,plain,
( ~ v2_cat_1(k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| spl40_6 ),
inference(avatar_component_clause,[],[f12107]) ).
fof(f12115,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(k11_cat_2(sK5,sK6))
| ~ l1_cat_1(k11_cat_2(sK5,sK6))
| spl40_3 ),
inference(resolution,[],[f12097,f12027]) ).
fof(f12117,definition,
( spl40_8
<=> l1_cat_1(k11_cat_2(sK5,sK6)) ),
introduced(definition,[new_symbols(definition,[spl40_8])],[avatar_definition]) ).
fof(f12119,plain,
( ~ l1_cat_1(k11_cat_2(sK5,sK6))
| spl40_8 ),
inference(avatar_component_clause,[],[f12117]) ).
fof(f12121,definition,
( spl40_9
<=> v2_cat_1(k11_cat_2(sK5,sK6)) ),
introduced(definition,[new_symbols(definition,[spl40_9])],[avatar_definition]) ).
fof(f12123,plain,
( ~ v2_cat_1(k11_cat_2(sK5,sK6))
| spl40_9 ),
inference(avatar_component_clause,[],[f12121]) ).
fof(f12125,definition,
( spl40_10
<=> l1_cat_1(sK4) ),
introduced(definition,[new_symbols(definition,[spl40_10])],[avatar_definition]) ).
fof(f12127,plain,
( ~ l1_cat_1(sK4)
| spl40_10 ),
inference(avatar_component_clause,[],[f12125]) ).
fof(f12129,definition,
( spl40_11
<=> v2_cat_1(sK4) ),
introduced(definition,[new_symbols(definition,[spl40_11])],[avatar_definition]) ).
fof(f12131,plain,
( ~ v2_cat_1(sK4)
| spl40_11 ),
inference(avatar_component_clause,[],[f12129]) ).
fof(f12132,plain,
( ~ spl40_8
| ~ spl40_9
| ~ spl40_10
| ~ spl40_11
| spl40_3 ),
inference(avatar_split_clause,[],[f12115,f12095,f12129,f12125,f12121,f12117]) ).
fof(f12133,plain,
( ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl40_8 ),
inference(resolution,[],[f12119,f11967]) ).
fof(f12135,definition,
( spl40_12
<=> l1_cat_1(sK6) ),
introduced(definition,[new_symbols(definition,[spl40_12])],[avatar_definition]) ).
fof(f12137,plain,
( ~ l1_cat_1(sK6)
| spl40_12 ),
inference(avatar_component_clause,[],[f12135]) ).
fof(f12139,definition,
( spl40_13
<=> v2_cat_1(sK6) ),
introduced(definition,[new_symbols(definition,[spl40_13])],[avatar_definition]) ).
fof(f12141,plain,
( ~ v2_cat_1(sK6)
| spl40_13 ),
inference(avatar_component_clause,[],[f12139]) ).
fof(f12143,definition,
( spl40_14
<=> l1_cat_1(sK5) ),
introduced(definition,[new_symbols(definition,[spl40_14])],[avatar_definition]) ).
fof(f12145,plain,
( ~ l1_cat_1(sK5)
| spl40_14 ),
inference(avatar_component_clause,[],[f12143]) ).
fof(f12147,definition,
( spl40_15
<=> v2_cat_1(sK5) ),
introduced(definition,[new_symbols(definition,[spl40_15])],[avatar_definition]) ).
fof(f12149,plain,
( ~ v2_cat_1(sK5)
| spl40_15 ),
inference(avatar_component_clause,[],[f12147]) ).
fof(f12150,plain,
( ~ spl40_12
| ~ spl40_13
| ~ spl40_14
| ~ spl40_15
| spl40_8 ),
inference(avatar_split_clause,[],[f12133,f12117,f12147,f12143,f12139,f12135]) ).
fof(f12151,plain,
( $false
| spl40_12 ),
inference(resolution,[],[f12137,f11949]) ).
fof(f12152,plain,
spl40_12,
inference(avatar_contradiction_clause,[],[f12151]) ).
fof(f12154,plain,
! [X0] :
( ~ m2_cat_1(X0,k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| ~ v8_cat_1(X0,k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| ~ v2_cat_1(k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| ~ l1_cat_1(k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| ~ v2_cat_1(k12_nattra_1(sK4,k11_cat_2(sK5,sK6)))
| ~ l1_cat_1(k12_nattra_1(sK4,k11_cat_2(sK5,sK6))) ),
inference(resolution,[],[f11966,f11951]) ).
fof(f12156,definition,
( spl40_16
<=> ! [X0] :
( ~ m2_cat_1(X0,k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| ~ v8_cat_1(X0,k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6))) ) ),
introduced(definition,[new_symbols(definition,[spl40_16])],[avatar_definition]) ).
fof(f12157,plain,
( ! [X0] :
( ~ v8_cat_1(X0,k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| ~ m2_cat_1(X0,k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6))) )
| ~ spl40_16 ),
inference(avatar_component_clause,[],[f12156]) ).
fof(f12158,plain,
( ~ spl40_3
| ~ spl40_4
| ~ spl40_5
| ~ spl40_6
| spl40_16 ),
inference(avatar_split_clause,[],[f12154,f12156,f12107,f12103,f12099,f12095]) ).
fof(f12159,plain,
( $false
| spl40_13 ),
inference(resolution,[],[f12141,f11950]) ).
fof(f12160,plain,
spl40_13,
inference(avatar_contradiction_clause,[],[f12159]) ).
fof(f12166,plain,
( $false
| spl40_14 ),
inference(resolution,[],[f12145,f11947]) ).
fof(f12167,plain,
spl40_14,
inference(avatar_contradiction_clause,[],[f12166]) ).
fof(f12168,plain,
( $false
| spl40_15 ),
inference(resolution,[],[f12149,f11948]) ).
fof(f12169,plain,
spl40_15,
inference(avatar_contradiction_clause,[],[f12168]) ).
fof(f12170,plain,
( ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl40_9 ),
inference(resolution,[],[f12123,f11968]) ).
fof(f12171,plain,
( ~ spl40_12
| ~ spl40_13
| ~ spl40_14
| ~ spl40_15
| spl40_9 ),
inference(avatar_split_clause,[],[f12170,f12121,f12147,f12143,f12139,f12135]) ).
fof(f12172,plain,
( $false
| spl40_10 ),
inference(resolution,[],[f12127,f11945]) ).
fof(f12173,plain,
spl40_10,
inference(avatar_contradiction_clause,[],[f12172]) ).
fof(f12174,plain,
( $false
| spl40_11 ),
inference(resolution,[],[f12131,f11946]) ).
fof(f12175,plain,
spl40_11,
inference(avatar_contradiction_clause,[],[f12174]) ).
fof(f12176,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(k11_cat_2(sK5,sK6))
| ~ l1_cat_1(k11_cat_2(sK5,sK6))
| spl40_4 ),
inference(resolution,[],[f12101,f12028]) ).
fof(f12177,plain,
( ~ spl40_8
| ~ spl40_9
| ~ spl40_10
| ~ spl40_11
| spl40_4 ),
inference(avatar_split_clause,[],[f12176,f12099,f12129,f12125,f12121,f12117]) ).
fof(f12178,plain,
( ~ v2_cat_1(k12_nattra_1(sK4,sK5))
| ~ l1_cat_1(k12_nattra_1(sK4,sK5))
| ~ v2_cat_1(k12_nattra_1(sK4,sK6))
| ~ l1_cat_1(k12_nattra_1(sK4,sK6))
| spl40_5 ),
inference(resolution,[],[f12105,f11967]) ).
fof(f12180,definition,
( spl40_18
<=> l1_cat_1(k12_nattra_1(sK4,sK6)) ),
introduced(definition,[new_symbols(definition,[spl40_18])],[avatar_definition]) ).
fof(f12182,plain,
( ~ l1_cat_1(k12_nattra_1(sK4,sK6))
| spl40_18 ),
inference(avatar_component_clause,[],[f12180]) ).
fof(f12184,definition,
( spl40_19
<=> v2_cat_1(k12_nattra_1(sK4,sK6)) ),
introduced(definition,[new_symbols(definition,[spl40_19])],[avatar_definition]) ).
fof(f12186,plain,
( ~ v2_cat_1(k12_nattra_1(sK4,sK6))
| spl40_19 ),
inference(avatar_component_clause,[],[f12184]) ).
fof(f12188,definition,
( spl40_20
<=> l1_cat_1(k12_nattra_1(sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl40_20])],[avatar_definition]) ).
fof(f12190,plain,
( ~ l1_cat_1(k12_nattra_1(sK4,sK5))
| spl40_20 ),
inference(avatar_component_clause,[],[f12188]) ).
fof(f12192,definition,
( spl40_21
<=> v2_cat_1(k12_nattra_1(sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl40_21])],[avatar_definition]) ).
fof(f12194,plain,
( ~ v2_cat_1(k12_nattra_1(sK4,sK5))
| spl40_21 ),
inference(avatar_component_clause,[],[f12192]) ).
fof(f12195,plain,
( ~ spl40_18
| ~ spl40_19
| ~ spl40_20
| ~ spl40_21
| spl40_5 ),
inference(avatar_split_clause,[],[f12178,f12103,f12192,f12188,f12184,f12180]) ).
fof(f12196,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl40_18 ),
inference(resolution,[],[f12182,f12027]) ).
fof(f12197,plain,
( ~ spl40_12
| ~ spl40_13
| ~ spl40_10
| ~ spl40_11
| spl40_18 ),
inference(avatar_split_clause,[],[f12196,f12180,f12129,f12125,f12139,f12135]) ).
fof(f12205,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK6)
| ~ l1_cat_1(sK6)
| spl40_19 ),
inference(resolution,[],[f12186,f12028]) ).
fof(f12206,plain,
( ~ spl40_12
| ~ spl40_13
| ~ spl40_10
| ~ spl40_11
| spl40_19 ),
inference(avatar_split_clause,[],[f12205,f12184,f12129,f12125,f12139,f12135]) ).
fof(f12219,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| spl40_20 ),
inference(resolution,[],[f12190,f12027]) ).
fof(f12220,plain,
( ~ spl40_14
| ~ spl40_15
| ~ spl40_10
| ~ spl40_11
| spl40_20 ),
inference(avatar_split_clause,[],[f12219,f12188,f12129,f12125,f12147,f12143]) ).
fof(f12229,plain,
( ~ v2_cat_1(sK4)
| ~ l1_cat_1(sK4)
| ~ v2_cat_1(sK5)
| ~ l1_cat_1(sK5)
| spl40_21 ),
inference(resolution,[],[f12194,f12028]) ).
fof(f12230,plain,
( ~ spl40_14
| ~ spl40_15
| ~ spl40_10
| ~ spl40_11
| spl40_21 ),
inference(avatar_split_clause,[],[f12229,f12192,f12129,f12125,f12147,f12143]) ).
fof(f12236,plain,
( ~ v2_cat_1(k12_nattra_1(sK4,sK5))
| ~ l1_cat_1(k12_nattra_1(sK4,sK5))
| ~ v2_cat_1(k12_nattra_1(sK4,sK6))
| ~ l1_cat_1(k12_nattra_1(sK4,sK6))
| spl40_6 ),
inference(resolution,[],[f12109,f11968]) ).
fof(f12237,plain,
( ~ spl40_18
| ~ spl40_19
| ~ spl40_20
| ~ spl40_21
| spl40_6 ),
inference(avatar_split_clause,[],[f12236,f12107,f12192,f12188,f12184,f12180]) ).
fof(f12334,plain,
( ~ m2_cat_1(k17_isocat_2(sK4,sK5,sK6),k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,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)
| ~ spl40_16 ),
inference(resolution,[],[f12157,f11969]) ).
fof(f12336,definition,
( spl40_39
<=> m2_cat_1(k17_isocat_2(sK4,sK5,sK6),k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6))) ),
introduced(definition,[new_symbols(definition,[spl40_39])],[avatar_definition]) ).
fof(f12338,plain,
( ~ m2_cat_1(k17_isocat_2(sK4,sK5,sK6),k12_nattra_1(sK4,k11_cat_2(sK5,sK6)),k11_cat_2(k12_nattra_1(sK4,sK5),k12_nattra_1(sK4,sK6)))
| spl40_39 ),
inference(avatar_component_clause,[],[f12336]) ).
fof(f12339,plain,
( ~ spl40_10
| ~ spl40_11
| ~ spl40_14
| ~ spl40_15
| ~ spl40_12
| ~ spl40_13
| ~ spl40_39
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f12334,f12156,f12336,f12139,f12135,f12147,f12143,f12129,f12125]) ).
fof(f12361,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)
| spl40_39 ),
inference(resolution,[],[f12338,f12022]) ).
fof(f12368,plain,
( ~ spl40_12
| ~ spl40_13
| ~ spl40_14
| ~ spl40_15
| ~ spl40_10
| ~ spl40_11
| spl40_39 ),
inference(avatar_split_clause,[],[f12361,f12336,f12129,f12125,f12147,f12143,f12139,f12135]) ).
cnf(s3,plain,
( spl40_3
| ~ spl40_8
| ~ spl40_9
| ~ spl40_10
| ~ spl40_11 ),
inference(sat_conversion,[],[f12132]) ).
cnf(s4,plain,
( spl40_8
| ~ spl40_12
| ~ spl40_13
| ~ spl40_14
| ~ spl40_15 ),
inference(sat_conversion,[],[f12150]) ).
cnf(s5,plain,
spl40_12,
inference(sat_conversion,[],[f12152]) ).
cnf(s6,plain,
( ~ spl40_3
| ~ spl40_4
| ~ spl40_5
| ~ spl40_6
| spl40_16 ),
inference(sat_conversion,[],[f12158]) ).
cnf(s7,plain,
spl40_13,
inference(sat_conversion,[],[f12160]) ).
cnf(s9,plain,
spl40_14,
inference(sat_conversion,[],[f12167]) ).
cnf(s10,plain,
spl40_15,
inference(sat_conversion,[],[f12169]) ).
cnf(s11,plain,
( spl40_9
| ~ spl40_12
| ~ spl40_13
| ~ spl40_14
| ~ spl40_15 ),
inference(sat_conversion,[],[f12171]) ).
cnf(s12,plain,
spl40_10,
inference(sat_conversion,[],[f12173]) ).
cnf(s13,plain,
spl40_11,
inference(sat_conversion,[],[f12175]) ).
cnf(s14,plain,
( spl40_4
| ~ spl40_8
| ~ spl40_9
| ~ spl40_10
| ~ spl40_11 ),
inference(sat_conversion,[],[f12177]) ).
cnf(s15,plain,
( spl40_5
| ~ spl40_18
| ~ spl40_19
| ~ spl40_20
| ~ spl40_21 ),
inference(sat_conversion,[],[f12195]) ).
cnf(s16,plain,
( ~ spl40_10
| ~ spl40_11
| ~ spl40_12
| ~ spl40_13
| spl40_18 ),
inference(sat_conversion,[],[f12197]) ).
cnf(s18,plain,
( ~ spl40_10
| ~ spl40_11
| ~ spl40_12
| ~ spl40_13
| spl40_19 ),
inference(sat_conversion,[],[f12206]) ).
cnf(s21,plain,
( ~ spl40_10
| ~ spl40_11
| ~ spl40_14
| ~ spl40_15
| spl40_20 ),
inference(sat_conversion,[],[f12220]) ).
cnf(s22,plain,
( ~ spl40_10
| ~ spl40_11
| ~ spl40_14
| ~ spl40_15
| spl40_21 ),
inference(sat_conversion,[],[f12230]) ).
cnf(s24,plain,
( spl40_6
| ~ spl40_18
| ~ spl40_19
| ~ spl40_20
| ~ spl40_21 ),
inference(sat_conversion,[],[f12237]) ).
cnf(s42,plain,
( ~ spl40_10
| ~ spl40_11
| ~ spl40_12
| ~ spl40_13
| ~ spl40_14
| ~ spl40_15
| ~ spl40_16
| ~ spl40_39 ),
inference(sat_conversion,[],[f12339]) ).
cnf(s48,plain,
( ~ spl40_10
| ~ spl40_11
| ~ spl40_12
| ~ spl40_13
| ~ spl40_14
| ~ spl40_15
| spl40_39 ),
inference(sat_conversion,[],[f12368]) ).
cnf(s49,plain,
spl40_21,
inference(rat,[],[s22,s10,s12,s13,s9]) ).
cnf(s50,plain,
spl40_20,
inference(rat,[],[s21,s10,s12,s13,s9]) ).
cnf(s53,plain,
spl40_39,
inference(rat,[],[s48,s7,s10,s9,s12,s13,s5]) ).
cnf(s54,plain,
~ spl40_16,
inference(rat,[],[s42,s53,s7,s10,s9,s12,s13,s5]) ).
cnf(s55,plain,
spl40_19,
inference(rat,[],[s18,s7,s12,s13,s5]) ).
cnf(s56,plain,
spl40_18,
inference(rat,[],[s16,s7,s12,s13,s5]) ).
cnf(s57,plain,
spl40_9,
inference(rat,[],[s11,s10,s9,s7,s5]) ).
cnf(s58,plain,
spl40_6,
inference(rat,[],[s24,s49,s50,s55,s56]) ).
cnf(s59,plain,
spl40_5,
inference(rat,[],[s15,s49,s50,s55,s56]) ).
cnf(s62,plain,
spl40_8,
inference(rat,[],[s4,s10,s9,s7,s5]) ).
cnf(s63,plain,
spl40_4,
inference(rat,[],[s14,s13,s12,s57,s62]) ).
cnf(s64,plain,
~ spl40_3,
inference(rat,[],[s6,s54,s58,s59,s63]) ).
cnf(s65,plain,
$false,
inference(rat,[],[s3,s13,s12,s57,s62,s64]) ).
fof(f12369,plain,
$false,
inference(avatar_sat_refutation,[],[s65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CAT032+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n005.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 21:23:18 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.76/2.92 % (1196472)Detected formulas, will run a generic FOF schedule.
% 11.76/2.92 % (1196480)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3519461473:i=109:sd=1:ins=1:gsp=on:ss=axioms_2994 on theBenchmark for (2994ds/109Mi)
% 11.76/2.92 % (1196477)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=1251529640:i=141193_2994 on theBenchmark for (2994ds/141193Mi)
% 11.76/2.92 % (1196478)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=1134501411:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2994 on theBenchmark for (2994ds/134677Mi)
% 11.76/2.92 % (1196479)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=2236343920:i=141695:sd=1:nm=32:gsp=on:ss=included_2994 on theBenchmark for (2994ds/141695Mi)
% 11.76/2.92 % (1196480)Refutation not found, incomplete strategy
% 11.76/2.92 % (1196480)------------------------------
% 11.76/2.92 % (1196480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.92 % (1196480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.92 % (1196480)CaDiCaL version: 2.1.3
% 11.76/2.92 % (1196480)Termination reason: Refutation not found, incomplete strategy
% 11.76/2.92 % (1196480)Time elapsed: 0.038 s
% 11.76/2.92 % (1196480)Peak memory usage: 104 MB
% 11.76/2.92 % (1196480)Instructions burned: 70 (million)
% 11.76/2.92 % (1196482)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3241380980:s2a=on:i=139:gtg=position_2994 on theBenchmark for (2994ds/139Mi)
% 11.76/2.92 % (1196483)dis-21_1_sil=8000:lcm=predicate:random_seed=1788748274:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2994 on theBenchmark for (2994ds/129Mi)
% 11.76/2.92 % (1196481)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2078737928:i=119:av=off:ss=axioms_2994 on theBenchmark for (2994ds/119Mi)
% 11.76/2.92 % (1196482)Instruction limit reached!
% 11.76/2.92 % (1196482)------------------------------
% 11.76/2.92 % (1196482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.92 % (1196482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.92 % (1196482)CaDiCaL version: 2.1.3
% 11.76/2.92 % (1196482)Termination reason: Instruction limit
% 11.76/2.92 % (1196482)Termination phase: Property scanning
% 11.76/2.92 % (1196482)Time elapsed: 0.060 s
% 11.76/2.92 % (1196482)Peak memory usage: 100 MB
% 11.76/2.92 % (1196482)Instructions burned: 142 (million)
% 11.76/2.92 % (1196481)Instruction limit reached!
% 11.76/2.92 % (1196481)------------------------------
% 11.76/2.92 % (1196481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.92 % (1196481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.92 % (1196481)CaDiCaL version: 2.1.3
% 11.76/2.92 % (1196481)Termination reason: Instruction limit
% 11.76/2.92 % (1196481)Termination phase: Property scanning
% 11.76/2.92 % (1196481)Time elapsed: 0.088 s
% 11.76/2.92 % (1196481)Peak memory usage: 103 MB
% 11.76/2.92 % (1196481)Instructions burned: 120 (million)
% 11.76/2.92 % (1196483)Instruction limit reached!
% 11.76/2.92 % (1196483)------------------------------
% 11.76/2.92 % (1196483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.92 % (1196483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.92 % (1196483)CaDiCaL version: 2.1.3
% 11.76/2.92 % (1196483)Termination reason: Instruction limit
% 11.76/2.92 % (1196483)Termination phase: Preprocessing 1
% 11.76/2.92 % (1196483)Time elapsed: 0.098 s
% 11.76/2.92 % (1196483)Peak memory usage: 101 MB
% 11.76/2.92 % (1196483)Instructions burned: 130 (million)
% 11.76/2.92 % (1196480)------------------------------
% 11.76/2.92 % (1196480)------------------------------
% 11.76/2.92 % (1196491)lrs+10_1_sil=8000:sp=occurrence:random_seed=390286801:i=285:sd=3:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/285Mi)
% 11.76/2.92 % (1196493)lrs+1011_1_sil=32000:sp=occurrence:random_seed=735692281:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi)
% 11.76/2.92 % (1196492)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1149179859:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 11.76/2.92 % (1196494)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=2352854732:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 17.79/3.77 % (1196493)Refutation not found, incomplete strategy
% 17.79/3.77 % (1196493)------------------------------
% 17.79/3.77 % (1196493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196493)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196493)Termination reason: Refutation not found, incomplete strategy
% 17.79/3.77 % (1196493)Time elapsed: 0.057 s
% 17.79/3.77 % (1196493)Peak memory usage: 105 MB
% 17.79/3.77 % (1196493)Instructions burned: 67 (million)
% 17.79/3.77 % (1196492)Instruction limit reached!
% 17.79/3.77 % (1196492)------------------------------
% 17.79/3.77 % (1196492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196492)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196492)Termination reason: Instruction limit
% 17.79/3.77 % (1196492)Termination phase: SInE selection
% 17.79/3.77 % (1196492)Time elapsed: 0.071 s
% 17.79/3.77 % (1196492)Peak memory usage: 100 MB
% 17.79/3.77 % (1196492)Instructions burned: 157 (million)
% 17.79/3.77 % (1196494)Instruction limit reached!
% 17.79/3.77 % (1196494)------------------------------
% 17.79/3.77 % (1196494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196494)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196494)Termination reason: Instruction limit
% 17.79/3.77 % (1196494)Termination phase: Preprocessing 1
% 17.79/3.77 % (1196494)Time elapsed: 0.079 s
% 17.79/3.77 % (1196494)Peak memory usage: 101 MB
% 17.79/3.77 % (1196494)Instructions burned: 249 (million)
% 17.79/3.77 % (1196491)Instruction limit reached!
% 17.79/3.77 % (1196491)------------------------------
% 17.79/3.77 % (1196491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196491)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196491)Termination reason: Instruction limit
% 17.79/3.77 % (1196491)Termination phase: Saturation
% 17.79/3.77 % (1196491)Time elapsed: 0.207 s
% 17.79/3.77 % (1196491)Peak memory usage: 107 MB
% 17.79/3.77 % (1196491)Instructions burned: 287 (million)
% 17.79/3.77 % (1196499)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2403186927:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 17.79/3.77 % (1196500)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=144466846:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 17.79/3.77 % (1196493)------------------------------
% 17.79/3.77 % (1196493)------------------------------
% 17.79/3.77 % (1196501)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3647297719:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 17.79/3.77 % (1196499)Instruction limit reached!
% 17.79/3.77 % (1196499)------------------------------
% 17.79/3.77 % (1196499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196499)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196499)Termination reason: Instruction limit
% 17.79/3.77 % (1196499)Termination phase: Saturation
% 17.79/3.77 % (1196499)Time elapsed: 0.187 s
% 17.79/3.77 % (1196499)Peak memory usage: 107 MB
% 17.79/3.77 % (1196499)Instructions burned: 294 (million)
% 17.79/3.77 % (1196501)Instruction limit reached!
% 17.79/3.77 % (1196501)------------------------------
% 17.79/3.77 % (1196501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196501)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196501)Termination reason: Instruction limit
% 17.79/3.77 % (1196501)Termination phase: Preprocessing 3
% 17.79/3.77 % (1196501)Time elapsed: 0.095 s
% 17.79/3.77 % (1196501)Peak memory usage: 103 MB
% 17.79/3.77 % (1196501)Instructions burned: 115 (million)
% 17.79/3.77 % (1196505)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1401268049:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 17.79/3.77 % (1196506)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2321531506:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 17.79/3.77 % (1196507)lrs+10_1_sil=8000:sp=occurrence:random_seed=2767826806:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 17.79/3.77 % (1196505)Instruction limit reached!
% 17.79/3.77 % (1196505)------------------------------
% 17.79/3.77 % (1196505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196505)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196505)Termination reason: Instruction limit
% 17.79/3.77 % (1196505)Termination phase: Preprocessing 2
% 17.79/3.77 % (1196505)Time elapsed: 0.104 s
% 17.79/3.77 % (1196505)Peak memory usage: 107 MB
% 17.79/3.77 % (1196505)Instructions burned: 128 (million)
% 17.79/3.77 % (1196506)Instruction limit reached!
% 17.79/3.77 % (1196506)------------------------------
% 17.79/3.77 % (1196506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196506)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196506)Termination reason: Instruction limit
% 17.79/3.77 % (1196506)Termination phase: Property scanning
% 17.79/3.77 % (1196506)Time elapsed: 0.049 s
% 17.79/3.77 % (1196506)Peak memory usage: 100 MB
% 17.79/3.77 % (1196506)Instructions burned: 116 (million)
% 17.79/3.77 % (1196512)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3187860541:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 17.79/3.77 % (1196511)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2474301123:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 17.79/3.77 % (1196511)Refutation not found, incomplete strategy
% 17.79/3.77 % (1196511)------------------------------
% 17.79/3.77 % (1196511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196511)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196511)Termination reason: Refutation not found, incomplete strategy
% 17.79/3.77 % (1196511)Time elapsed: 0.113 s
% 17.79/3.77 % (1196511)Peak memory usage: 107 MB
% 17.79/3.77 % (1196511)Instructions burned: 167 (million)
% 17.79/3.77 % (1196507)Instruction limit reached!
% 17.79/3.77 % (1196507)------------------------------
% 17.79/3.77 % (1196507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196507)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196507)Termination reason: Instruction limit
% 17.79/3.77 % (1196507)Termination phase: Saturation
% 17.79/3.77 % (1196507)Time elapsed: 0.496 s
% 17.79/3.77 % (1196507)Peak memory usage: 120 MB
% 17.79/3.77 % (1196507)Instructions burned: 908 (million)
% 17.79/3.77 % (1196511)------------------------------
% 17.79/3.77 % (1196511)------------------------------
% 17.79/3.77 % (1196515)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4187556284:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 17.79/3.77 % (1196500)Instruction limit reached!
% 17.79/3.77 % (1196500)------------------------------
% 17.79/3.77 % (1196500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196500)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196500)Termination reason: Instruction limit
% 17.79/3.77 % (1196500)Termination phase: Saturation
% 17.79/3.77 % (1196500)Time elapsed: 0.956 s
% 17.79/3.77 % (1196500)Peak memory usage: 257 MB
% 17.79/3.77 % (1196500)Instructions burned: 2350 (million)
% 17.79/3.77 % (1196516)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3256211702:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 17.79/3.77 % (1196515)Instruction limit reached!
% 17.79/3.77 % (1196515)------------------------------
% 17.79/3.77 % (1196515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196515)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196515)Termination reason: Instruction limit
% 17.79/3.77 % (1196515)Termination phase: Function definition elimination
% 17.79/3.77 % (1196515)Time elapsed: 0.100 s
% 17.79/3.77 % (1196515)Peak memory usage: 104 MB
% 17.79/3.77 % (1196515)Instructions burned: 134 (million)
% 17.79/3.77 % (1196519)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3243830219:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 17.79/3.77 % (1196520)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3221126616:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 17.79/3.77 % (1196520)Instruction limit reached!
% 17.79/3.77 % (1196520)------------------------------
% 17.79/3.77 % (1196520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196520)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196520)Termination reason: Instruction limit
% 17.79/3.77 % (1196520)Termination phase: Property scanning
% 17.79/3.77 % (1196520)Time elapsed: 0.056 s
% 17.79/3.77 % (1196520)Peak memory usage: 100 MB
% 17.79/3.77 % (1196520)Instructions burned: 127 (million)
% 17.79/3.77 % (1196516)Instruction limit reached!
% 17.79/3.77 % (1196516)------------------------------
% 17.79/3.77 % (1196516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196516)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196516)Termination reason: Instruction limit
% 17.79/3.77 % (1196516)Termination phase: Property scanning
% 17.79/3.77 % (1196516)Time elapsed: 0.367 s
% 17.79/3.77 % (1196516)Peak memory usage: 116 MB
% 17.79/3.77 % (1196516)Instructions burned: 593 (million)
% 17.79/3.77 % (1196523)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=28277521:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 17.79/3.77 % (1196523)Instruction limit reached!
% 17.79/3.77 % (1196523)------------------------------
% 17.79/3.77 % (1196523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196523)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196523)Termination reason: Instruction limit
% 17.79/3.77 % (1196523)Termination phase: Property scanning
% 17.79/3.77 % (1196523)Time elapsed: 0.058 s
% 17.79/3.77 % (1196523)Peak memory usage: 100 MB
% 17.79/3.77 % (1196523)Instructions burned: 134 (million)
% 17.79/3.77 % (1196524)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2881120586:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/141Mi)
% 17.79/3.77 % (1196524)Instruction limit reached!
% 17.79/3.77 % (1196524)------------------------------
% 17.79/3.77 % (1196524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.79/3.77 % (1196524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/3.77 % (1196524)CaDiCaL version: 2.1.3
% 17.79/3.77 % (1196524)Termination reason: Instruction limit
% 17.79/3.77 % (1196524)Termination phase: Saturation
% 17.79/3.77 % (1196524)Time elapsed: 0.095 s
% 17.79/3.77 % (1196524)Peak memory usage: 105 MB
% 17.79/3.77 % (1196524)Instructions burned: 141 (million)
% 17.79/3.77 % (1196526)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1223973473:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 17.79/3.77 % (1196526)First to succeed.
% 17.79/3.77 % (1196526)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1196472"
% 17.79/3.77 % (1196529)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4214352998:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi)
% 17.79/3.77 % (1196526)Refutation found. Thanks to Tanya!
% 17.79/3.77 % SZS status Theorem for theBenchmark
% 17.79/3.77 % SZS output start Proof for theBenchmark
% See solution above
% 19.11/3.97 % (1196526)------------------------------
% 19.11/3.97 % (1196526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.11/3.97 % (1196526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.11/3.97 % (1196526)CaDiCaL version: 2.1.3
% 19.11/3.97 % (1196526)Termination reason: Refutation
% 19.11/3.97 % (1196526)Time elapsed: 0.073 s
% 19.11/3.97 % (1196526)Peak memory usage: 106 MB
% 19.11/3.97 % (1196526)Instructions burned: 87 (million)
% 19.11/3.97 % (1196526)------------------------------
% 19.11/3.97 % (1196526)------------------------------
% 19.11/3.97 % (1196472)Success in time 3.115 s
% 19.11/3.97 % Vampire exiting
%------------------------------------------------------------------------------