%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CAT025+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:37:00 AM UTC 2026
% Result : Theorem 181.59s 30.27s
% Output : Refutation 181.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 16
% Syntax : Number of formulae : 136 ( 30 unt; 9 def)
% Number of atoms : 489 ( 0 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 535 ( 182 ~; 274 |; 52 &)
% ( 12 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 10 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 94 ( 0 sgn 85 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3684,axiom,
! [X0,X1] :
( ( v2_cat_1(X0)
& l1_cat_1(X0)
& v2_cat_1(X1)
& l1_cat_1(X1) )
=> ( v1_cat_1(k11_cat_2(X0,X1))
& v2_cat_1(k11_cat_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+237.ax',fc2_cat_2) ).
fof(f3782,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/Axioms/SET007/SET007+237.ax',dt_k11_cat_2) ).
fof(f3905,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/Axioms/SET007/SET007+299.ax',dt_k12_nattra_1) ).
fof(f3929,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/Axioms/SET007/SET007+322.ax',d4_isocat_1) ).
fof(f4001,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/sandbox/benchmark/theBenchmark.p',dt_k7_isocat_2) ).
fof(f4055,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/sandbox/benchmark/theBenchmark.p',t33_isocat_2) ).
fof(f4056,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/sandbox/benchmark/theBenchmark.p',t34_isocat_2) ).
fof(f4057,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)],[f4056]) ).
fof(f8078,plain,
! [X0,X1] :
( ( v1_cat_1(k11_cat_2(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(ennf_transformation,[],[f3684]) ).
fof(f8079,plain,
! [X0,X1] :
( ( v1_cat_1(k11_cat_2(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(flattening,[],[f8078]) ).
fof(f8248,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,[],[f3782]) ).
fof(f8249,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,[],[f8248]) ).
fof(f8470,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,[],[f3905]) ).
fof(f8471,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,[],[f8470]) ).
fof(f8514,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,[],[f3929]) ).
fof(f8515,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,[],[f8514]) ).
fof(f8650,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,[],[f4001]) ).
fof(f8651,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,[],[f8650]) ).
fof(f8750,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,[],[f4055]) ).
fof(f8751,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,[],[f8750]) ).
fof(f8752,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,[],[f4057]) ).
fof(f8753,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,[],[f8752]) ).
fof(f16126,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| v2_cat_1(k11_cat_2(X0,X1)) ),
inference(cnf_transformation,[],[f8079]) ).
fof(f16308,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| l1_cat_1(k11_cat_2(X0,X1)) ),
inference(cnf_transformation,[],[f8249]) ).
fof(f16584,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| l1_cat_1(k12_nattra_1(X0,X1)) ),
inference(cnf_transformation,[],[f8471]) ).
fof(f16585,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| v2_cat_1(k12_nattra_1(X0,X1)) ),
inference(cnf_transformation,[],[f8471]) ).
fof(f16645,plain,
! [X2,X0,X1] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ v8_cat_1(X2,X0,X1)
| ~ m2_cat_1(X2,X0,X1)
| r1_isocat_1(X0,X1) ),
inference(cnf_transformation,[],[f8515]) ).
fof(f16732,plain,
! [X2,X0,X1] :
( ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| 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))) ),
inference(cnf_transformation,[],[f8651]) ).
fof(f16820,plain,
! [X2,X0,X1] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X2)
| ~ v2_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))) ),
inference(cnf_transformation,[],[f8751]) ).
fof(f16821,plain,
l1_cat_1(sK1376),
inference(cnf_transformation,[],[f8753]) ).
fof(f16822,plain,
v2_cat_1(sK1376),
inference(cnf_transformation,[],[f8753]) ).
fof(f16823,plain,
~ r1_isocat_1(k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376))),
inference(cnf_transformation,[],[f8753]) ).
fof(f16824,plain,
l1_cat_1(sK1375),
inference(cnf_transformation,[],[f8753]) ).
fof(f16825,plain,
v2_cat_1(sK1375),
inference(cnf_transformation,[],[f8753]) ).
fof(f16826,plain,
l1_cat_1(sK1374),
inference(cnf_transformation,[],[f8753]) ).
fof(f16827,plain,
v2_cat_1(sK1374),
inference(cnf_transformation,[],[f8753]) ).
fof(f26920,plain,
! [X0,X1] :
( ~ v2_cat_1(k11_cat_2(X0,X1))
| v2_cat_1(X1)
| l1_cat_1(X0)
| v2_cat_1(X0)
| l1_cat_1(X1) ),
inference(consistent_polarity_flipping,[],[f16126]) ).
fof(f27102,plain,
! [X0,X1] :
( ~ l1_cat_1(k11_cat_2(X0,X1))
| v2_cat_1(X1)
| l1_cat_1(X0)
| v2_cat_1(X0)
| l1_cat_1(X1) ),
inference(consistent_polarity_flipping,[],[f16308]) ).
fof(f27371,plain,
! [X0,X1] :
( ~ v2_cat_1(k12_nattra_1(X0,X1))
| v2_cat_1(X1)
| l1_cat_1(X0)
| v2_cat_1(X0)
| l1_cat_1(X1) ),
inference(consistent_polarity_flipping,[],[f16585]) ).
fof(f27372,plain,
! [X0,X1] :
( ~ l1_cat_1(k12_nattra_1(X0,X1))
| v2_cat_1(X1)
| l1_cat_1(X0)
| v2_cat_1(X0)
| l1_cat_1(X1) ),
inference(consistent_polarity_flipping,[],[f16584]) ).
fof(f27429,plain,
! [X2,X0,X1] :
( ~ r1_isocat_1(X0,X1)
| v2_cat_1(X0)
| l1_cat_1(X1)
| v2_cat_1(X1)
| ~ v8_cat_1(X2,X0,X1)
| m2_cat_1(X2,X0,X1)
| l1_cat_1(X0) ),
inference(consistent_polarity_flipping,[],[f16645]) ).
fof(f27518,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(X2)
| l1_cat_1(X1)
| v2_cat_1(X1)
| l1_cat_1(X0)
| v2_cat_1(X0)
| l1_cat_1(X2) ),
inference(consistent_polarity_flipping,[],[f16732]) ).
fof(f27604,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(X0)
| l1_cat_1(X1)
| v2_cat_1(X1)
| l1_cat_1(X2)
| v2_cat_1(X2)
| l1_cat_1(X0) ),
inference(consistent_polarity_flipping,[],[f16820]) ).
fof(f27605,plain,
~ v2_cat_1(sK1374),
inference(consistent_polarity_flipping,[],[f16827]) ).
fof(f27606,plain,
~ l1_cat_1(sK1374),
inference(consistent_polarity_flipping,[],[f16826]) ).
fof(f27607,plain,
~ v2_cat_1(sK1375),
inference(consistent_polarity_flipping,[],[f16825]) ).
fof(f27608,plain,
~ l1_cat_1(sK1375),
inference(consistent_polarity_flipping,[],[f16824]) ).
fof(f27609,plain,
r1_isocat_1(k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376))),
inference(consistent_polarity_flipping,[],[f16823]) ).
fof(f27610,plain,
~ v2_cat_1(sK1376),
inference(consistent_polarity_flipping,[],[f16822]) ).
fof(f27611,plain,
~ l1_cat_1(sK1376),
inference(consistent_polarity_flipping,[],[f16821]) ).
fof(f105698,definition,
( spl1377_5301
<=> l1_cat_1(k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376)) ),
introduced(definition,[new_symbols(definition,[spl1377_5301])],[avatar_definition]) ).
fof(f105700,plain,
( l1_cat_1(k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376))
| ~ spl1377_5301 ),
inference(avatar_component_clause,[],[f105698]) ).
fof(f105706,definition,
( spl1377_5303
<=> v2_cat_1(k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376))) ),
introduced(definition,[new_symbols(definition,[spl1377_5303])],[avatar_definition]) ).
fof(f105708,plain,
( v2_cat_1(k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| ~ spl1377_5303 ),
inference(avatar_component_clause,[],[f105706]) ).
fof(f105710,definition,
( spl1377_5304
<=> l1_cat_1(k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376))) ),
introduced(definition,[new_symbols(definition,[spl1377_5304])],[avatar_definition]) ).
fof(f105712,plain,
( l1_cat_1(k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| ~ spl1377_5304 ),
inference(avatar_component_clause,[],[f105710]) ).
fof(f105714,definition,
( spl1377_5305
<=> v2_cat_1(k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376)) ),
introduced(definition,[new_symbols(definition,[spl1377_5305])],[avatar_definition]) ).
fof(f105716,plain,
( v2_cat_1(k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376))
| ~ spl1377_5305 ),
inference(avatar_component_clause,[],[f105714]) ).
fof(f182013,plain,
! [X0] :
( v2_cat_1(k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376))
| l1_cat_1(k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| v2_cat_1(k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| ~ v8_cat_1(X0,k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| m2_cat_1(X0,k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| l1_cat_1(k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376)) ),
inference(resolution,[],[f27429,f27609]) ).
fof(f182015,definition,
( spl1377_7941
<=> ! [X0] :
( ~ v8_cat_1(X0,k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| m2_cat_1(X0,k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376))) ) ),
introduced(definition,[new_symbols(definition,[spl1377_7941])],[avatar_definition]) ).
fof(f182016,plain,
( ! [X0] :
( ~ v8_cat_1(X0,k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| m2_cat_1(X0,k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376))) )
| ~ spl1377_7941 ),
inference(avatar_component_clause,[],[f182015]) ).
fof(f182017,plain,
( spl1377_5301
| spl1377_7941
| spl1377_5303
| spl1377_5304
| spl1377_5305 ),
inference(avatar_split_clause,[],[f182013,f105714,f105710,f105706,f182015,f105698]) ).
fof(f565176,plain,
( m2_cat_1(k7_isocat_2(sK1374,sK1375,sK1376),k12_nattra_1(k11_cat_2(sK1374,sK1375),sK1376),k12_nattra_1(sK1374,k12_nattra_1(sK1375,sK1376)))
| v2_cat_1(sK1374)
| l1_cat_1(sK1375)
| v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| v2_cat_1(sK1376)
| l1_cat_1(sK1374)
| ~ spl1377_7941 ),
inference(resolution,[],[f182016,f27604]) ).
fof(f565179,plain,
( v2_cat_1(sK1374)
| l1_cat_1(sK1375)
| v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| v2_cat_1(sK1376)
| l1_cat_1(sK1374)
| ~ spl1377_7941 ),
inference(forward_subsumption_resolution,[],[f565176,f27518]) ).
fof(f565186,plain,
( l1_cat_1(sK1375)
| v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| v2_cat_1(sK1376)
| l1_cat_1(sK1374)
| ~ spl1377_7941 ),
inference(forward_subsumption_resolution,[],[f565179,f27605]) ).
fof(f565192,plain,
( v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| v2_cat_1(sK1376)
| l1_cat_1(sK1374)
| ~ spl1377_7941 ),
inference(forward_subsumption_resolution,[],[f565186,f27608]) ).
fof(f565193,plain,
( l1_cat_1(sK1376)
| v2_cat_1(sK1376)
| l1_cat_1(sK1374)
| ~ spl1377_7941 ),
inference(forward_subsumption_resolution,[],[f565192,f27607]) ).
fof(f565194,plain,
( v2_cat_1(sK1376)
| l1_cat_1(sK1374)
| ~ spl1377_7941 ),
inference(forward_subsumption_resolution,[],[f565193,f27611]) ).
fof(f565195,plain,
( l1_cat_1(sK1374)
| ~ spl1377_7941 ),
inference(forward_subsumption_resolution,[],[f565194,f27610]) ).
fof(f565196,plain,
( $false
| ~ spl1377_7941 ),
inference(forward_subsumption_resolution,[],[f565195,f27606]) ).
fof(f565197,plain,
~ spl1377_7941,
inference(avatar_contradiction_clause,[],[f565196]) ).
fof(f565209,definition,
( spl1377_20048
<=> v2_cat_1(k11_cat_2(sK1374,sK1375)) ),
introduced(definition,[new_symbols(definition,[spl1377_20048])],[avatar_definition]) ).
fof(f565211,plain,
( v2_cat_1(k11_cat_2(sK1374,sK1375))
| ~ spl1377_20048 ),
inference(avatar_component_clause,[],[f565209]) ).
fof(f565213,definition,
( spl1377_20049
<=> l1_cat_1(k11_cat_2(sK1374,sK1375)) ),
introduced(definition,[new_symbols(definition,[spl1377_20049])],[avatar_definition]) ).
fof(f565215,plain,
( l1_cat_1(k11_cat_2(sK1374,sK1375))
| ~ spl1377_20049 ),
inference(avatar_component_clause,[],[f565213]) ).
fof(f565283,definition,
( spl1377_20055
<=> l1_cat_1(k12_nattra_1(sK1375,sK1376)) ),
introduced(definition,[new_symbols(definition,[spl1377_20055])],[avatar_definition]) ).
fof(f565285,plain,
( l1_cat_1(k12_nattra_1(sK1375,sK1376))
| ~ spl1377_20055 ),
inference(avatar_component_clause,[],[f565283]) ).
fof(f565287,definition,
( spl1377_20056
<=> v2_cat_1(k12_nattra_1(sK1375,sK1376)) ),
introduced(definition,[new_symbols(definition,[spl1377_20056])],[avatar_definition]) ).
fof(f565289,plain,
( v2_cat_1(k12_nattra_1(sK1375,sK1376))
| ~ spl1377_20056 ),
inference(avatar_component_clause,[],[f565287]) ).
fof(f566081,plain,
( v2_cat_1(k12_nattra_1(sK1375,sK1376))
| l1_cat_1(sK1374)
| v2_cat_1(sK1374)
| l1_cat_1(k12_nattra_1(sK1375,sK1376))
| ~ spl1377_5303 ),
inference(resolution,[],[f105708,f27371]) ).
fof(f566087,plain,
( v2_cat_1(k12_nattra_1(sK1375,sK1376))
| v2_cat_1(sK1374)
| l1_cat_1(k12_nattra_1(sK1375,sK1376))
| ~ spl1377_5303 ),
inference(forward_subsumption_resolution,[],[f566081,f27606]) ).
fof(f566088,plain,
( v2_cat_1(k12_nattra_1(sK1375,sK1376))
| l1_cat_1(k12_nattra_1(sK1375,sK1376))
| ~ spl1377_5303 ),
inference(forward_subsumption_resolution,[],[f566087,f27605]) ).
fof(f566089,plain,
( spl1377_20055
| spl1377_20056
| ~ spl1377_5303 ),
inference(avatar_split_clause,[],[f566088,f105706,f565287,f565283]) ).
fof(f566617,plain,
( v2_cat_1(sK1376)
| l1_cat_1(sK1375)
| v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| ~ spl1377_20055 ),
inference(resolution,[],[f565285,f27372]) ).
fof(f566619,plain,
( l1_cat_1(sK1375)
| v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| ~ spl1377_20055 ),
inference(forward_subsumption_resolution,[],[f566617,f27610]) ).
fof(f566620,plain,
( v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| ~ spl1377_20055 ),
inference(forward_subsumption_resolution,[],[f566619,f27608]) ).
fof(f566621,plain,
( l1_cat_1(sK1376)
| ~ spl1377_20055 ),
inference(forward_subsumption_resolution,[],[f566620,f27607]) ).
fof(f566622,plain,
( $false
| ~ spl1377_20055 ),
inference(forward_subsumption_resolution,[],[f566621,f27611]) ).
fof(f566623,plain,
~ spl1377_20055,
inference(avatar_contradiction_clause,[],[f566622]) ).
fof(f567032,plain,
( v2_cat_1(sK1376)
| l1_cat_1(k11_cat_2(sK1374,sK1375))
| v2_cat_1(k11_cat_2(sK1374,sK1375))
| l1_cat_1(sK1376)
| ~ spl1377_5305 ),
inference(resolution,[],[f105716,f27371]) ).
fof(f567038,plain,
( l1_cat_1(k11_cat_2(sK1374,sK1375))
| v2_cat_1(k11_cat_2(sK1374,sK1375))
| l1_cat_1(sK1376)
| ~ spl1377_5305 ),
inference(forward_subsumption_resolution,[],[f567032,f27610]) ).
fof(f567061,plain,
( l1_cat_1(k11_cat_2(sK1374,sK1375))
| v2_cat_1(k11_cat_2(sK1374,sK1375))
| ~ spl1377_5305 ),
inference(forward_subsumption_resolution,[],[f567038,f27611]) ).
fof(f567062,plain,
( spl1377_20048
| spl1377_20049
| ~ spl1377_5305 ),
inference(avatar_split_clause,[],[f567061,f105714,f565213,f565209]) ).
fof(f567064,plain,
( v2_cat_1(sK1376)
| l1_cat_1(k11_cat_2(sK1374,sK1375))
| v2_cat_1(k11_cat_2(sK1374,sK1375))
| l1_cat_1(sK1376)
| ~ spl1377_5301 ),
inference(resolution,[],[f105700,f27372]) ).
fof(f567066,plain,
( l1_cat_1(k11_cat_2(sK1374,sK1375))
| v2_cat_1(k11_cat_2(sK1374,sK1375))
| l1_cat_1(sK1376)
| ~ spl1377_5301 ),
inference(forward_subsumption_resolution,[],[f567064,f27610]) ).
fof(f567067,plain,
( l1_cat_1(k11_cat_2(sK1374,sK1375))
| v2_cat_1(k11_cat_2(sK1374,sK1375))
| ~ spl1377_5301 ),
inference(forward_subsumption_resolution,[],[f567066,f27611]) ).
fof(f567068,plain,
( spl1377_20048
| spl1377_20049
| ~ spl1377_5301 ),
inference(avatar_split_clause,[],[f567067,f105698,f565213,f565209]) ).
fof(f567127,plain,
( v2_cat_1(sK1375)
| l1_cat_1(sK1374)
| v2_cat_1(sK1374)
| l1_cat_1(sK1375)
| ~ spl1377_20048 ),
inference(resolution,[],[f565211,f26920]) ).
fof(f567153,plain,
( l1_cat_1(sK1374)
| v2_cat_1(sK1374)
| l1_cat_1(sK1375)
| ~ spl1377_20048 ),
inference(forward_subsumption_resolution,[],[f567127,f27607]) ).
fof(f567154,plain,
( v2_cat_1(sK1374)
| l1_cat_1(sK1375)
| ~ spl1377_20048 ),
inference(forward_subsumption_resolution,[],[f567153,f27606]) ).
fof(f567155,plain,
( l1_cat_1(sK1375)
| ~ spl1377_20048 ),
inference(forward_subsumption_resolution,[],[f567154,f27605]) ).
fof(f567156,plain,
( $false
| ~ spl1377_20048 ),
inference(forward_subsumption_resolution,[],[f567155,f27608]) ).
fof(f567157,plain,
~ spl1377_20048,
inference(avatar_contradiction_clause,[],[f567156]) ).
fof(f568025,plain,
( v2_cat_1(sK1375)
| l1_cat_1(sK1374)
| v2_cat_1(sK1374)
| l1_cat_1(sK1375)
| ~ spl1377_20049 ),
inference(resolution,[],[f565215,f27102]) ).
fof(f568027,plain,
( l1_cat_1(sK1374)
| v2_cat_1(sK1374)
| l1_cat_1(sK1375)
| ~ spl1377_20049 ),
inference(forward_subsumption_resolution,[],[f568025,f27607]) ).
fof(f568028,plain,
( v2_cat_1(sK1374)
| l1_cat_1(sK1375)
| ~ spl1377_20049 ),
inference(forward_subsumption_resolution,[],[f568027,f27606]) ).
fof(f568029,plain,
( l1_cat_1(sK1375)
| ~ spl1377_20049 ),
inference(forward_subsumption_resolution,[],[f568028,f27605]) ).
fof(f568030,plain,
( $false
| ~ spl1377_20049 ),
inference(forward_subsumption_resolution,[],[f568029,f27608]) ).
fof(f568031,plain,
~ spl1377_20049,
inference(avatar_contradiction_clause,[],[f568030]) ).
fof(f568033,plain,
( v2_cat_1(k12_nattra_1(sK1375,sK1376))
| l1_cat_1(sK1374)
| v2_cat_1(sK1374)
| l1_cat_1(k12_nattra_1(sK1375,sK1376))
| ~ spl1377_5304 ),
inference(resolution,[],[f105712,f27372]) ).
fof(f568035,plain,
( v2_cat_1(k12_nattra_1(sK1375,sK1376))
| v2_cat_1(sK1374)
| l1_cat_1(k12_nattra_1(sK1375,sK1376))
| ~ spl1377_5304 ),
inference(forward_subsumption_resolution,[],[f568033,f27606]) ).
fof(f568036,plain,
( v2_cat_1(k12_nattra_1(sK1375,sK1376))
| l1_cat_1(k12_nattra_1(sK1375,sK1376))
| ~ spl1377_5304 ),
inference(forward_subsumption_resolution,[],[f568035,f27605]) ).
fof(f568037,plain,
( spl1377_20055
| spl1377_20056
| ~ spl1377_5304 ),
inference(avatar_split_clause,[],[f568036,f105710,f565287,f565283]) ).
fof(f568324,plain,
( v2_cat_1(sK1376)
| l1_cat_1(sK1375)
| v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| ~ spl1377_20056 ),
inference(resolution,[],[f565289,f27371]) ).
fof(f568330,plain,
( l1_cat_1(sK1375)
| v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| ~ spl1377_20056 ),
inference(forward_subsumption_resolution,[],[f568324,f27610]) ).
fof(f568353,plain,
( v2_cat_1(sK1375)
| l1_cat_1(sK1376)
| ~ spl1377_20056 ),
inference(forward_subsumption_resolution,[],[f568330,f27608]) ).
fof(f568354,plain,
( l1_cat_1(sK1376)
| ~ spl1377_20056 ),
inference(forward_subsumption_resolution,[],[f568353,f27607]) ).
fof(f568355,plain,
( $false
| ~ spl1377_20056 ),
inference(forward_subsumption_resolution,[],[f568354,f27611]) ).
fof(f568356,plain,
~ spl1377_20056,
inference(avatar_contradiction_clause,[],[f568355]) ).
cnf(s7065,plain,
( spl1377_5301
| spl1377_5303
| spl1377_5304
| spl1377_5305
| spl1377_7941 ),
inference(sat_conversion,[],[f182017]) ).
cnf(s19093,plain,
~ spl1377_7941,
inference(sat_conversion,[],[f565197]) ).
cnf(s19241,plain,
( ~ spl1377_5303
| spl1377_20055
| spl1377_20056 ),
inference(sat_conversion,[],[f566089]) ).
cnf(s19254,plain,
~ spl1377_20055,
inference(sat_conversion,[],[f566623]) ).
cnf(s19529,plain,
( ~ spl1377_5305
| spl1377_20048
| spl1377_20049 ),
inference(sat_conversion,[],[f567062]) ).
cnf(s19531,plain,
( ~ spl1377_5301
| spl1377_20048
| spl1377_20049 ),
inference(sat_conversion,[],[f567068]) ).
cnf(s19540,plain,
~ spl1377_20048,
inference(sat_conversion,[],[f567157]) ).
cnf(s19686,plain,
~ spl1377_20049,
inference(sat_conversion,[],[f568031]) ).
cnf(s19688,plain,
( ~ spl1377_5304
| spl1377_20055
| spl1377_20056 ),
inference(sat_conversion,[],[f568037]) ).
cnf(s19693,plain,
~ spl1377_20056,
inference(sat_conversion,[],[f568356]) ).
cnf(s19694,plain,
( ~ spl1377_5304
| spl1377_20055 ),
inference(rat,[],[s19688,s19693]) ).
cnf(s19968,plain,
~ spl1377_5301,
inference(rat,[],[s19531,s19686,s19540]) ).
cnf(s19969,plain,
~ spl1377_5305,
inference(rat,[],[s19529,s19686,s19540]) ).
cnf(s19970,plain,
~ spl1377_5304,
inference(rat,[],[s19694,s19254]) ).
cnf(s19971,plain,
~ spl1377_5303,
inference(rat,[],[s19241,s19693,s19254]) ).
cnf(s20236,plain,
$false,
inference(rat,[],[s7065,s19093,s19969,s19970,s19971,s19968]) ).
fof(f568357,plain,
$false,
inference(avatar_sat_refutation,[],[s20236]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT025+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n017.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 21:12:07 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.71/4.40 % (4041337)Will run a generic schedule for satisfiability detection.
% 28.71/4.40 % (4041342)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2401906034_2998 on theBenchmark for (2998ds/0Mi)
% 28.71/4.40 % (4041343)% WARNING: option uhcvi not known.
% 28.71/4.40 % (4041343)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2474168628:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 28.71/4.40 % (4041344)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3728983131:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 28.71/4.40 % (4041345)dis+10_1_sil=32000:sp=arity:random_seed=2413101371:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 28.71/4.40 % (4041346)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1692345073:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 28.71/4.40 % (4041347)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1345164070:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 28.71/4.40 % (4041348)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1206585004:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 28.71/4.40 % (4041345)Instruction limit reached!
% 28.71/4.40 % (4041345)------------------------------
% 28.71/4.40 % (4041345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.40 % (4041345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.40 % (4041345)CaDiCaL version: 2.1.3
% 28.71/4.40 % (4041345)Termination reason: Instruction limit
% 28.71/4.40 % (4041345)Termination phase: Preprocessing 3
% 28.71/4.40 % (4041345)Time elapsed: 0.070 s
% 28.71/4.40 % (4041345)Peak memory usage: 21 MB
% 28.71/4.40 % (4041345)Instructions burned: 105 (million)
% 28.71/4.40 % (4041346)Instruction limit reached!
% 28.71/4.40 % (4041346)------------------------------
% 28.71/4.40 % (4041346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.40 % (4041346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.40 % (4041346)CaDiCaL version: 2.1.3
% 28.71/4.40 % (4041346)Termination reason: Instruction limit
% 28.71/4.40 % (4041346)Termination phase: NewCNF
% 28.71/4.40 % (4041346)Time elapsed: 0.078 s
% 28.71/4.40 % (4041346)Peak memory usage: 22 MB
% 28.71/4.40 % (4041346)Instructions burned: 117 (million)
% 28.71/4.40 % (4041347)Instruction limit reached!
% 28.71/4.40 % (4041347)------------------------------
% 28.71/4.40 % (4041347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.40 % (4041347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.40 % (4041347)CaDiCaL version: 2.1.3
% 28.71/4.40 % (4041347)Termination reason: Instruction limit
% 28.71/4.40 % (4041347)Termination phase: Preprocessing 3
% 28.71/4.40 % (4041347)Time elapsed: 0.087 s
% 28.71/4.40 % (4041347)Peak memory usage: 23 MB
% 28.71/4.40 % (4041347)Instructions burned: 132 (million)
% 28.71/4.40 % (4041356)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=822858811:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 28.71/4.40 % (4041357)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=26259289:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 28.71/4.40 % (4041348)Instruction limit reached!
% 28.71/4.40 % (4041348)------------------------------
% 28.71/4.40 % (4041348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.40 % (4041348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.40 % (4041348)CaDiCaL version: 2.1.3
% 28.71/4.40 % (4041348)Termination reason: Instruction limit
% 28.71/4.40 % (4041348)Termination phase: Clausification
% 28.71/4.40 % (4041348)Time elapsed: 0.102 s
% 28.71/4.40 % (4041348)Peak memory usage: 24 MB
% 28.71/4.40 % (4041348)Instructions burned: 159 (million)
% 28.71/4.40 % (4041358)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=2836375524:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 28.71/4.40 % (4041361)ott-21_1_sil=16000:fs=off:random_seed=1276736137:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 28.71/4.40 % (4041357)Instruction limit reached!
% 28.71/4.40 % (4041357)------------------------------
% 28.71/4.40 % (4041357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.40 % (4041357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.21/8.65 % (4041357)CaDiCaL version: 2.1.3
% 58.21/8.65 % (4041357)Termination reason: Instruction limit
% 58.21/8.65 % (4041357)Termination phase: Preprocessing 3
% 58.21/8.65 % (4041357)Time elapsed: 0.085 s
% 58.21/8.65 % (4041357)Peak memory usage: 23 MB
% 58.21/8.65 % (4041357)Instructions burned: 131 (million)
% 58.21/8.65 % (4041364)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1156995485:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 58.21/8.65 % (4041361)Instruction limit reached!
% 58.21/8.65 % (4041361)------------------------------
% 58.21/8.65 % (4041361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.21/8.65 % (4041361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.21/8.65 % (4041361)CaDiCaL version: 2.1.3
% 58.21/8.65 % (4041361)Termination reason: Instruction limit
% 58.21/8.65 % (4041361)Termination phase: Property scanning
% 58.21/8.65 % (4041361)Time elapsed: 0.110 s
% 58.21/8.65 % (4041361)Peak memory usage: 25 MB
% 58.21/8.65 % (4041361)Instructions burned: 180 (million)
% 58.21/8.65 % (4041366)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2264304264:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 58.21/8.65 % (4041358)Instruction limit reached!
% 58.21/8.65 % (4041358)------------------------------
% 58.21/8.65 % (4041358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.21/8.65 % (4041358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.21/8.65 % (4041358)CaDiCaL version: 2.1.3
% 58.21/8.65 % (4041358)Termination reason: Instruction limit
% 58.21/8.65 % (4041358)Termination phase: Saturation
% 58.21/8.65 % (4041358)Time elapsed: 0.325 s
% 58.21/8.65 % (4041358)Peak memory usage: 29 MB
% 58.21/8.65 % (4041358)Instructions burned: 686 (million)
% 58.21/8.65 % (4041356)Instruction limit reached!
% 58.21/8.65 % (4041356)------------------------------
% 58.21/8.65 % (4041356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.21/8.65 % (4041356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.21/8.65 % (4041356)CaDiCaL version: 2.1.3
% 58.21/8.65 % (4041356)Termination reason: Instruction limit
% 58.21/8.65 % (4041356)Termination phase: Finite model building preprocessing
% 58.21/8.65 % (4041356)Time elapsed: 0.344 s
% 58.21/8.65 % (4041356)Peak memory usage: 31 MB
% 58.21/8.65 % (4041356)Instructions burned: 716 (million)
% 58.21/8.65 % (4041364)Instruction limit reached!
% 58.21/8.65 % (4041364)------------------------------
% 58.21/8.65 % (4041364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.21/8.65 % (4041364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.21/8.65 % (4041364)CaDiCaL version: 2.1.3
% 58.21/8.65 % (4041364)Termination reason: Instruction limit
% 58.21/8.65 % (4041364)Termination phase: Saturation
% 58.21/8.65 % (4041364)Time elapsed: 0.234 s
% 58.21/8.65 % (4041364)Peak memory usage: 27 MB
% 58.21/8.65 % (4041364)Instructions burned: 477 (million)
% 58.21/8.65 % (4041368)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1237456509:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 58.21/8.65 % (4041369)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1461595302:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 58.21/8.65 % (4041370)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=3812368910:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 58.21/8.65 % (4041366)Instruction limit reached!
% 58.21/8.65 % (4041366)------------------------------
% 58.21/8.65 % (4041366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.21/8.65 % (4041366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.21/8.65 % (4041366)CaDiCaL version: 2.1.3
% 58.21/8.65 % (4041366)Termination reason: Instruction limit
% 58.21/8.65 % (4041366)Termination phase: Finite model building preprocessing
% 58.21/8.65 % (4041366)Time elapsed: 0.385 s
% 58.21/8.65 % (4041366)Peak memory usage: 33 MB
% 58.21/8.65 % (4041366)Instructions burned: 865 (million)
% 58.21/8.65 % (4041374)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=587802062:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 58.21/8.65 % (4041370)Instruction limit reached!
% 58.21/8.65 % (4041370)------------------------------
% 58.21/8.65 % (4041370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.21/8.65 % (4041370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.44/18.12 % (4041370)CaDiCaL version: 2.1.3
% 125.44/18.12 % (4041370)Termination reason: Instruction limit
% 125.44/18.12 % (4041370)Termination phase: Saturation
% 125.44/18.12 % (4041370)Time elapsed: 0.350 s
% 125.44/18.12 % (4041370)Peak memory usage: 31 MB
% 125.44/18.12 % (4041370)Instructions burned: 693 (million)
% 125.44/18.12 % (4041376)fmb+10_1_sil=64000:random_seed=2920559256:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 125.44/18.12 % (4041369)Instruction limit reached!
% 125.44/18.12 % (4041369)------------------------------
% 125.44/18.12 % (4041369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.44/18.12 % (4041369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.44/18.12 % (4041369)CaDiCaL version: 2.1.3
% 125.44/18.12 % (4041369)Termination reason: Instruction limit
% 125.44/18.12 % (4041369)Termination phase: Finite model building preprocessing
% 125.44/18.12 % (4041369)Time elapsed: 0.396 s
% 125.44/18.12 % (4041369)Peak memory usage: 34 MB
% 125.44/18.12 % (4041369)Instructions burned: 890 (million)
% 125.44/18.12 % (4041378)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3398333532:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 125.44/18.12 % (4041368)Instruction limit reached!
% 125.44/18.12 % (4041368)------------------------------
% 125.44/18.12 % (4041368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.44/18.12 % (4041368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.44/18.12 % (4041368)CaDiCaL version: 2.1.3
% 125.44/18.12 % (4041368)Termination reason: Instruction limit
% 125.44/18.12 % (4041368)Termination phase: Saturation
% 125.44/18.12 % (4041368)Time elapsed: 0.623 s
% 125.44/18.12 % (4041368)Peak memory usage: 40 MB
% 125.44/18.12 % (4041368)Instructions burned: 1179 (million)
% 125.44/18.12 % (4041374)Instruction limit reached!
% 125.44/18.12 % (4041374)------------------------------
% 125.44/18.12 % (4041374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.44/18.12 % (4041374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.44/18.12 % (4041374)CaDiCaL version: 2.1.3
% 125.44/18.12 % (4041374)Termination reason: Instruction limit
% 125.44/18.12 % (4041374)Termination phase: Saturation
% 125.44/18.12 % (4041374)Time elapsed: 0.420 s
% 125.44/18.12 % (4041374)Peak memory usage: 36 MB
% 125.44/18.12 % (4041374)Instructions burned: 881 (million)
% 125.44/18.12 % (4041380)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1421631998:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 125.44/18.12 % (4041381)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2291828879:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 125.44/18.12 % (4041380)Instruction limit reached!
% 125.44/18.12 % (4041380)------------------------------
% 125.44/18.12 % (4041380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.44/18.12 % (4041380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.44/18.12 % (4041380)CaDiCaL version: 2.1.3
% 125.44/18.12 % (4041380)Termination reason: Instruction limit
% 125.44/18.12 % (4041380)Termination phase: Finite model building preprocessing
% 125.44/18.12 % (4041380)Time elapsed: 0.402 s
% 125.44/18.12 % (4041380)Peak memory usage: 34 MB
% 125.44/18.12 % (4041380)Instructions burned: 921 (million)
% 125.44/18.12 % (4041384)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1549194579:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 125.44/18.12 % (4041384)Instruction limit reached!
% 125.44/18.12 % (4041384)------------------------------
% 125.44/18.12 % (4041384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.44/18.12 % (4041384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.44/18.12 % (4041384)CaDiCaL version: 2.1.3
% 125.44/18.12 % (4041384)Termination reason: Instruction limit
% 125.44/18.12 % (4041384)Termination phase: Saturation
% 125.44/18.12 % (4041384)Time elapsed: 0.684 s
% 125.44/18.12 % (4041384)Peak memory usage: 33 MB
% 125.44/18.12 % (4041384)Instructions burned: 1473 (million)
% 125.44/18.12 % (4041386)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=821697609:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 125.44/18.12 % (4041381)Instruction limit reached!
% 125.44/18.12 % (4041381)------------------------------
% 125.44/18.12 % (4041381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.44/18.12 % (4041381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.44/18.12 % (4041381)CaDiCaL version: 2.1.3
% 125.44/18.12 % (4041381)Termination reason: Instruction limit
% 181.59/30.26 % (4041381)Termination phase: Saturation
% 181.59/30.26 % (4041381)Time elapsed: 2.881 s
% 181.59/30.26 % (4041381)Peak memory usage: 77 MB
% 181.59/30.26 % (4041381)Instructions burned: 5132 (million)
% 181.59/30.26 % (4041389)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=224187045:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi)
% 181.59/30.26 % (4041389)Instruction limit reached!
% 181.59/30.26 % (4041389)------------------------------
% 181.59/30.26 % (4041389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.26 % (4041389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.26 % (4041389)CaDiCaL version: 2.1.3
% 181.59/30.26 % (4041389)Termination reason: Instruction limit
% 181.59/30.26 % (4041389)Termination phase: Finite model building preprocessing
% 181.59/30.26 % (4041389)Time elapsed: 0.771 s
% 181.59/30.26 % (4041389)Peak memory usage: 43 MB
% 181.59/30.26 % (4041389)Instructions burned: 2182 (million)
% 181.59/30.26 % (4041391)ott-2_1_sil=16000:newcnf=on:random_seed=3608150563:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2950 on theBenchmark for (2950ds/869Mi)
% 181.59/30.26 % (4041391)Instruction limit reached!
% 181.59/30.26 % (4041391)------------------------------
% 181.59/30.26 % (4041391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.26 % (4041391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.26 % (4041391)CaDiCaL version: 2.1.3
% 181.59/30.26 % (4041391)Termination reason: Instruction limit
% 181.59/30.26 % (4041391)Termination phase: Saturation
% 181.59/30.26 % (4041391)Time elapsed: 0.406 s
% 181.59/30.26 % (4041391)Peak memory usage: 32 MB
% 181.59/30.26 % (4041391)Instructions burned: 869 (million)
% 181.59/30.26 % (4041393)ott+10_1_sil=32000:tgt=ground:random_seed=2929830884:i=5114:av=off_2945 on theBenchmark for (2945ds/5114Mi)
% 181.59/30.26 % (4041386)Instruction limit reached!
% 181.59/30.26 % (4041386)------------------------------
% 181.59/30.26 % (4041386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.26 % (4041386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.26 % (4041386)CaDiCaL version: 2.1.3
% 181.59/30.26 % (4041386)Termination reason: Instruction limit
% 181.59/30.26 % (4041386)Termination phase: Finite model building preprocessing
% 181.59/30.26 % (4041386)Time elapsed: 3.381 s
% 181.59/30.26 % (4041386)Peak memory usage: 56 MB
% 181.59/30.26 % (4041386)Instructions burned: 6324 (million)
% 181.59/30.26 % (4041395)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=55107201:i=54282_2941 on theBenchmark for (2941ds/54282Mi)
% 181.59/30.26 % (4041378)Instruction limit reached!
% 181.59/30.26 % (4041378)------------------------------
% 181.59/30.26 % (4041378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.26 % (4041378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.26 % (4041378)CaDiCaL version: 2.1.3
% 181.59/30.26 % (4041378)Termination reason: Instruction limit
% 181.59/30.26 % (4041378)Termination phase: Finite model building preprocessing
% 181.59/30.26 % (4041378)Time elapsed: 5.103 s
% 181.59/30.26 % (4041378)Peak memory usage: 68 MB
% 181.59/30.26 % (4041378)Instructions burned: 9516 (million)
% 181.59/30.26 % (4041397)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=607212754:i=3512:aac=none_2938 on theBenchmark for (2938ds/3512Mi)
% 181.59/30.26 % (4041397)Instruction limit reached!
% 181.59/30.26 % (4041397)------------------------------
% 181.59/30.27 % (4041397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041397)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041397)Termination reason: Instruction limit
% 181.59/30.27 % (4041397)Termination phase: Saturation
% 181.59/30.27 % (4041397)Time elapsed: 1.879 s
% 181.59/30.27 % (4041397)Peak memory usage: 54 MB
% 181.59/30.27 % (4041397)Instructions burned: 3512 (million)
% 181.59/30.27 % (4041399)dis+21_1_sil=32000:sas=cadical:random_seed=3976577822:i=3773:amm=off_2919 on theBenchmark for (2919ds/3773Mi)
% 181.59/30.27 % (4041393)Instruction limit reached!
% 181.59/30.27 % (4041393)------------------------------
% 181.59/30.27 % (4041393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041393)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041393)Termination reason: Instruction limit
% 181.59/30.27 % (4041393)Termination phase: Saturation
% 181.59/30.27 % (4041393)Time elapsed: 2.998 s
% 181.59/30.27 % (4041393)Peak memory usage: 90 MB
% 181.59/30.27 % (4041393)Instructions burned: 5115 (million)
% 181.59/30.27 % (4041401)ott+11_1_sil=16000:gs=on:random_seed=2640326363:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2915 on theBenchmark for (2915ds/2251Mi)
% 181.59/30.27 % (4041401)Instruction limit reached!
% 181.59/30.27 % (4041401)------------------------------
% 181.59/30.27 % (4041401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041401)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041401)Termination reason: Instruction limit
% 181.59/30.27 % (4041401)Termination phase: Saturation
% 181.59/30.27 % (4041401)Time elapsed: 0.987 s
% 181.59/30.27 % (4041401)Peak memory usage: 38 MB
% 181.59/30.27 % (4041401)Instructions burned: 2252 (million)
% 181.59/30.27 % (4041403)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1558541866:fmbsr=1.6:i=67534_2905 on theBenchmark for (2905ds/67534Mi)
% 181.59/30.27 % (4041399)Instruction limit reached!
% 181.59/30.27 % (4041399)------------------------------
% 181.59/30.27 % (4041399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041399)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041399)Termination reason: Instruction limit
% 181.59/30.27 % (4041399)Termination phase: Saturation
% 181.59/30.27 % (4041399)Time elapsed: 1.845 s
% 181.59/30.27 % (4041399)Peak memory usage: 67 MB
% 181.59/30.27 % (4041399)Instructions burned: 3773 (million)
% 181.59/30.27 % (4041405)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1752311871:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2900 on theBenchmark for (2900ds/4591Mi)
% 181.59/30.27 % (4041405)Instruction limit reached!
% 181.59/30.27 % (4041405)------------------------------
% 181.59/30.27 % (4041405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041405)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041405)Termination reason: Instruction limit
% 181.59/30.27 % (4041405)Termination phase: Saturation
% 181.59/30.27 % (4041405)Time elapsed: 1.927 s
% 181.59/30.27 % (4041405)Peak memory usage: 43 MB
% 181.59/30.27 % (4041405)Instructions burned: 4591 (million)
% 181.59/30.27 % (4041407)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4161298436:i=29340_2880 on theBenchmark for (2880ds/29340Mi)
% 181.59/30.27 % (4041376)Instruction limit reached!
% 181.59/30.27 % (4041376)------------------------------
% 181.59/30.27 % (4041376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041376)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041376)Termination reason: Instruction limit
% 181.59/30.27 % (4041376)Termination phase: Finite model building preprocessing
% 181.59/30.27 % (4041376)Time elapsed: 12.012 s
% 181.59/30.27 % (4041376)Peak memory usage: 85 MB
% 181.59/30.27 % (4041376)Instructions burned: 22063 (million)
% 181.59/30.27 % (4041409)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=720846674:i=5211_2869 on theBenchmark for (2869ds/5211Mi)
% 181.59/30.27 % (4041409)Instruction limit reached!
% 181.59/30.27 % (4041409)------------------------------
% 181.59/30.27 % (4041409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041409)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041409)Termination reason: Instruction limit
% 181.59/30.27 % (4041409)Termination phase: Saturation
% 181.59/30.27 % (4041409)Time elapsed: 1.825 s
% 181.59/30.27 % (4041409)Peak memory usage: 49 MB
% 181.59/30.27 % (4041409)Instructions burned: 5213 (million)
% 181.59/30.27 % (4041411)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=435913701:i=5497:nm=2_2851 on theBenchmark for (2851ds/5497Mi)
% 181.59/30.27 % (4041411)Instruction limit reached!
% 181.59/30.27 % (4041411)------------------------------
% 181.59/30.27 % (4041411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041411)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041411)Termination reason: Instruction limit
% 181.59/30.27 % (4041411)Termination phase: Finite model building preprocessing
% 181.59/30.27 % (4041411)Time elapsed: 2.982 s
% 181.59/30.27 % (4041411)Peak memory usage: 52 MB
% 181.59/30.27 % (4041411)Instructions burned: 5498 (million)
% 181.59/30.27 % (4041413)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2973998255:fmbsr=2:i=46332_2820 on theBenchmark for (2820ds/46332Mi)
% 181.59/30.27 % (4041344)Instruction limit reached!
% 181.59/30.27 % (4041344)------------------------------
% 181.59/30.27 % (4041344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041344)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041344)Termination reason: Instruction limit
% 181.59/30.27 % (4041344)Termination phase: Saturation
% 181.59/30.27 % (4041344)Time elapsed: 23.164 s
% 181.59/30.27 % (4041344)Peak memory usage: 89 MB
% 181.59/30.27 % (4041344)Instructions burned: 88028 (million)
% 181.59/30.27 % (4041415)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3645125640:i=14071_2766 on theBenchmark for (2766ds/14071Mi)
% 181.59/30.27 % (4041407)Instruction limit reached!
% 181.59/30.27 % (4041407)------------------------------
% 181.59/30.27 % (4041407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041407)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041407)Termination reason: Instruction limit
% 181.59/30.27 % (4041407)Termination phase: Saturation
% 181.59/30.27 % (4041407)Time elapsed: 15.925 s
% 181.59/30.27 % (4041407)Peak memory usage: 1057 MB
% 181.59/30.27 % (4041407)Instructions burned: 29340 (million)
% 181.59/30.27 % (4041417)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1844189707:i=22565:add=on:rawr=on_2720 on theBenchmark for (2720ds/22565Mi)
% 181.59/30.27 % (4041343) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4041337-4041343"...
% 181.59/30.27 % (4041343)...printing done.
% 181.59/30.27 % (4041343)Refutation found. Thanks to Tanya!
% 181.59/30.27 % SZS status Theorem for theBenchmark
% 181.59/30.27 % SZS output start Proof for theBenchmark
% See solution above
% 181.59/30.27 % (4041343)------------------------------
% 181.59/30.27 % (4041343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.59/30.27 % (4041343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.59/30.27 % (4041343)CaDiCaL version: 2.1.3
% 181.59/30.27 % (4041343)Termination reason: Refutation
% 181.59/30.27 % (4041343)Time elapsed: 29.775 s
% 181.59/30.27 % (4041343)Peak memory usage: 295 MB
% 181.59/30.27 % (4041343)Instructions burned: 54752 (million)
% 181.59/30.27 % (4041337)Success in time 30.044 s
% 181.59/30.27 % Vampire exiting
%------------------------------------------------------------------------------