%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP637+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 26.59s 4.87s
% Output : Refutation 27.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 16
% Syntax : Number of formulae : 145 ( 37 unt; 6 def)
% Number of atoms : 568 ( 29 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 699 ( 276 ~; 271 |; 109 &)
% ( 13 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 7 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-4 aty)
% Number of variables : 149 ( 0 sgn 135 !; 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/sandbox/benchmark/theBenchmark.p',t156_relat_1) ).
fof(f1257,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1316,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/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1318,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1890,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/sandbox/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f4388,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/sandbox/benchmark/theBenchmark.p',d5_group_2) ).
fof(f4410,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/sandbox/benchmark/theBenchmark.p',t66_group_2) ).
fof(f4540,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/sandbox/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f5350,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/sandbox/benchmark/theBenchmark.p',redefinition_m1_group_6) ).
fof(f5648,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/sandbox/benchmark/theBenchmark.p',t10_latsubgr) ).
fof(f5649,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)],[f5648]) ).
fof(f5827,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,[],[f5649]) ).
fof(f5828,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,[],[f5827]) ).
fof(f5897,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,[],[f1316]) ).
fof(f5932,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,[],[f1890]) ).
fof(f5933,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,[],[f5932]) ).
fof(f5960,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,[],[f4540]) ).
fof(f5961,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,[],[f5960]) ).
fof(f5962,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,[],[f4410]) ).
fof(f5963,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,[],[f5962]) ).
fof(f5992,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,[],[f5350]) ).
fof(f5993,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,[],[f5992]) ).
fof(f6124,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1257]) ).
fof(f6504,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(f6505,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,[],[f6504]) ).
fof(f7048,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,[],[f4388]) ).
fof(f7049,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,[],[f7048]) ).
fof(f9040,plain,
( ~ m1_group_6(sK47,sK43,sK48)
& u1_struct_0(sK47) = k2_funct_2(u1_struct_0(sK42),u1_struct_0(sK43),sK44,u1_struct_0(sK45))
& u1_struct_0(sK48) = k2_funct_2(u1_struct_0(sK42),u1_struct_0(sK43),sK44,u1_struct_0(sK46))
& m1_group_6(sK45,sK42,sK46)
& m1_group_2(sK48,sK43)
& m1_group_2(sK47,sK43)
& m1_group_2(sK46,sK42)
& m1_group_2(sK45,sK42)
& v1_funct_1(sK44)
& v1_funct_2(sK44,u1_struct_0(sK42),u1_struct_0(sK43))
& v1_group_6(sK44,sK42,sK43)
& m2_relset_1(sK44,u1_struct_0(sK42),u1_struct_0(sK43))
& ~ v3_struct_0(sK43)
& v3_group_1(sK43)
& v4_group_1(sK43)
& l1_group_1(sK43)
& ~ v3_struct_0(sK42)
& v3_group_1(sK42)
& v4_group_1(sK42)
& l1_group_1(sK42) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42,sK43,sK44,sK45,sK46,sK47,sK48]),skolemize(X0,sK42),skolemize(X1,sK43),skolemize(X2,sK44),skolemize(X3,sK45),skolemize(X4,sK46),skolemize(X5,sK47),skolemize(X6,sK48)],[f5828]) ).
fof(f9065,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,[],[f5993]) ).
fof(f9270,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,[],[f1318]) ).
fof(f9464,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,[],[f7049]) ).
fof(f9465,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,[],[f9464]) ).
fof(f9965,plain,
l1_group_1(sK42),
inference(cnf_transformation,[],[f9040]) ).
fof(f9966,plain,
v4_group_1(sK42),
inference(cnf_transformation,[],[f9040]) ).
fof(f9967,plain,
v3_group_1(sK42),
inference(cnf_transformation,[],[f9040]) ).
fof(f9968,plain,
~ v3_struct_0(sK42),
inference(cnf_transformation,[],[f9040]) ).
fof(f9969,plain,
l1_group_1(sK43),
inference(cnf_transformation,[],[f9040]) ).
fof(f9970,plain,
v4_group_1(sK43),
inference(cnf_transformation,[],[f9040]) ).
fof(f9971,plain,
v3_group_1(sK43),
inference(cnf_transformation,[],[f9040]) ).
fof(f9972,plain,
~ v3_struct_0(sK43),
inference(cnf_transformation,[],[f9040]) ).
fof(f9973,plain,
m2_relset_1(sK44,u1_struct_0(sK42),u1_struct_0(sK43)),
inference(cnf_transformation,[],[f9040]) ).
fof(f9975,plain,
v1_funct_2(sK44,u1_struct_0(sK42),u1_struct_0(sK43)),
inference(cnf_transformation,[],[f9040]) ).
fof(f9976,plain,
v1_funct_1(sK44),
inference(cnf_transformation,[],[f9040]) ).
fof(f9978,plain,
m1_group_2(sK46,sK42),
inference(cnf_transformation,[],[f9040]) ).
fof(f9979,plain,
m1_group_2(sK47,sK43),
inference(cnf_transformation,[],[f9040]) ).
fof(f9980,plain,
m1_group_2(sK48,sK43),
inference(cnf_transformation,[],[f9040]) ).
fof(f9981,plain,
m1_group_6(sK45,sK42,sK46),
inference(cnf_transformation,[],[f9040]) ).
fof(f9982,plain,
u1_struct_0(sK48) = k2_funct_2(u1_struct_0(sK42),u1_struct_0(sK43),sK44,u1_struct_0(sK46)),
inference(cnf_transformation,[],[f9040]) ).
fof(f9983,plain,
u1_struct_0(sK47) = k2_funct_2(u1_struct_0(sK42),u1_struct_0(sK43),sK44,u1_struct_0(sK45)),
inference(cnf_transformation,[],[f9040]) ).
fof(f9984,plain,
~ m1_group_6(sK47,sK43,sK48),
inference(cnf_transformation,[],[f9040]) ).
fof(f10067,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,[],[f5897]) ).
fof(f10102,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,[],[f5933]) ).
fof(f10127,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,[],[f5961]) ).
fof(f10128,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,[],[f5961]) ).
fof(f10129,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,[],[f5961]) ).
fof(f10130,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,[],[f5963]) ).
fof(f10160,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,[],[f9065]) ).
fof(f10161,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,[],[f9065]) ).
fof(f10386,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f6124]) ).
fof(f10862,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f9270]) ).
fof(f10957,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,[],[f6505]) ).
fof(f11619,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,[],[f9465]) ).
fof(f15304,plain,
( ~ m1_group_2(sK47,sK48)
| v3_struct_0(sK43)
| ~ v3_group_1(sK43)
| ~ v4_group_1(sK43)
| ~ l1_group_1(sK43)
| ~ m1_group_2(sK48,sK43) ),
inference(resolution,[],[f10161,f9984]) ).
fof(f15305,plain,
( m1_group_2(sK45,sK46)
| v3_struct_0(sK42)
| ~ v3_group_1(sK42)
| ~ v4_group_1(sK42)
| ~ l1_group_1(sK42)
| ~ m1_group_2(sK46,sK42) ),
inference(resolution,[],[f10160,f9981]) ).
fof(f15311,plain,
( ~ v3_struct_0(sK46)
| v3_struct_0(sK42)
| ~ v3_group_1(sK42)
| ~ l1_group_1(sK42) ),
inference(resolution,[],[f10129,f9978]) ).
fof(f15312,plain,
( ~ v3_struct_0(sK46)
| ~ v3_group_1(sK42)
| ~ l1_group_1(sK42) ),
inference(forward_subsumption_resolution,[],[f15311,f9968]) ).
fof(f15316,plain,
( ~ v3_struct_0(sK46)
| ~ l1_group_1(sK42) ),
inference(forward_subsumption_resolution,[],[f15312,f9967]) ).
fof(f15320,plain,
~ v3_struct_0(sK46),
inference(forward_subsumption_resolution,[],[f15316,f9965]) ).
fof(f15324,plain,
! [X0] :
( ~ v1_funct_1(sK44)
| k9_relat_1(sK44,X0) = k2_funct_2(u1_struct_0(sK42),u1_struct_0(sK43),sK44,X0)
| ~ m1_relset_1(sK44,u1_struct_0(sK42),u1_struct_0(sK43)) ),
inference(resolution,[],[f10102,f9975]) ).
fof(f15325,plain,
! [X0] :
( k9_relat_1(sK44,X0) = k2_funct_2(u1_struct_0(sK42),u1_struct_0(sK43),sK44,X0)
| ~ m1_relset_1(sK44,u1_struct_0(sK42),u1_struct_0(sK43)) ),
inference(forward_subsumption_resolution,[],[f15324,f9976]) ).
fof(f15327,definition,
( spl533_17
<=> m1_relset_1(sK44,u1_struct_0(sK42),u1_struct_0(sK43)) ),
introduced(definition,[new_symbols(definition,[spl533_17])],[avatar_definition]) ).
fof(f15329,plain,
( ~ m1_relset_1(sK44,u1_struct_0(sK42),u1_struct_0(sK43))
| spl533_17 ),
inference(avatar_component_clause,[],[f15327]) ).
fof(f15331,definition,
( spl533_18
<=> ! [X0] : k9_relat_1(sK44,X0) = k2_funct_2(u1_struct_0(sK42),u1_struct_0(sK43),sK44,X0) ),
introduced(definition,[new_symbols(definition,[spl533_18])],[avatar_definition]) ).
fof(f15332,plain,
( ! [X0] : k9_relat_1(sK44,X0) = k2_funct_2(u1_struct_0(sK42),u1_struct_0(sK43),sK44,X0)
| ~ spl533_18 ),
inference(avatar_component_clause,[],[f15331]) ).
fof(f15333,plain,
( ~ spl533_17
| spl533_18 ),
inference(avatar_split_clause,[],[f15325,f15331,f15327]) ).
fof(f15346,plain,
m1_relset_1(sK44,u1_struct_0(sK42),u1_struct_0(sK43)),
inference(resolution,[],[f10862,f9973]) ).
fof(f15347,plain,
( $false
| spl533_17 ),
inference(forward_subsumption_resolution,[],[f15346,f15329]) ).
fof(f15348,plain,
spl533_17,
inference(avatar_contradiction_clause,[],[f15347]) ).
fof(f15357,plain,
( u1_struct_0(sK47) = k9_relat_1(sK44,u1_struct_0(sK45))
| ~ spl533_18 ),
inference(superposition,[],[f9983,f15332]) ).
fof(f15358,plain,
( u1_struct_0(sK48) = k9_relat_1(sK44,u1_struct_0(sK46))
| ~ spl533_18 ),
inference(superposition,[],[f9982,f15332]) ).
fof(f15366,plain,
( l1_group_1(sK46)
| v3_struct_0(sK42)
| ~ v3_group_1(sK42)
| ~ l1_group_1(sK42) ),
inference(resolution,[],[f10127,f9978]) ).
fof(f15367,plain,
( l1_group_1(sK46)
| ~ v3_group_1(sK42)
| ~ l1_group_1(sK42) ),
inference(forward_subsumption_resolution,[],[f15366,f9968]) ).
fof(f15371,plain,
( l1_group_1(sK46)
| ~ l1_group_1(sK42) ),
inference(forward_subsumption_resolution,[],[f15367,f9967]) ).
fof(f15375,plain,
l1_group_1(sK46),
inference(forward_subsumption_resolution,[],[f15371,f9965]) ).
fof(f15384,plain,
( v3_group_1(sK46)
| v3_struct_0(sK42)
| ~ v3_group_1(sK42)
| ~ l1_group_1(sK42) ),
inference(resolution,[],[f10128,f9978]) ).
fof(f15385,plain,
( v3_group_1(sK46)
| ~ v3_group_1(sK42)
| ~ l1_group_1(sK42) ),
inference(forward_subsumption_resolution,[],[f15384,f9968]) ).
fof(f15389,plain,
( v3_group_1(sK46)
| ~ l1_group_1(sK42) ),
inference(forward_subsumption_resolution,[],[f15385,f9967]) ).
fof(f15393,plain,
v3_group_1(sK46),
inference(forward_subsumption_resolution,[],[f15389,f9965]) ).
fof(f15468,plain,
( ! [X0] :
( r1_tarski(k9_relat_1(sK44,X0),u1_struct_0(sK48))
| ~ r1_tarski(X0,u1_struct_0(sK46))
| ~ v1_relat_1(sK44) )
| ~ spl533_18 ),
inference(superposition,[],[f10957,f15358]) ).
fof(f15470,definition,
( spl533_19
<=> v1_relat_1(sK44) ),
introduced(definition,[new_symbols(definition,[spl533_19])],[avatar_definition]) ).
fof(f15472,plain,
( ~ v1_relat_1(sK44)
| spl533_19 ),
inference(avatar_component_clause,[],[f15470]) ).
fof(f15474,definition,
( spl533_20
<=> ! [X0] :
( r1_tarski(k9_relat_1(sK44,X0),u1_struct_0(sK48))
| ~ r1_tarski(X0,u1_struct_0(sK46)) ) ),
introduced(definition,[new_symbols(definition,[spl533_20])],[avatar_definition]) ).
fof(f15475,plain,
( ! [X0] :
( r1_tarski(k9_relat_1(sK44,X0),u1_struct_0(sK48))
| ~ r1_tarski(X0,u1_struct_0(sK46)) )
| ~ spl533_20 ),
inference(avatar_component_clause,[],[f15474]) ).
fof(f15476,plain,
( ~ spl533_19
| spl533_20
| ~ spl533_18 ),
inference(avatar_split_clause,[],[f15468,f15331,f15474,f15470]) ).
fof(f15529,plain,
( ~ m1_group_2(sK47,sK48)
| ~ v3_group_1(sK43)
| ~ v4_group_1(sK43)
| ~ l1_group_1(sK43)
| ~ m1_group_2(sK48,sK43) ),
inference(forward_subsumption_resolution,[],[f15304,f9972]) ).
fof(f15530,plain,
( m1_group_2(sK45,sK46)
| ~ v3_group_1(sK42)
| ~ v4_group_1(sK42)
| ~ l1_group_1(sK42)
| ~ m1_group_2(sK46,sK42) ),
inference(forward_subsumption_resolution,[],[f15305,f9968]) ).
fof(f15595,plain,
( ~ m1_group_2(sK47,sK48)
| ~ v4_group_1(sK43)
| ~ l1_group_1(sK43)
| ~ m1_group_2(sK48,sK43) ),
inference(forward_subsumption_resolution,[],[f15529,f9971]) ).
fof(f15596,plain,
( m1_group_2(sK45,sK46)
| ~ v4_group_1(sK42)
| ~ l1_group_1(sK42)
| ~ m1_group_2(sK46,sK42) ),
inference(forward_subsumption_resolution,[],[f15530,f9967]) ).
fof(f15646,plain,
( ~ m1_group_2(sK47,sK48)
| ~ l1_group_1(sK43)
| ~ m1_group_2(sK48,sK43) ),
inference(forward_subsumption_resolution,[],[f15595,f9970]) ).
fof(f15647,plain,
( m1_group_2(sK45,sK46)
| ~ l1_group_1(sK42)
| ~ m1_group_2(sK46,sK42) ),
inference(forward_subsumption_resolution,[],[f15596,f9966]) ).
fof(f15697,plain,
( ~ m1_group_2(sK47,sK48)
| ~ m1_group_2(sK48,sK43) ),
inference(forward_subsumption_resolution,[],[f15646,f9969]) ).
fof(f15698,plain,
( m1_group_2(sK45,sK46)
| ~ m1_group_2(sK46,sK42) ),
inference(forward_subsumption_resolution,[],[f15647,f9965]) ).
fof(f15748,plain,
~ m1_group_2(sK47,sK48),
inference(forward_subsumption_resolution,[],[f15697,f9980]) ).
fof(f15749,plain,
m1_group_2(sK45,sK46),
inference(forward_subsumption_resolution,[],[f15698,f9978]) ).
fof(f16509,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f10386,f10067]) ).
fof(f16511,plain,
v1_relat_1(sK44),
inference(resolution,[],[f16509,f9973]) ).
fof(f16512,plain,
( $false
| spl533_19 ),
inference(forward_subsumption_resolution,[],[f16511,f15472]) ).
fof(f16513,plain,
spl533_19,
inference(avatar_contradiction_clause,[],[f16512]) ).
fof(f16532,plain,
( r1_tarski(u1_struct_0(sK47),u1_struct_0(sK48))
| ~ r1_tarski(u1_struct_0(sK45),u1_struct_0(sK46))
| ~ spl533_18
| ~ spl533_20 ),
inference(superposition,[],[f15475,f15357]) ).
fof(f16535,definition,
( spl533_107
<=> r1_tarski(u1_struct_0(sK45),u1_struct_0(sK46)) ),
introduced(definition,[new_symbols(definition,[spl533_107])],[avatar_definition]) ).
fof(f16537,plain,
( ~ r1_tarski(u1_struct_0(sK45),u1_struct_0(sK46))
| spl533_107 ),
inference(avatar_component_clause,[],[f16535]) ).
fof(f16539,definition,
( spl533_108
<=> r1_tarski(u1_struct_0(sK47),u1_struct_0(sK48)) ),
introduced(definition,[new_symbols(definition,[spl533_108])],[avatar_definition]) ).
fof(f16541,plain,
( r1_tarski(u1_struct_0(sK47),u1_struct_0(sK48))
| ~ spl533_108 ),
inference(avatar_component_clause,[],[f16539]) ).
fof(f16542,plain,
( ~ spl533_107
| spl533_108
| ~ spl533_18
| ~ spl533_20 ),
inference(avatar_split_clause,[],[f16532,f15474,f15331,f16539,f16535]) ).
fof(f16543,plain,
( ~ m1_group_2(sK45,sK46)
| v3_struct_0(sK45)
| ~ v3_group_1(sK45)
| ~ l1_group_1(sK45)
| v3_struct_0(sK46)
| ~ v3_group_1(sK46)
| ~ l1_group_1(sK46)
| spl533_107 ),
inference(resolution,[],[f16537,f11619]) ).
fof(f16544,plain,
( ~ m1_group_2(sK45,sK46)
| ~ v3_group_1(sK45)
| ~ l1_group_1(sK45)
| v3_struct_0(sK46)
| ~ v3_group_1(sK46)
| ~ l1_group_1(sK46)
| spl533_107 ),
inference(forward_subsumption_resolution,[],[f16543,f10129]) ).
fof(f16545,plain,
( ~ m1_group_2(sK45,sK46)
| ~ l1_group_1(sK45)
| v3_struct_0(sK46)
| ~ v3_group_1(sK46)
| ~ l1_group_1(sK46)
| spl533_107 ),
inference(forward_subsumption_resolution,[],[f16544,f10128]) ).
fof(f16546,plain,
( ~ m1_group_2(sK45,sK46)
| v3_struct_0(sK46)
| ~ v3_group_1(sK46)
| ~ l1_group_1(sK46)
| spl533_107 ),
inference(forward_subsumption_resolution,[],[f16545,f10127]) ).
fof(f16547,plain,
( v3_struct_0(sK46)
| ~ v3_group_1(sK46)
| ~ l1_group_1(sK46)
| spl533_107 ),
inference(forward_subsumption_resolution,[],[f16546,f15749]) ).
fof(f16548,plain,
( ~ v3_group_1(sK46)
| ~ l1_group_1(sK46)
| spl533_107 ),
inference(forward_subsumption_resolution,[],[f16547,f15320]) ).
fof(f16549,plain,
( ~ l1_group_1(sK46)
| spl533_107 ),
inference(forward_subsumption_resolution,[],[f16548,f15393]) ).
fof(f16550,plain,
( $false
| spl533_107 ),
inference(forward_subsumption_resolution,[],[f16549,f15375]) ).
fof(f16551,plain,
spl533_107,
inference(avatar_contradiction_clause,[],[f16550]) ).
fof(f16552,plain,
( ! [X0] :
( m1_group_2(sK47,sK48)
| ~ m1_group_2(sK48,X0)
| ~ m1_group_2(sK47,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl533_108 ),
inference(resolution,[],[f16541,f10130]) ).
fof(f16553,plain,
( ! [X0] :
( ~ m1_group_2(sK48,X0)
| ~ m1_group_2(sK47,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl533_108 ),
inference(forward_subsumption_resolution,[],[f16552,f15748]) ).
fof(f16556,plain,
( ~ m1_group_2(sK47,sK43)
| v3_struct_0(sK43)
| ~ v3_group_1(sK43)
| ~ v4_group_1(sK43)
| ~ l1_group_1(sK43)
| ~ spl533_108 ),
inference(resolution,[],[f16553,f9980]) ).
fof(f16557,plain,
( v3_struct_0(sK43)
| ~ v3_group_1(sK43)
| ~ v4_group_1(sK43)
| ~ l1_group_1(sK43)
| ~ spl533_108 ),
inference(forward_subsumption_resolution,[],[f16556,f9979]) ).
fof(f16560,plain,
( ~ v3_group_1(sK43)
| ~ v4_group_1(sK43)
| ~ l1_group_1(sK43)
| ~ spl533_108 ),
inference(forward_subsumption_resolution,[],[f16557,f9972]) ).
fof(f16561,plain,
( ~ v4_group_1(sK43)
| ~ l1_group_1(sK43)
| ~ spl533_108 ),
inference(forward_subsumption_resolution,[],[f16560,f9971]) ).
fof(f16562,plain,
( ~ l1_group_1(sK43)
| ~ spl533_108 ),
inference(forward_subsumption_resolution,[],[f16561,f9970]) ).
fof(f16563,plain,
( $false
| ~ spl533_108 ),
inference(forward_subsumption_resolution,[],[f16562,f9969]) ).
fof(f16564,plain,
~ spl533_108,
inference(avatar_contradiction_clause,[],[f16563]) ).
cnf(s14,plain,
( ~ spl533_17
| spl533_18 ),
inference(sat_conversion,[],[f15333]) ).
cnf(s15,plain,
spl533_17,
inference(sat_conversion,[],[f15348]) ).
cnf(s16,plain,
( ~ spl533_18
| ~ spl533_19
| spl533_20 ),
inference(sat_conversion,[],[f15476]) ).
cnf(s83,plain,
spl533_19,
inference(sat_conversion,[],[f16513]) ).
cnf(s85,plain,
( ~ spl533_18
| ~ spl533_20
| ~ spl533_107
| spl533_108 ),
inference(sat_conversion,[],[f16542]) ).
cnf(s86,plain,
spl533_107,
inference(sat_conversion,[],[f16551]) ).
cnf(s87,plain,
~ spl533_108,
inference(sat_conversion,[],[f16564]) ).
cnf(s88,plain,
( ~ spl533_18
| ~ spl533_20 ),
inference(rat,[],[s85,s87,s86]) ).
cnf(s92,plain,
( ~ spl533_18
| spl533_20 ),
inference(rat,[],[s16,s83]) ).
cnf(s93,plain,
spl533_18,
inference(rat,[],[s14,s15]) ).
cnf(s94,plain,
~ spl533_20,
inference(rat,[],[s88,s93]) ).
cnf(s98,plain,
$false,
inference(rat,[],[s92,s94,s93]) ).
fof(f16565,plain,
$false,
inference(avatar_sat_refutation,[],[s98]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP637+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n009.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 10:19:45 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.87/3.18 % (1813819)Detected formulas, will run a generic FOF schedule.
% 14.87/3.18 % (1814142)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=2711546524:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 14.87/3.18 % (1814147)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=717251306:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 14.87/3.18 % (1814151)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=123699268:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 14.87/3.18 % (1814144)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=2358200355:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 14.87/3.18 % (1814148)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1958334226:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 14.87/3.18 % (1814146)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=3050118971:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 14.87/3.18 % (1814152)dis-21_1_sil=8000:lcm=predicate:random_seed=4219159090:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 14.87/3.18 % (1814147)Instruction limit reached!
% 14.87/3.18 % (1814147)------------------------------
% 14.87/3.18 % (1814147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.87/3.18 % (1814147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/3.18 % (1814147)CaDiCaL version: 2.1.3
% 14.87/3.18 % (1814147)Termination reason: Instruction limit
% 14.87/3.18 % (1814147)Termination phase: Saturation
% 14.87/3.18 % (1814147)Time elapsed: 0.067 s
% 14.87/3.18 % (1814147)Peak memory usage: 95 MB
% 14.87/3.18 % (1814147)Instructions burned: 109 (million)
% 14.87/3.18 % (1814148)Instruction limit reached!
% 14.87/3.18 % (1814148)------------------------------
% 14.87/3.18 % (1814148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.87/3.18 % (1814148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/3.18 % (1814148)CaDiCaL version: 2.1.3
% 14.87/3.18 % (1814148)Termination reason: Instruction limit
% 14.87/3.18 % (1814148)Termination phase: Saturation
% 14.87/3.18 % (1814148)Time elapsed: 0.077 s
% 14.87/3.18 % (1814148)Peak memory usage: 96 MB
% 14.87/3.18 % (1814148)Instructions burned: 120 (million)
% 14.87/3.18 % (1814151)Instruction limit reached!
% 14.87/3.18 % (1814151)------------------------------
% 14.87/3.18 % (1814151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.87/3.18 % (1814151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/3.18 % (1814151)CaDiCaL version: 2.1.3
% 14.87/3.18 % (1814151)Termination reason: Instruction limit
% 14.87/3.18 % (1814151)Termination phase: Preprocessing 2
% 14.87/3.18 % (1814151)Time elapsed: 0.086 s
% 14.87/3.18 % (1814151)Peak memory usage: 92 MB
% 14.87/3.18 % (1814151)Instructions burned: 140 (million)
% 14.87/3.18 % (1814152)Instruction limit reached!
% 14.87/3.18 % (1814152)------------------------------
% 14.87/3.18 % (1814152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.87/3.18 % (1814152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.87/3.18 % (1814152)CaDiCaL version: 2.1.3
% 14.87/3.18 % (1814152)Termination reason: Instruction limit
% 14.87/3.18 % (1814152)Termination phase: Preprocessing 3
% 14.87/3.18 % (1814152)Time elapsed: 0.096 s
% 14.87/3.18 % (1814152)Peak memory usage: 96 MB
% 14.87/3.18 % (1814152)Instructions burned: 130 (million)
% 14.87/3.18 % (1814261)lrs+10_1_sil=32000:urr=on:br=off:random_seed=924107512:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 14.87/3.18 % (1814255)lrs+10_1_sil=8000:sp=occurrence:random_seed=1645728532:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 14.87/3.18 % (1814267)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4087407404:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 14.87/3.18 % (1814272)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=2958973380:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 14.87/3.18 % (1814261)Instruction limit reached!
% 19.11/3.89 % (1814261)------------------------------
% 19.11/3.89 % (1814261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.11/3.89 % (1814261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.11/3.89 % (1814261)CaDiCaL version: 2.1.3
% 19.11/3.89 % (1814261)Termination reason: Instruction limit
% 19.11/3.89 % (1814261)Termination phase: Saturation
% 19.11/3.89 % (1814261)Time elapsed: 0.085 s
% 19.11/3.89 % (1814261)Peak memory usage: 95 MB
% 19.11/3.89 % (1814261)Instructions burned: 157 (million)
% 19.11/3.89 % (1814255)Instruction limit reached!
% 19.11/3.89 % (1814255)------------------------------
% 19.11/3.89 % (1814255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.11/3.89 % (1814255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.11/3.89 % (1814255)CaDiCaL version: 2.1.3
% 19.11/3.89 % (1814255)Termination reason: Instruction limit
% 19.11/3.89 % (1814255)Termination phase: Saturation
% 19.11/3.89 % (1814255)Time elapsed: 0.190 s
% 19.11/3.89 % (1814255)Peak memory usage: 99 MB
% 19.11/3.89 % (1814255)Instructions burned: 285 (million)
% 19.11/3.89 % (1814272)Instruction limit reached!
% 19.11/3.89 % (1814272)------------------------------
% 19.11/3.89 % (1814272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.11/3.89 % (1814272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.11/3.89 % (1814272)CaDiCaL version: 2.1.3
% 19.11/3.89 % (1814272)Termination reason: Instruction limit
% 19.11/3.89 % (1814272)Termination phase: Preprocessing 3
% 19.11/3.89 % (1814272)Time elapsed: 0.155 s
% 19.11/3.89 % (1814272)Peak memory usage: 100 MB
% 19.11/3.89 % (1814272)Instructions burned: 248 (million)
% 19.11/3.89 % (1814267)Instruction limit reached!
% 19.11/3.89 % (1814267)------------------------------
% 19.11/3.89 % (1814267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.11/3.89 % (1814267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.11/3.89 % (1814267)CaDiCaL version: 2.1.3
% 19.11/3.89 % (1814267)Termination reason: Instruction limit
% 19.11/3.89 % (1814267)Termination phase: Saturation
% 19.11/3.89 % (1814267)Time elapsed: 0.209 s
% 19.11/3.89 % (1814267)Peak memory usage: 98 MB
% 19.11/3.89 % (1814267)Instructions burned: 326 (million)
% 19.11/3.89 % (1814369)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3717628955:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 19.11/3.89 % (1814419)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3365128300:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 19.11/3.89 % (1814369)Instruction limit reached!
% 19.11/3.89 % (1814369)------------------------------
% 19.11/3.89 % (1814369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.11/3.89 % (1814369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.11/3.89 % (1814369)CaDiCaL version: 2.1.3
% 19.11/3.89 % (1814369)Termination reason: Instruction limit
% 19.11/3.89 % (1814369)Termination phase: Saturation
% 19.11/3.89 % (1814369)Time elapsed: 0.108 s
% 19.11/3.89 % (1814369)Peak memory usage: 99 MB
% 19.11/3.89 % (1814369)Instructions burned: 297 (million)
% 19.11/3.89 % (1814421)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=377908375:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 19.11/3.89 % (1814434)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2957465378:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 19.11/3.89 % (1814421)Instruction limit reached!
% 19.11/3.89 % (1814421)------------------------------
% 19.11/3.89 % (1814421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.11/3.89 % (1814421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.11/3.89 % (1814421)CaDiCaL version: 2.1.3
% 19.11/3.89 % (1814421)Termination reason: Instruction limit
% 19.11/3.89 % (1814421)Termination phase: Property scanning
% 19.11/3.89 % (1814421)Time elapsed: 0.083 s
% 19.11/3.89 % (1814421)Peak memory usage: 95 MB
% 19.11/3.89 % (1814421)Instructions burned: 114 (million)
% 19.11/3.89 % (1814434)Instruction limit reached!
% 19.11/3.89 % (1814434)------------------------------
% 19.11/3.89 % (1814434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.11/3.89 % (1814434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.11/3.89 % (1814434)CaDiCaL version: 2.1.3
% 19.11/3.89 % (1814434)Termination reason: Instruction limit
% 26.59/4.87 % (1814434)Termination phase: Preprocessing 3
% 26.59/4.87 % (1814434)Time elapsed: 0.093 s
% 26.59/4.87 % (1814434)Peak memory usage: 99 MB
% 26.59/4.87 % (1814434)Instructions burned: 127 (million)
% 26.59/4.87 % (1814493)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1988540032:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 26.59/4.87 % (1814493)Instruction limit reached!
% 26.59/4.87 % (1814493)------------------------------
% 26.59/4.87 % (1814493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1814493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1814493)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1814493)Termination reason: Instruction limit
% 26.59/4.87 % (1814493)Termination phase: Property scanning
% 26.59/4.87 % (1814493)Time elapsed: 0.029 s
% 26.59/4.87 % (1814493)Peak memory usage: 91 MB
% 26.59/4.87 % (1814493)Instructions burned: 119 (million)
% 26.59/4.87 % (1814539)lrs+10_1_sil=8000:sp=occurrence:random_seed=3628738596:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 26.59/4.87 % (1814570)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1646918794:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 26.59/4.87 % (1814557)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2276522187:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 26.59/4.87 % (1814557)Instruction limit reached!
% 26.59/4.87 % (1814557)------------------------------
% 26.59/4.87 % (1814557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1814557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1814557)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1814557)Termination reason: Instruction limit
% 26.59/4.87 % (1814557)Termination phase: Saturation
% 26.59/4.87 % (1814557)Time elapsed: 0.252 s
% 26.59/4.87 % (1814557)Peak memory usage: 98 MB
% 26.59/4.87 % (1814557)Instructions burned: 439 (million)
% 26.59/4.87 % (1814744)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2683603812:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 26.59/4.87 % (1814744)Instruction limit reached!
% 26.59/4.87 % (1814744)------------------------------
% 26.59/4.87 % (1814744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1814744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1814744)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1814744)Termination reason: Instruction limit
% 26.59/4.87 % (1814744)Termination phase: Saturation
% 26.59/4.87 % (1814744)Time elapsed: 0.088 s
% 26.59/4.87 % (1814744)Peak memory usage: 97 MB
% 26.59/4.87 % (1814744)Instructions burned: 135 (million)
% 26.59/4.87 % (1814539)Instruction limit reached!
% 26.59/4.87 % (1814539)------------------------------
% 26.59/4.87 % (1814539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1814539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1814539)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1814539)Termination reason: Instruction limit
% 26.59/4.87 % (1814539)Termination phase: Saturation
% 26.59/4.87 % (1814539)Time elapsed: 0.596 s
% 26.59/4.87 % (1814539)Peak memory usage: 109 MB
% 26.59/4.87 % (1814539)Instructions burned: 907 (million)
% 26.59/4.87 % (1814854)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4115374151:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 26.59/4.87 % (1814888)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=106197487:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 26.59/4.87 % (1814854)Instruction limit reached!
% 26.59/4.87 % (1814854)------------------------------
% 26.59/4.87 % (1814854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1814854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1814854)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1814854)Termination reason: Instruction limit
% 26.59/4.87 % (1814854)Termination phase: Saturation
% 26.59/4.87 % (1814854)Time elapsed: 0.297 s
% 26.59/4.87 % (1814854)Peak memory usage: 104 MB
% 26.59/4.87 % (1814854)Instructions burned: 594 (million)
% 26.59/4.87 % (1815061)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=49272411:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 26.59/4.87 % (1815061)Instruction limit reached!
% 26.59/4.87 % (1815061)------------------------------
% 26.59/4.87 % (1815061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1815061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1815061)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1815061)Termination reason: Instruction limit
% 26.59/4.87 % (1815061)Termination phase: Preprocessing 3
% 26.59/4.87 % (1815061)Time elapsed: 0.076 s
% 26.59/4.87 % (1815061)Peak memory usage: 93 MB
% 26.59/4.87 % (1815061)Instructions burned: 125 (million)
% 26.59/4.87 % (1814419)Instruction limit reached!
% 26.59/4.87 % (1814419)------------------------------
% 26.59/4.87 % (1814419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1814419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1814419)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1814419)Termination reason: Instruction limit
% 26.59/4.87 % (1814419)Termination phase: Saturation
% 26.59/4.87 % (1814419)Time elapsed: 1.482 s
% 26.59/4.87 % (1814419)Peak memory usage: 211 MB
% 26.59/4.87 % (1814419)Instructions burned: 2351 (million)
% 26.59/4.87 % (1815165)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=908479808:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 26.59/4.87 % (1815186)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3064825259:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/141Mi)
% 26.59/4.87 % (1815165)Instruction limit reached!
% 26.59/4.87 % (1815165)------------------------------
% 26.59/4.87 % (1815165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1815165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1815165)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1815165)Termination reason: Instruction limit
% 26.59/4.87 % (1815165)Termination phase: Property scanning
% 26.59/4.87 % (1815165)Time elapsed: 0.059 s
% 26.59/4.87 % (1815165)Peak memory usage: 91 MB
% 26.59/4.87 % (1815165)Instructions burned: 135 (million)
% 26.59/4.87 % (1815186)Instruction limit reached!
% 26.59/4.87 % (1815186)------------------------------
% 26.59/4.87 % (1815186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1815186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1815186)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1815186)Termination reason: Instruction limit
% 26.59/4.87 % (1815186)Termination phase: Saturation
% 26.59/4.87 % (1815186)Time elapsed: 0.085 s
% 26.59/4.87 % (1815186)Peak memory usage: 96 MB
% 26.59/4.87 % (1815186)Instructions burned: 142 (million)
% 26.59/4.87 % (1815267)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3581805861:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 26.59/4.87 % (1815301)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=2393619665:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 26.59/4.87 % (1814570)Instruction limit reached!
% 26.59/4.87 % (1814570)------------------------------
% 26.59/4.87 % (1814570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1814570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1814570)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1814570)Termination reason: Instruction limit
% 26.59/4.87 % (1814570)Termination phase: Saturation
% 26.59/4.87 % (1814570)Time elapsed: 1.687 s
% 26.59/4.87 % (1814570)Peak memory usage: 168 MB
% 26.59/4.87 % (1814570)Instructions burned: 5205 (million)
% 26.59/4.87 % (1815267)Instruction limit reached!
% 26.59/4.87 % (1815267)------------------------------
% 26.59/4.87 % (1815267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1815267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1815267)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1815267)Termination reason: Instruction limit
% 26.59/4.87 % (1815267)Termination phase: Saturation
% 26.59/4.87 % (1815267)Time elapsed: 0.258 s
% 26.59/4.87 % (1815267)Peak memory usage: 102 MB
% 26.59/4.87 % (1815267)Instructions burned: 433 (million)
% 26.59/4.87 % (1815410)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=1550071980:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 26.59/4.87 % (1815410)Instruction limit reached!
% 26.59/4.87 % (1815410)------------------------------
% 26.59/4.87 % (1815410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1815410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1815410)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1815410)Termination reason: Instruction limit
% 26.59/4.87 % (1815410)Termination phase: Preprocessing 3
% 26.59/4.87 % (1815410)Time elapsed: 0.062 s
% 26.59/4.87 % (1815410)Peak memory usage: 99 MB
% 26.59/4.87 % (1815410)Instructions burned: 152 (million)
% 26.59/4.87 % (1815456)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3913812748:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi)
% 26.59/4.87 % (1815492)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2051850609:i=667:av=off:fsr=off_2969 on theBenchmark for (2969ds/667Mi)
% 26.59/4.87 % (1815492)Instruction limit reached!
% 26.59/4.87 % (1815492)------------------------------
% 26.59/4.87 % (1815492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1815492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1815492)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1815492)Termination reason: Instruction limit
% 26.59/4.87 % (1815492)Termination phase: Saturation
% 26.59/4.87 % (1815492)Time elapsed: 0.183 s
% 26.59/4.87 % (1815492)Peak memory usage: 107 MB
% 26.59/4.87 % (1815492)Instructions burned: 669 (million)
% 26.59/4.87 % (1815628)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=2272134790:s2a=on:i=185:s2at=1.8:fdi=4_2966 on theBenchmark for (2966ds/185Mi)
% 26.59/4.87 % (1815628)Instruction limit reached!
% 26.59/4.87 % (1815628)------------------------------
% 26.59/4.87 % (1815628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1815628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1815628)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1815628)Termination reason: Instruction limit
% 26.59/4.87 % (1815628)Termination phase: NewCNF
% 26.59/4.87 % (1815628)Time elapsed: 0.071 s
% 26.59/4.87 % (1815628)Peak memory usage: 101 MB
% 26.59/4.87 % (1815628)Instructions burned: 186 (million)
% 26.59/4.87 % (1814888)First to succeed.
% 26.59/4.87 % (1814888)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1813819"
% 26.59/4.87 % (1815713)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3349683960:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2964 on theBenchmark for (2964ds/193Mi)
% 26.59/4.87 % (1815713)Instruction limit reached!
% 26.59/4.87 % (1815713)------------------------------
% 26.59/4.87 % (1815713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.59/4.87 % (1815713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.59/4.87 % (1815713)CaDiCaL version: 2.1.3
% 26.59/4.87 % (1815713)Termination reason: Instruction limit
% 26.59/4.87 % (1815713)Termination phase: Saturation
% 26.59/4.87 % (1815713)Time elapsed: 0.067 s
% 26.59/4.87 % (1815713)Peak memory usage: 99 MB
% 26.59/4.87 % (1815713)Instructions burned: 194 (million)
% 26.59/4.87 % (1815797)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=380945120:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2962 on theBenchmark for (2962ds/4850Mi)
% 26.59/4.87 % (1814888)Refutation found. Thanks to Tanya!
% 26.59/4.87 % SZS status Theorem for theBenchmark
% 26.59/4.87 % SZS output start Proof for theBenchmark
% See solution above
% 27.34/5.55 % (1814888)------------------------------
% 27.34/5.55 % (1814888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.34/5.55 % (1814888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.34/5.55 % (1814888)CaDiCaL version: 2.1.3
% 27.34/5.55 % (1814888)Termination reason: Refutation
% 27.34/5.55 % (1814888)Time elapsed: 1.716 s
% 27.34/5.55 % (1814888)Peak memory usage: 195 MB
% 27.34/5.55 % (1814888)Instructions burned: 2871 (million)
% 27.34/5.55 % (1814888)------------------------------
% 27.34/5.55 % (1814888)------------------------------
% 27.34/5.55 % (1813819)Success in time 4.006 s
% 27.34/5.55 % Vampire exiting
%------------------------------------------------------------------------------