%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP637+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 10:15:11 AM UTC 2026
% Result : Theorem 38.76s 11.51s
% Output : Refutation 61.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of formulae : 132 ( 33 unt; 3 def)
% Number of atoms : 544 ( 28 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 680 ( 268 ~; 263 |; 109 &)
% ( 10 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 4 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-4 aty)
% Number of variables : 147 ( 0 sgn 133 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f865,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t156_relat_1) ).
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1481,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f2094,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1) )
=> k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f21855,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
=> ( m1_group_2(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_group_2) ).
fof(f21877,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
=> m1_group_2(X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t66_group_2) ).
fof(f22007,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f27005,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0) )
=> ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_group_6) ).
fof(f36499,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_group_2(X4,X0)
=> ! [X5] :
( m1_group_2(X5,X1)
=> ! [X6] :
( m1_group_2(X6,X1)
=> ( ( u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X0,X4) )
=> m1_group_6(X5,X1,X6) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_latsubgr) ).
fof(f36500,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_group_2(X4,X0)
=> ! [X5] :
( m1_group_2(X5,X1)
=> ! [X6] :
( m1_group_2(X6,X1)
=> ( ( u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X0,X4) )
=> m1_group_6(X5,X1,X6) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f36499]) ).
fof(f37070,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ~ m1_group_6(X5,X1,X6)
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X0,X4)
& m1_group_2(X6,X1) )
& m1_group_2(X5,X1) )
& m1_group_2(X4,X0) )
& m1_group_2(X3,X0) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f36500]) ).
fof(f37071,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ~ m1_group_6(X5,X1,X6)
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X0,X4)
& m1_group_2(X6,X1) )
& m1_group_2(X5,X1) )
& m1_group_2(X4,X0) )
& m1_group_2(X3,X0) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f37070]) ).
fof(f37091,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1481]) ).
fof(f37161,plain,
! [X0,X1,X2,X3] :
( k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f2094]) ).
fof(f37162,plain,
! [X0,X1,X2,X3] :
( k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f37161]) ).
fof(f37189,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22007]) ).
fof(f37190,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f37189]) ).
fof(f37191,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21877]) ).
fof(f37192,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f37191]) ).
fof(f37255,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f27005]) ).
fof(f37256,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f37255]) ).
fof(f37313,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f38678,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f865]) ).
fof(f38679,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f38678]) ).
fof(f42543,plain,
! [X0] :
( ! [X1] :
( ( m1_group_2(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1)) ) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21855]) ).
fof(f42544,plain,
! [X0] :
( ! [X1] :
( ( m1_group_2(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1)) ) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f42543]) ).
fof(f48546,plain,
( ~ m1_group_6(sK435,sK431,sK436)
& u1_struct_0(sK435) = k2_funct_2(u1_struct_0(sK430),u1_struct_0(sK431),sK432,u1_struct_0(sK433))
& u1_struct_0(sK436) = k2_funct_2(u1_struct_0(sK430),u1_struct_0(sK431),sK432,u1_struct_0(sK434))
& m1_group_6(sK433,sK430,sK434)
& m1_group_2(sK436,sK431)
& m1_group_2(sK435,sK431)
& m1_group_2(sK434,sK430)
& m1_group_2(sK433,sK430)
& v1_funct_1(sK432)
& v1_funct_2(sK432,u1_struct_0(sK430),u1_struct_0(sK431))
& v1_group_6(sK432,sK430,sK431)
& m2_relset_1(sK432,u1_struct_0(sK430),u1_struct_0(sK431))
& ~ v3_struct_0(sK431)
& v3_group_1(sK431)
& v4_group_1(sK431)
& l1_group_1(sK431)
& ~ v3_struct_0(sK430)
& v3_group_1(sK430)
& v4_group_1(sK430)
& l1_group_1(sK430) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK430,sK431,sK432,sK433,sK434,sK435,sK436]),skolemize(X0,sK430),skolemize(X1,sK431),skolemize(X2,sK432),skolemize(X3,sK433),skolemize(X4,sK434),skolemize(X5,sK435),skolemize(X6,sK436)],[f37071]) ).
fof(f48574,plain,
! [X0,X1] :
( ! [X2] :
( ( m1_group_6(X2,X0,X1)
| ~ m1_group_2(X2,X1) )
& ( m1_group_2(X2,X1)
| ~ m1_group_6(X2,X0,X1) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(nnf_transformation,[],[f37256]) ).
fof(f49135,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1483]) ).
fof(f50343,plain,
! [X0] :
( ! [X1] :
( ( ( m1_group_2(X1,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| u1_group_1(X1) != k1_realset1(u1_group_1(X0),u1_struct_0(X1)) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) ) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f42544]) ).
fof(f50344,plain,
! [X0] :
( ! [X1] :
( ( ( m1_group_2(X1,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| u1_group_1(X1) != k1_realset1(u1_group_1(X0),u1_struct_0(X1)) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) ) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f50343]) ).
fof(f52475,plain,
l1_group_1(sK430),
inference(cnf_transformation,[],[f48546]) ).
fof(f52476,plain,
v4_group_1(sK430),
inference(cnf_transformation,[],[f48546]) ).
fof(f52477,plain,
v3_group_1(sK430),
inference(cnf_transformation,[],[f48546]) ).
fof(f52478,plain,
~ v3_struct_0(sK430),
inference(cnf_transformation,[],[f48546]) ).
fof(f52479,plain,
l1_group_1(sK431),
inference(cnf_transformation,[],[f48546]) ).
fof(f52480,plain,
v4_group_1(sK431),
inference(cnf_transformation,[],[f48546]) ).
fof(f52481,plain,
v3_group_1(sK431),
inference(cnf_transformation,[],[f48546]) ).
fof(f52482,plain,
~ v3_struct_0(sK431),
inference(cnf_transformation,[],[f48546]) ).
fof(f52483,plain,
m2_relset_1(sK432,u1_struct_0(sK430),u1_struct_0(sK431)),
inference(cnf_transformation,[],[f48546]) ).
fof(f52485,plain,
v1_funct_2(sK432,u1_struct_0(sK430),u1_struct_0(sK431)),
inference(cnf_transformation,[],[f48546]) ).
fof(f52486,plain,
v1_funct_1(sK432),
inference(cnf_transformation,[],[f48546]) ).
fof(f52488,plain,
m1_group_2(sK434,sK430),
inference(cnf_transformation,[],[f48546]) ).
fof(f52489,plain,
m1_group_2(sK435,sK431),
inference(cnf_transformation,[],[f48546]) ).
fof(f52490,plain,
m1_group_2(sK436,sK431),
inference(cnf_transformation,[],[f48546]) ).
fof(f52491,plain,
m1_group_6(sK433,sK430,sK434),
inference(cnf_transformation,[],[f48546]) ).
fof(f52492,plain,
u1_struct_0(sK436) = k2_funct_2(u1_struct_0(sK430),u1_struct_0(sK431),sK432,u1_struct_0(sK434)),
inference(cnf_transformation,[],[f48546]) ).
fof(f52493,plain,
u1_struct_0(sK435) = k2_funct_2(u1_struct_0(sK430),u1_struct_0(sK431),sK432,u1_struct_0(sK433)),
inference(cnf_transformation,[],[f48546]) ).
fof(f52494,plain,
~ m1_group_6(sK435,sK431,sK436),
inference(cnf_transformation,[],[f48546]) ).
fof(f52522,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f37091]) ).
fof(f52580,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k9_relat_1(X2,X3) = k2_funct_2(X0,X1,X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f37162]) ).
fof(f52605,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37190]) ).
fof(f52606,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| v3_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37190]) ).
fof(f52607,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ v3_struct_0(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37190]) ).
fof(f52608,plain,
! [X2,X0,X1] :
( ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| m1_group_2(X1,X2)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37192]) ).
fof(f52672,plain,
! [X2,X0,X1] :
( ~ m1_group_6(X2,X0,X1)
| m1_group_2(X2,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f48574]) ).
fof(f52673,plain,
! [X2,X0,X1] :
( m1_group_6(X2,X0,X1)
| ~ m1_group_2(X2,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f48574]) ).
fof(f52773,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f37313]) ).
fof(f54734,plain,
! [X2,X0,X1] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f38679]) ).
fof(f54787,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f49135]) ).
fof(f60234,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f50344]) ).
fof(f73975,plain,
( ~ m1_group_2(sK435,sK436)
| v3_struct_0(sK431)
| ~ v3_group_1(sK431)
| ~ v4_group_1(sK431)
| ~ l1_group_1(sK431)
| ~ m1_group_2(sK436,sK431) ),
inference(resolution,[],[f52494,f52673]) ).
fof(f73977,plain,
( m1_group_2(sK433,sK434)
| v3_struct_0(sK430)
| ~ v3_group_1(sK430)
| ~ v4_group_1(sK430)
| ~ l1_group_1(sK430)
| ~ m1_group_2(sK434,sK430) ),
inference(resolution,[],[f52672,f52491]) ).
fof(f73979,plain,
( ~ v3_struct_0(sK434)
| v3_struct_0(sK430)
| ~ v3_group_1(sK430)
| ~ l1_group_1(sK430) ),
inference(resolution,[],[f52488,f52607]) ).
fof(f73987,plain,
( v3_group_1(sK434)
| v3_struct_0(sK430)
| ~ v3_group_1(sK430)
| ~ l1_group_1(sK430) ),
inference(resolution,[],[f52606,f52488]) ).
fof(f73995,plain,
( l1_group_1(sK434)
| v3_struct_0(sK430)
| ~ v3_group_1(sK430)
| ~ l1_group_1(sK430) ),
inference(resolution,[],[f52605,f52488]) ).
fof(f74004,definition,
( spl2848_106
<=> m1_relset_1(sK432,u1_struct_0(sK430),u1_struct_0(sK431)) ),
introduced(definition,[new_symbols(definition,[spl2848_106])],[avatar_definition]) ).
fof(f74005,plain,
( m1_relset_1(sK432,u1_struct_0(sK430),u1_struct_0(sK431))
| ~ spl2848_106 ),
inference(avatar_component_clause,[],[f74004]) ).
fof(f74006,plain,
( ~ m1_relset_1(sK432,u1_struct_0(sK430),u1_struct_0(sK431))
| spl2848_106 ),
inference(avatar_component_clause,[],[f74004]) ).
fof(f74017,plain,
! [X0] :
( ~ v1_funct_1(sK432)
| k9_relat_1(sK432,X0) = k2_funct_2(u1_struct_0(sK430),u1_struct_0(sK431),sK432,X0)
| ~ m1_relset_1(sK432,u1_struct_0(sK430),u1_struct_0(sK431)) ),
inference(resolution,[],[f52580,f52485]) ).
fof(f74033,plain,
m1_relset_1(sK432,u1_struct_0(sK430),u1_struct_0(sK431)),
inference(resolution,[],[f54787,f52483]) ).
fof(f74034,plain,
( $false
| spl2848_106 ),
inference(forward_subsumption_resolution,[],[f74033,f74006]) ).
fof(f74035,plain,
spl2848_106,
inference(avatar_contradiction_clause,[],[f74034]) ).
fof(f74036,plain,
! [X0] :
( k9_relat_1(sK432,X0) = k2_funct_2(u1_struct_0(sK430),u1_struct_0(sK431),sK432,X0)
| ~ m1_relset_1(sK432,u1_struct_0(sK430),u1_struct_0(sK431)) ),
inference(forward_subsumption_resolution,[],[f74017,f52486]) ).
fof(f74037,plain,
( ! [X0] : k9_relat_1(sK432,X0) = k2_funct_2(u1_struct_0(sK430),u1_struct_0(sK431),sK432,X0)
| ~ spl2848_106 ),
inference(forward_subsumption_resolution,[],[f74036,f74005]) ).
fof(f74040,plain,
( u1_struct_0(sK435) = k9_relat_1(sK432,u1_struct_0(sK433))
| ~ spl2848_106 ),
inference(superposition,[],[f52493,f74037]) ).
fof(f74041,plain,
( u1_struct_0(sK436) = k9_relat_1(sK432,u1_struct_0(sK434))
| ~ spl2848_106 ),
inference(superposition,[],[f52492,f74037]) ).
fof(f74085,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f52522,f52773]) ).
fof(f74086,plain,
v1_relat_1(sK432),
inference(resolution,[],[f74085,f52483]) ).
fof(f74115,plain,
( ! [X0] :
( r1_tarski(k9_relat_1(sK432,X0),u1_struct_0(sK436))
| ~ r1_tarski(X0,u1_struct_0(sK434))
| ~ v1_relat_1(sK432) )
| ~ spl2848_106 ),
inference(superposition,[],[f54734,f74041]) ).
fof(f74116,plain,
( ! [X0] :
( r1_tarski(k9_relat_1(sK432,X0),u1_struct_0(sK436))
| ~ r1_tarski(X0,u1_struct_0(sK434)) )
| ~ spl2848_106 ),
inference(forward_subsumption_resolution,[],[f74115,f74086]) ).
fof(f74120,plain,
( r1_tarski(u1_struct_0(sK435),u1_struct_0(sK436))
| ~ r1_tarski(u1_struct_0(sK433),u1_struct_0(sK434))
| ~ spl2848_106 ),
inference(superposition,[],[f74116,f74040]) ).
fof(f74123,definition,
( spl2848_109
<=> r1_tarski(u1_struct_0(sK433),u1_struct_0(sK434)) ),
introduced(definition,[new_symbols(definition,[spl2848_109])],[avatar_definition]) ).
fof(f74125,plain,
( ~ r1_tarski(u1_struct_0(sK433),u1_struct_0(sK434))
| spl2848_109 ),
inference(avatar_component_clause,[],[f74123]) ).
fof(f74127,definition,
( spl2848_110
<=> r1_tarski(u1_struct_0(sK435),u1_struct_0(sK436)) ),
introduced(definition,[new_symbols(definition,[spl2848_110])],[avatar_definition]) ).
fof(f74129,plain,
( r1_tarski(u1_struct_0(sK435),u1_struct_0(sK436))
| ~ spl2848_110 ),
inference(avatar_component_clause,[],[f74127]) ).
fof(f74130,plain,
( ~ spl2848_109
| spl2848_110
| ~ spl2848_106 ),
inference(avatar_split_clause,[],[f74120,f74004,f74127,f74123]) ).
fof(f74131,plain,
( ~ m1_group_2(sK433,sK434)
| v3_struct_0(sK433)
| ~ v3_group_1(sK433)
| ~ l1_group_1(sK433)
| v3_struct_0(sK434)
| ~ v3_group_1(sK434)
| ~ l1_group_1(sK434)
| spl2848_109 ),
inference(resolution,[],[f74125,f60234]) ).
fof(f75089,plain,
( ~ v3_struct_0(sK434)
| ~ v3_group_1(sK430)
| ~ l1_group_1(sK430) ),
inference(forward_subsumption_resolution,[],[f73979,f52478]) ).
fof(f75092,plain,
( v3_group_1(sK434)
| ~ v3_group_1(sK430)
| ~ l1_group_1(sK430) ),
inference(forward_subsumption_resolution,[],[f73987,f52478]) ).
fof(f75096,plain,
( l1_group_1(sK434)
| ~ v3_group_1(sK430)
| ~ l1_group_1(sK430) ),
inference(forward_subsumption_resolution,[],[f73995,f52478]) ).
fof(f75099,plain,
( ~ m1_group_2(sK433,sK434)
| ~ v3_group_1(sK433)
| ~ l1_group_1(sK433)
| v3_struct_0(sK434)
| ~ v3_group_1(sK434)
| ~ l1_group_1(sK434)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f74131,f52607]) ).
fof(f75146,plain,
( ~ v3_struct_0(sK434)
| ~ l1_group_1(sK430) ),
inference(forward_subsumption_resolution,[],[f75089,f52477]) ).
fof(f75149,plain,
( v3_group_1(sK434)
| ~ l1_group_1(sK430) ),
inference(forward_subsumption_resolution,[],[f75092,f52477]) ).
fof(f75153,plain,
( l1_group_1(sK434)
| ~ l1_group_1(sK430) ),
inference(forward_subsumption_resolution,[],[f75096,f52477]) ).
fof(f75156,plain,
( ~ m1_group_2(sK433,sK434)
| ~ l1_group_1(sK433)
| v3_struct_0(sK434)
| ~ v3_group_1(sK434)
| ~ l1_group_1(sK434)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f75099,f52606]) ).
fof(f75195,plain,
~ v3_struct_0(sK434),
inference(forward_subsumption_resolution,[],[f75146,f52475]) ).
fof(f75198,plain,
v3_group_1(sK434),
inference(forward_subsumption_resolution,[],[f75149,f52475]) ).
fof(f75202,plain,
l1_group_1(sK434),
inference(forward_subsumption_resolution,[],[f75153,f52475]) ).
fof(f75205,plain,
( ~ m1_group_2(sK433,sK434)
| v3_struct_0(sK434)
| ~ v3_group_1(sK434)
| ~ l1_group_1(sK434)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f75156,f52605]) ).
fof(f75228,plain,
( ~ m1_group_2(sK433,sK434)
| ~ v3_group_1(sK434)
| ~ l1_group_1(sK434)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f75205,f75195]) ).
fof(f75266,plain,
( ~ m1_group_2(sK433,sK434)
| ~ l1_group_1(sK434)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f75228,f75198]) ).
fof(f75276,plain,
( ~ m1_group_2(sK433,sK434)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f75266,f75202]) ).
fof(f75336,plain,
( ~ m1_group_2(sK435,sK436)
| ~ v3_group_1(sK431)
| ~ v4_group_1(sK431)
| ~ l1_group_1(sK431)
| ~ m1_group_2(sK436,sK431) ),
inference(forward_subsumption_resolution,[],[f73975,f52482]) ).
fof(f75337,plain,
( v3_struct_0(sK430)
| ~ v3_group_1(sK430)
| ~ v4_group_1(sK430)
| ~ l1_group_1(sK430)
| ~ m1_group_2(sK434,sK430)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f73977,f75276]) ).
fof(f75626,plain,
( ~ m1_group_2(sK435,sK436)
| ~ v4_group_1(sK431)
| ~ l1_group_1(sK431)
| ~ m1_group_2(sK436,sK431) ),
inference(forward_subsumption_resolution,[],[f75336,f52481]) ).
fof(f75627,plain,
( ~ v3_group_1(sK430)
| ~ v4_group_1(sK430)
| ~ l1_group_1(sK430)
| ~ m1_group_2(sK434,sK430)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f75337,f52478]) ).
fof(f75862,plain,
( ~ m1_group_2(sK435,sK436)
| ~ l1_group_1(sK431)
| ~ m1_group_2(sK436,sK431) ),
inference(forward_subsumption_resolution,[],[f75626,f52480]) ).
fof(f75863,plain,
( ~ v4_group_1(sK430)
| ~ l1_group_1(sK430)
| ~ m1_group_2(sK434,sK430)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f75627,f52477]) ).
fof(f76068,plain,
( ~ m1_group_2(sK435,sK436)
| ~ m1_group_2(sK436,sK431) ),
inference(forward_subsumption_resolution,[],[f75862,f52479]) ).
fof(f76069,plain,
( ~ l1_group_1(sK430)
| ~ m1_group_2(sK434,sK430)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f75863,f52476]) ).
fof(f76247,plain,
~ m1_group_2(sK435,sK436),
inference(forward_subsumption_resolution,[],[f76068,f52490]) ).
fof(f76248,plain,
( ~ m1_group_2(sK434,sK430)
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f76069,f52475]) ).
fof(f76419,plain,
( $false
| spl2848_109 ),
inference(forward_subsumption_resolution,[],[f76248,f52488]) ).
fof(f76420,plain,
spl2848_109,
inference(avatar_contradiction_clause,[],[f76419]) ).
fof(f76720,plain,
( ! [X0] :
( m1_group_2(sK435,sK436)
| ~ m1_group_2(sK436,X0)
| ~ m1_group_2(sK435,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl2848_110 ),
inference(resolution,[],[f74129,f52608]) ).
fof(f76730,plain,
( ! [X0] :
( ~ m1_group_2(sK436,X0)
| ~ m1_group_2(sK435,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl2848_110 ),
inference(forward_subsumption_resolution,[],[f76720,f76247]) ).
fof(f76737,plain,
( ~ m1_group_2(sK435,sK431)
| v3_struct_0(sK431)
| ~ v3_group_1(sK431)
| ~ v4_group_1(sK431)
| ~ l1_group_1(sK431)
| ~ spl2848_110 ),
inference(resolution,[],[f76730,f52490]) ).
fof(f76739,plain,
( v3_struct_0(sK431)
| ~ v3_group_1(sK431)
| ~ v4_group_1(sK431)
| ~ l1_group_1(sK431)
| ~ spl2848_110 ),
inference(forward_subsumption_resolution,[],[f76737,f52489]) ).
fof(f76743,plain,
( ~ v3_group_1(sK431)
| ~ v4_group_1(sK431)
| ~ l1_group_1(sK431)
| ~ spl2848_110 ),
inference(forward_subsumption_resolution,[],[f76739,f52482]) ).
fof(f76746,plain,
( ~ v4_group_1(sK431)
| ~ l1_group_1(sK431)
| ~ spl2848_110 ),
inference(forward_subsumption_resolution,[],[f76743,f52481]) ).
fof(f76749,plain,
( ~ l1_group_1(sK431)
| ~ spl2848_110 ),
inference(forward_subsumption_resolution,[],[f76746,f52480]) ).
fof(f76751,plain,
( $false
| ~ spl2848_110 ),
inference(forward_subsumption_resolution,[],[f76749,f52479]) ).
fof(f76752,plain,
~ spl2848_110,
inference(avatar_contradiction_clause,[],[f76751]) ).
cnf(s98,plain,
spl2848_106,
inference(sat_conversion,[],[f74035]) ).
cnf(s99,plain,
( ~ spl2848_106
| ~ spl2848_109
| spl2848_110 ),
inference(sat_conversion,[],[f74130]) ).
cnf(s130,plain,
spl2848_109,
inference(sat_conversion,[],[f76420]) ).
cnf(s140,plain,
~ spl2848_110,
inference(sat_conversion,[],[f76752]) ).
cnf(s144,plain,
~ spl2848_106,
inference(rat,[],[s99,s140,s130]) ).
cnf(s145,plain,
$false,
inference(rat,[],[s98,s144]) ).
fof(f76754,plain,
$false,
inference(avatar_sat_refutation,[],[s145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP637+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 10:23:28 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.70/5.10 % (3333204)Detected formulas, will run a generic FOF schedule.
% 15.70/5.10 % (3333215)dis-21_1_sil=8000:lcm=predicate:random_seed=2924472096:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2976 on theBenchmark for (2976ds/129Mi)
% 15.70/5.10 % (3333211)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=1884253:i=141695:sd=1:nm=32:gsp=on:ss=included_2976 on theBenchmark for (2976ds/141695Mi)
% 15.70/5.10 % (3333209)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=3312935302:i=141193_2976 on theBenchmark for (2976ds/141193Mi)
% 15.70/5.10 % (3333210)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=3044557208:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2976 on theBenchmark for (2976ds/134677Mi)
% 15.70/5.10 % (3333214)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2700027665:s2a=on:i=139:gtg=position_2976 on theBenchmark for (2976ds/139Mi)
% 15.70/5.10 % (3333212)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=493927232:i=109:sd=1:ins=1:gsp=on:ss=axioms_2976 on theBenchmark for (2976ds/109Mi)
% 15.70/5.10 % (3333213)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3931973966:i=119:av=off:ss=axioms_2976 on theBenchmark for (2976ds/119Mi)
% 15.70/5.10 % (3333215)Instruction limit reached!
% 15.70/5.10 % (3333215)------------------------------
% 15.70/5.10 % (3333215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.70/5.10 % (3333215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.70/5.10 % (3333215)CaDiCaL version: 2.1.3
% 15.70/5.10 % (3333215)Termination reason: Instruction limit
% 15.70/5.10 % (3333215)Termination phase: SInE selection
% 15.70/5.10 % (3333215)Time elapsed: 0.055 s
% 15.70/5.10 % (3333215)Peak memory usage: 139 MB
% 15.70/5.10 % (3333215)Instructions burned: 130 (million)
% 15.70/5.10 % (3333214)Instruction limit reached!
% 15.70/5.10 % (3333214)------------------------------
% 15.70/5.10 % (3333214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.70/5.10 % (3333214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.70/5.10 % (3333214)CaDiCaL version: 2.1.3
% 15.70/5.10 % (3333214)Termination reason: Instruction limit
% 15.70/5.10 % (3333214)Termination phase: Property scanning
% 15.70/5.10 % (3333214)Time elapsed: 0.063 s
% 15.70/5.10 % (3333214)Peak memory usage: 139 MB
% 15.70/5.10 % (3333214)Instructions burned: 140 (million)
% 15.70/5.10 % (3333212)Instruction limit reached!
% 15.70/5.10 % (3333212)------------------------------
% 15.70/5.10 % (3333212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.70/5.10 % (3333212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.70/5.10 % (3333212)CaDiCaL version: 2.1.3
% 15.70/5.10 % (3333212)Termination reason: Instruction limit
% 15.70/5.10 % (3333212)Termination phase: SInE selection
% 15.70/5.10 % (3333212)Time elapsed: 0.086 s
% 15.70/5.10 % (3333212)Peak memory usage: 139 MB
% 15.70/5.10 % (3333212)Instructions burned: 110 (million)
% 15.70/5.10 % (3333213)Instruction limit reached!
% 15.70/5.10 % (3333213)------------------------------
% 15.70/5.10 % (3333213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.70/5.10 % (3333213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.70/5.10 % (3333213)CaDiCaL version: 2.1.3
% 15.70/5.10 % (3333213)Termination reason: Instruction limit
% 15.70/5.10 % (3333213)Termination phase: SInE selection
% 15.70/5.10 % (3333213)Time elapsed: 0.093 s
% 15.70/5.10 % (3333213)Peak memory usage: 139 MB
% 15.70/5.10 % (3333213)Instructions burned: 120 (million)
% 15.70/5.10 % (3333223)lrs+10_1_sil=8000:sp=occurrence:random_seed=1228158134:i=285:sd=3:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/285Mi)
% 15.70/5.10 % (3333224)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1127107222:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/157Mi)
% 15.70/5.10 % (3333225)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3301103081:i=325:sd=1:ss=axioms:sgt=32_2973 on theBenchmark for (2973ds/325Mi)
% 15.70/5.10 % (3333226)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=3160130737:s2a=on:i=248:s2at=1.23:gtg=position_2973 on theBenchmark for (2973ds/248Mi)
% 15.70/5.10 % (3333223)Instruction limit reached!
% 23.96/6.22 % (3333223)------------------------------
% 23.96/6.22 % (3333223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.96/6.22 % (3333223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.96/6.22 % (3333223)CaDiCaL version: 2.1.3
% 23.96/6.22 % (3333223)Termination reason: Instruction limit
% 23.96/6.22 % (3333223)Termination phase: Preprocessing 3
% 23.96/6.22 % (3333223)Time elapsed: 0.137 s
% 23.96/6.22 % (3333223)Peak memory usage: 142 MB
% 23.96/6.22 % (3333223)Instructions burned: 287 (million)
% 23.96/6.22 % (3333224)Instruction limit reached!
% 23.96/6.22 % (3333224)------------------------------
% 23.96/6.22 % (3333224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.96/6.22 % (3333224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.96/6.22 % (3333224)CaDiCaL version: 2.1.3
% 23.96/6.22 % (3333224)Termination reason: Instruction limit
% 23.96/6.22 % (3333224)Termination phase: Property scanning
% 23.96/6.22 % (3333224)Time elapsed: 0.071 s
% 23.96/6.22 % (3333224)Peak memory usage: 139 MB
% 23.96/6.22 % (3333224)Instructions burned: 158 (million)
% 23.96/6.22 % (3333226)Instruction limit reached!
% 23.96/6.22 % (3333226)------------------------------
% 23.96/6.22 % (3333226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.96/6.22 % (3333226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.96/6.22 % (3333226)CaDiCaL version: 2.1.3
% 23.96/6.22 % (3333226)Termination reason: Instruction limit
% 23.96/6.22 % (3333226)Termination phase: Property scanning
% 23.96/6.22 % (3333226)Time elapsed: 0.108 s
% 23.96/6.22 % (3333226)Peak memory usage: 139 MB
% 23.96/6.22 % (3333226)Instructions burned: 250 (million)
% 23.96/6.22 % (3333231)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1738373055:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2972 on theBenchmark for (2972ds/294Mi)
% 23.96/6.22 % (3333232)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3648550477:i=2350_2971 on theBenchmark for (2971ds/2350Mi)
% 23.96/6.22 % (3333225)Instruction limit reached!
% 23.96/6.22 % (3333225)------------------------------
% 23.96/6.22 % (3333225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.96/6.23 % (3333225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.96/6.23 % (3333225)CaDiCaL version: 2.1.3
% 23.96/6.23 % (3333225)Termination reason: Instruction limit
% 23.96/6.23 % (3333225)Termination phase: Saturation
% 23.96/6.23 % (3333225)Time elapsed: 0.254 s
% 23.96/6.23 % (3333225)Peak memory usage: 145 MB
% 23.96/6.23 % (3333225)Instructions burned: 326 (million)
% 23.96/6.23 % (3333231)Instruction limit reached!
% 23.96/6.23 % (3333231)------------------------------
% 23.96/6.23 % (3333231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.96/6.23 % (3333231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.96/6.23 % (3333231)CaDiCaL version: 2.1.3
% 23.96/6.23 % (3333231)Termination reason: Instruction limit
% 23.96/6.23 % (3333231)Termination phase: SInE selection
% 23.96/6.23 % (3333231)Time elapsed: 0.106 s
% 23.96/6.23 % (3333231)Peak memory usage: 139 MB
% 23.96/6.23 % (3333231)Instructions burned: 298 (million)
% 23.96/6.23 % (3333233)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=641062720:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 23.96/6.23 % (3333233)Instruction limit reached!
% 23.96/6.23 % (3333233)------------------------------
% 23.96/6.23 % (3333233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.96/6.23 % (3333233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.96/6.23 % (3333233)CaDiCaL version: 2.1.3
% 23.96/6.23 % (3333233)Termination reason: Instruction limit
% 23.96/6.23 % (3333233)Termination phase: SInE selection
% 23.96/6.23 % (3333233)Time elapsed: 0.092 s
% 23.96/6.23 % (3333233)Peak memory usage: 139 MB
% 23.96/6.23 % (3333233)Instructions burned: 114 (million)
% 23.96/6.23 % (3333237)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3971272847:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 23.96/6.23 % (3333237)Instruction limit reached!
% 23.96/6.23 % (3333237)------------------------------
% 23.96/6.23 % (3333237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.96/6.23 % (3333237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.96/6.23 % (3333237)CaDiCaL version: 2.1.3
% 49.50/9.88 % (3333237)Termination reason: Instruction limit
% 49.50/9.88 % (3333237)Termination phase: Property scanning
% 49.50/9.88 % (3333237)Time elapsed: 0.029 s
% 49.50/9.88 % (3333237)Peak memory usage: 139 MB
% 49.50/9.88 % (3333237)Instructions burned: 117 (million)
% 49.50/9.88 % (3333236)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=28275829:i=127:av=off:fsr=off:sup=off_2969 on theBenchmark for (2969ds/127Mi)
% 49.50/9.88 % (3333236)Instruction limit reached!
% 49.50/9.88 % (3333236)------------------------------
% 49.50/9.88 % (3333236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/9.88 % (3333236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/9.88 % (3333236)CaDiCaL version: 2.1.3
% 49.50/9.88 % (3333236)Termination reason: Instruction limit
% 49.50/9.88 % (3333236)Termination phase: Preprocessing 1
% 49.50/9.88 % (3333236)Time elapsed: 0.096 s
% 49.50/9.88 % (3333236)Peak memory usage: 140 MB
% 49.50/9.88 % (3333236)Instructions burned: 128 (million)
% 49.50/9.88 % (3333239)lrs+10_1_sil=8000:sp=occurrence:random_seed=2280076697:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2968 on theBenchmark for (2968ds/907Mi)
% 49.50/9.88 % (3333241)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3220087287:i=437:sd=1:aac=none:ss=included_2967 on theBenchmark for (2967ds/437Mi)
% 49.50/9.88 % (3333243)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2900247105:i=5202:ss=axioms:sgt=16_2966 on theBenchmark for (2966ds/5202Mi)
% 49.50/9.88 % (3333241)Instruction limit reached!
% 49.50/9.88 % (3333241)------------------------------
% 49.50/9.88 % (3333241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/9.88 % (3333241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/9.88 % (3333241)CaDiCaL version: 2.1.3
% 49.50/9.88 % (3333241)Termination reason: Instruction limit
% 49.50/9.88 % (3333241)Termination phase: Saturation
% 49.50/9.88 % (3333241)Time elapsed: 0.177 s
% 49.50/9.88 % (3333241)Peak memory usage: 146 MB
% 49.50/9.88 % (3333241)Instructions burned: 438 (million)
% 49.50/9.88 % (3333247)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=653614982:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2964 on theBenchmark for (2964ds/134Mi)
% 49.50/9.88 % (3333247)Instruction limit reached!
% 49.50/9.88 % (3333247)------------------------------
% 49.50/9.88 % (3333247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/9.88 % (3333247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/9.88 % (3333247)CaDiCaL version: 2.1.3
% 49.50/9.88 % (3333247)Termination reason: Instruction limit
% 49.50/9.88 % (3333247)Termination phase: SInE selection
% 49.50/9.88 % (3333247)Time elapsed: 0.058 s
% 49.50/9.88 % (3333247)Peak memory usage: 139 MB
% 49.50/9.88 % (3333247)Instructions burned: 135 (million)
% 49.50/9.88 % (3333249)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=597765774:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 49.50/9.88 % (3333239)Instruction limit reached!
% 49.50/9.88 % (3333239)------------------------------
% 49.50/9.88 % (3333239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/9.88 % (3333239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/9.88 % (3333239)CaDiCaL version: 2.1.3
% 49.50/9.88 % (3333239)Termination reason: Instruction limit
% 49.50/9.88 % (3333239)Termination phase: Property scanning
% 49.50/9.88 % (3333239)Time elapsed: 0.593 s
% 49.50/9.88 % (3333239)Peak memory usage: 158 MB
% 49.50/9.88 % (3333239)Instructions burned: 908 (million)
% 49.50/9.88 % (3333249)Instruction limit reached!
% 49.50/9.88 % (3333249)------------------------------
% 49.50/9.88 % (3333249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/9.88 % (3333249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/9.88 % (3333249)CaDiCaL version: 2.1.3
% 49.50/9.88 % (3333249)Termination reason: Instruction limit
% 49.50/9.88 % (3333249)Termination phase: Preprocessing 1
% 49.50/9.88 % (3333249)Time elapsed: 0.251 s
% 49.50/9.88 % (3333249)Peak memory usage: 142 MB
% 49.50/9.88 % (3333249)Instructions burned: 594 (million)
% 49.50/9.88 % (3333251)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=238504129:st=3:i=13193:sd=3:ss=axioms_2960 on theBenchmark for (2960ds/13193Mi)
% 49.50/9.88 % (3333252)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=2608922468:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2958 on theBenchmark for (2958ds/125Mi)
% 38.76/11.51 % (3333252)Instruction limit reached!
% 38.76/11.51 % (3333252)------------------------------
% 38.76/11.51 % (3333252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333252)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333252)Termination reason: Instruction limit
% 38.76/11.51 % (3333252)Termination phase: Property scanning
% 38.76/11.51 % (3333252)Time elapsed: 0.032 s
% 38.76/11.51 % (3333252)Peak memory usage: 139 MB
% 38.76/11.51 % (3333252)Instructions burned: 130 (million)
% 38.76/11.51 % (3333255)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1723261347:i=134:gtgl=5:slsql=off:gtg=exists_sym_2957 on theBenchmark for (2957ds/134Mi)
% 38.76/11.51 % (3333255)Instruction limit reached!
% 38.76/11.51 % (3333255)------------------------------
% 38.76/11.51 % (3333255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333255)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333255)Termination reason: Instruction limit
% 38.76/11.51 % (3333255)Termination phase: Property scanning
% 38.76/11.51 % (3333255)Time elapsed: 0.034 s
% 38.76/11.51 % (3333255)Peak memory usage: 139 MB
% 38.76/11.51 % (3333255)Instructions burned: 138 (million)
% 38.76/11.51 % (3333232)Instruction limit reached!
% 38.76/11.51 % (3333232)------------------------------
% 38.76/11.51 % (3333232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333232)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333232)Termination reason: Instruction limit
% 38.76/11.51 % (3333232)Termination phase: Property scanning
% 38.76/11.51 % (3333232)Time elapsed: 1.602 s
% 38.76/11.51 % (3333232)Peak memory usage: 242 MB
% 38.76/11.51 % (3333232)Instructions burned: 2353 (million)
% 38.76/11.51 % (3333257)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3842566310:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/141Mi)
% 38.76/11.51 % (3333257)Instruction limit reached!
% 38.76/11.51 % (3333257)------------------------------
% 38.76/11.51 % (3333257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333257)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333257)Termination reason: Instruction limit
% 38.76/11.51 % (3333257)Termination phase: SInE selection
% 38.76/11.51 % (3333257)Time elapsed: 0.061 s
% 38.76/11.51 % (3333257)Peak memory usage: 139 MB
% 38.76/11.51 % (3333257)Instructions burned: 142 (million)
% 38.76/11.51 % (3333258)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3767740139:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2954 on theBenchmark for (2954ds/431Mi)
% 38.76/11.51 % (3333260)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=1780220973:i=6060:aac=none:ins=25_2953 on theBenchmark for (2953ds/6060Mi)
% 38.76/11.51 % (3333258)Instruction limit reached!
% 38.76/11.51 % (3333258)------------------------------
% 38.76/11.51 % (3333258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333258)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333258)Termination reason: Instruction limit
% 38.76/11.51 % (3333258)Termination phase: Saturation
% 38.76/11.51 % (3333258)Time elapsed: 0.320 s
% 38.76/11.51 % (3333258)Peak memory usage: 147 MB
% 38.76/11.51 % (3333258)Instructions burned: 432 (million)
% 38.76/11.51 % (3333263)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4243854734:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2949 on theBenchmark for (2949ds/150Mi)
% 38.76/11.51 % (3333263)Instruction limit reached!
% 38.76/11.51 % (3333263)------------------------------
% 38.76/11.51 % (3333263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333263)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333263)Termination reason: Instruction limit
% 38.76/11.51 % (3333263)Termination phase: SInE selection
% 38.76/11.51 % (3333263)Time elapsed: 0.114 s
% 38.76/11.51 % (3333263)Peak memory usage: 139 MB
% 38.76/11.51 % (3333263)Instructions burned: 150 (million)
% 38.76/11.51 % (3333265)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2662129083:i=14155:bd=all_2946 on theBenchmark for (2946ds/14155Mi)
% 38.76/11.51 % (3333243)Instruction limit reached!
% 38.76/11.51 % (3333243)------------------------------
% 38.76/11.51 % (3333243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333243)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333243)Termination reason: Instruction limit
% 38.76/11.51 % (3333243)Termination phase: Saturation
% 38.76/11.51 % (3333243)Time elapsed: 3.247 s
% 38.76/11.51 % (3333243)Peak memory usage: 265 MB
% 38.76/11.51 % (3333243)Instructions burned: 5203 (million)
% 38.76/11.51 % (3333267)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1145999908:i=667:av=off:fsr=off_2932 on theBenchmark for (2932ds/667Mi)
% 38.76/11.51 % (3333260)Instruction limit reached!
% 38.76/11.51 % (3333260)------------------------------
% 38.76/11.51 % (3333260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333260)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333260)Termination reason: Instruction limit
% 38.76/11.51 % (3333260)Termination phase: Function definition elimination
% 38.76/11.51 % (3333260)Time elapsed: 2.197 s
% 38.76/11.51 % (3333260)Peak memory usage: 254 MB
% 38.76/11.51 % (3333260)Instructions burned: 6060 (million)
% 38.76/11.51 % (3333269)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2435645809:s2a=on:i=185:s2at=1.8:fdi=4_2930 on theBenchmark for (2930ds/185Mi)
% 38.76/11.51 % (3333269)Instruction limit reached!
% 38.76/11.51 % (3333269)------------------------------
% 38.76/11.51 % (3333269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333269)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333269)Termination reason: Instruction limit
% 38.76/11.51 % (3333269)Termination phase: SInE selection
% 38.76/11.51 % (3333269)Time elapsed: 0.074 s
% 38.76/11.51 % (3333269)Peak memory usage: 139 MB
% 38.76/11.51 % (3333269)Instructions burned: 188 (million)
% 38.76/11.51 % (3333271)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2836103826:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2927 on theBenchmark for (2927ds/193Mi)
% 38.76/11.51 % (3333271)Instruction limit reached!
% 38.76/11.51 % (3333271)------------------------------
% 38.76/11.51 % (3333271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333271)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333271)Termination reason: Instruction limit
% 38.76/11.51 % (3333271)Termination phase: SInE selection
% 38.76/11.51 % (3333271)Time elapsed: 0.086 s
% 38.76/11.51 % (3333271)Peak memory usage: 139 MB
% 38.76/11.51 % (3333271)Instructions burned: 195 (million)
% 38.76/11.51 % (3333267)Instruction limit reached!
% 38.76/11.51 % (3333267)------------------------------
% 38.76/11.51 % (3333267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333267)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333267)Termination reason: Instruction limit
% 38.76/11.51 % (3333267)Termination phase: NewCNF
% 38.76/11.51 % (3333267)Time elapsed: 0.546 s
% 38.76/11.51 % (3333267)Peak memory usage: 190 MB
% 38.76/11.51 % (3333267)Instructions burned: 668 (million)
% 38.76/11.51 % (3333273)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2337097521:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2925 on theBenchmark for (2925ds/4850Mi)
% 38.76/11.51 % (3333274)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2311630224:i=12111:sd=1:ss=included_2925 on theBenchmark for (2925ds/12111Mi)
% 38.76/11.51 % (3333273)Instruction limit reached!
% 38.76/11.51 % (3333273)------------------------------
% 38.76/11.51 % (3333273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333273)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333273)Termination reason: Instruction limit
% 38.76/11.51 % (3333273)Termination phase: Property scanning
% 38.76/11.51 % (3333273)Time elapsed: 1.470 s
% 38.76/11.51 % (3333273)Peak memory usage: 227 MB
% 38.76/11.51 % (3333273)Instructions burned: 4856 (million)
% 38.76/11.51 % (3333277)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2939491049:i=319:kws=precedence:fsr=off_2909 on theBenchmark for (2909ds/319Mi)
% 38.76/11.51 % (3333277)Instruction limit reached!
% 38.76/11.51 % (3333277)------------------------------
% 38.76/11.51 % (3333277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333277)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333277)Termination reason: Instruction limit
% 38.76/11.51 % (3333277)Termination phase: Unused predicate definition removal
% 38.76/11.51 % (3333277)Time elapsed: 0.139 s
% 38.76/11.51 % (3333277)Peak memory usage: 143 MB
% 38.76/11.51 % (3333277)Instructions burned: 320 (million)
% 38.76/11.51 % (3333279)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2331296269:i=2064:ep=RST_2906 on theBenchmark for (2906ds/2064Mi)
% 38.76/11.51 % (3333251)First to succeed.
% 38.76/11.51 % (3333251)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3333204"
% 38.76/11.51 % (3333279)Instruction limit reached!
% 38.76/11.51 % (3333279)------------------------------
% 38.76/11.51 % (3333279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.76/11.51 % (3333279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/11.51 % (3333279)CaDiCaL version: 2.1.3
% 38.76/11.51 % (3333279)Termination reason: Instruction limit
% 38.76/11.51 % (3333279)Termination phase: Property scanning
% 38.76/11.51 % (3333279)Time elapsed: 0.778 s
% 38.76/11.51 % (3333279)Peak memory usage: 241 MB
% 38.76/11.51 % (3333279)Instructions burned: 2069 (million)
% 38.76/11.51 % (3333281)dis-1011_128_sil=32000:random_seed=1131795289:i=3706:ep=RST:av=off_2897 on theBenchmark for (2897ds/3706Mi)
% 38.76/11.51 % (3333251)Refutation found. Thanks to Tanya!
% 38.76/11.51 % SZS status Theorem for theBenchmark
% 38.76/11.51 % SZS output start Proof for theBenchmark
% See solution above
% 61.09/11.77 % (3333251)------------------------------
% 61.09/11.77 % (3333251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.09/11.77 % (3333251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.09/11.77 % (3333251)CaDiCaL version: 2.1.3
% 61.09/11.77 % (3333251)Termination reason: Refutation
% 61.09/11.77 % (3333251)Time elapsed: 6.044 s
% 61.09/11.77 % (3333251)Peak memory usage: 424 MB
% 61.09/11.77 % (3333251)Instructions burned: 10001 (million)
% 61.09/11.77 % (3333251)------------------------------
% 61.09/11.77 % (3333251)------------------------------
% 61.09/11.77 % (3333204)Success in time 10.649 s
% 61.09/11.77 % Vampire exiting
%------------------------------------------------------------------------------