%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP638+3 : 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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:12 AM UTC 2026
% Result : Theorem 30.99s 5.87s
% Output : Refutation 31.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 15
% Syntax : Number of formulae : 140 ( 35 unt; 5 def)
% Number of atoms : 556 ( 27 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 687 ( 271 ~; 266 |; 108 &)
% ( 12 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 6 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(f888,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k10_relat_1(X2,X0),k10_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t178_relat_1) ).
fof(f1333,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(f1392,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(f1394,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(f2007,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& m1_relset_1(X2,X0,X1) )
=> k3_funct_2(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k3_funct_2) ).
fof(f8746,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(f8768,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(f8898,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(f11207,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(f13974,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,X1)
=> ! [X4] :
( m1_group_2(X4,X1)
=> ! [X5] :
( m1_group_2(X5,X0)
=> ! [X6] :
( m1_group_2(X6,X0)
=> ( ( u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X1,X4) )
=> m1_group_6(X5,X0,X6) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_latsubgr) ).
fof(f13975,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,X1)
=> ! [X4] :
( m1_group_2(X4,X1)
=> ! [X5] :
( m1_group_2(X5,X0)
=> ! [X6] :
( m1_group_2(X6,X0)
=> ( ( u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X1,X4) )
=> m1_group_6(X5,X0,X6) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13974]) ).
fof(f14149,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ~ m1_group_6(X5,X0,X6)
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X1,X4)
& m1_group_2(X6,X0) )
& m1_group_2(X5,X0) )
& m1_group_2(X4,X1) )
& m1_group_2(X3,X1) )
& 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,[],[f13975]) ).
fof(f14150,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ~ m1_group_6(X5,X0,X6)
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X1,X4)
& m1_group_2(X6,X0) )
& m1_group_2(X5,X0) )
& m1_group_2(X4,X1) )
& m1_group_2(X3,X1) )
& 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,[],[f14149]) ).
fof(f14187,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,[],[f1392]) ).
fof(f14235,plain,
! [X0,X1,X2,X3] :
( k3_funct_2(X0,X1,X2,X3) = k10_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f2007]) ).
fof(f14236,plain,
! [X0,X1,X2,X3] :
( k3_funct_2(X0,X1,X2,X3) = k10_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f14235]) ).
fof(f14257,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,[],[f8898]) ).
fof(f14258,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,[],[f14257]) ).
fof(f14259,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,[],[f8768]) ).
fof(f14260,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,[],[f14259]) ).
fof(f14311,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,[],[f11207]) ).
fof(f14312,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,[],[f14311]) ).
fof(f14429,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1333]) ).
fof(f15074,plain,
! [X0,X1,X2] :
( r1_tarski(k10_relat_1(X2,X0),k10_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f888]) ).
fof(f15075,plain,
! [X0,X1,X2] :
( r1_tarski(k10_relat_1(X2,X0),k10_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f15074]) ).
fof(f15780,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,[],[f8746]) ).
fof(f15781,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,[],[f15780]) ).
fof(f20614,plain,
( ~ m1_group_6(sK153,sK148,sK154)
& u1_struct_0(sK153) = k3_funct_2(u1_struct_0(sK148),u1_struct_0(sK149),sK150,u1_struct_0(sK151))
& u1_struct_0(sK154) = k3_funct_2(u1_struct_0(sK148),u1_struct_0(sK149),sK150,u1_struct_0(sK152))
& m1_group_6(sK151,sK149,sK152)
& m1_group_2(sK154,sK148)
& m1_group_2(sK153,sK148)
& m1_group_2(sK152,sK149)
& m1_group_2(sK151,sK149)
& v1_funct_1(sK150)
& v1_funct_2(sK150,u1_struct_0(sK148),u1_struct_0(sK149))
& v1_group_6(sK150,sK148,sK149)
& m2_relset_1(sK150,u1_struct_0(sK148),u1_struct_0(sK149))
& ~ v3_struct_0(sK149)
& v3_group_1(sK149)
& v4_group_1(sK149)
& l1_group_1(sK149)
& ~ v3_struct_0(sK148)
& v3_group_1(sK148)
& v4_group_1(sK148)
& l1_group_1(sK148) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK148,sK149,sK150,sK151,sK152,sK153,sK154]),skolemize(X0,sK148),skolemize(X1,sK149),skolemize(X2,sK150),skolemize(X3,sK151),skolemize(X4,sK152),skolemize(X5,sK153),skolemize(X6,sK154)],[f14150]) ).
fof(f20638,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,[],[f14312]) ).
fof(f20934,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,[],[f1394]) ).
fof(f21146,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,[],[f15781]) ).
fof(f21147,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,[],[f21146]) ).
fof(f22668,plain,
l1_group_1(sK148),
inference(cnf_transformation,[],[f20614]) ).
fof(f22669,plain,
v4_group_1(sK148),
inference(cnf_transformation,[],[f20614]) ).
fof(f22670,plain,
v3_group_1(sK148),
inference(cnf_transformation,[],[f20614]) ).
fof(f22671,plain,
~ v3_struct_0(sK148),
inference(cnf_transformation,[],[f20614]) ).
fof(f22672,plain,
l1_group_1(sK149),
inference(cnf_transformation,[],[f20614]) ).
fof(f22673,plain,
v4_group_1(sK149),
inference(cnf_transformation,[],[f20614]) ).
fof(f22674,plain,
v3_group_1(sK149),
inference(cnf_transformation,[],[f20614]) ).
fof(f22675,plain,
~ v3_struct_0(sK149),
inference(cnf_transformation,[],[f20614]) ).
fof(f22676,plain,
m2_relset_1(sK150,u1_struct_0(sK148),u1_struct_0(sK149)),
inference(cnf_transformation,[],[f20614]) ).
fof(f22679,plain,
v1_funct_1(sK150),
inference(cnf_transformation,[],[f20614]) ).
fof(f22681,plain,
m1_group_2(sK152,sK149),
inference(cnf_transformation,[],[f20614]) ).
fof(f22682,plain,
m1_group_2(sK153,sK148),
inference(cnf_transformation,[],[f20614]) ).
fof(f22683,plain,
m1_group_2(sK154,sK148),
inference(cnf_transformation,[],[f20614]) ).
fof(f22684,plain,
m1_group_6(sK151,sK149,sK152),
inference(cnf_transformation,[],[f20614]) ).
fof(f22685,plain,
u1_struct_0(sK154) = k3_funct_2(u1_struct_0(sK148),u1_struct_0(sK149),sK150,u1_struct_0(sK152)),
inference(cnf_transformation,[],[f20614]) ).
fof(f22686,plain,
u1_struct_0(sK153) = k3_funct_2(u1_struct_0(sK148),u1_struct_0(sK149),sK150,u1_struct_0(sK151)),
inference(cnf_transformation,[],[f20614]) ).
fof(f22687,plain,
~ m1_group_6(sK153,sK148,sK154),
inference(cnf_transformation,[],[f20614]) ).
fof(f22738,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,[],[f14187]) ).
fof(f22781,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| k10_relat_1(X2,X3) = k3_funct_2(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f14236]) ).
fof(f22801,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,[],[f14258]) ).
fof(f22802,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,[],[f14258]) ).
fof(f22803,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,[],[f14258]) ).
fof(f22804,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,[],[f14260]) ).
fof(f22853,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,[],[f20638]) ).
fof(f22854,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,[],[f20638]) ).
fof(f23024,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f14429]) ).
fof(f23929,plain,
! [X2,X0,X1] :
( r1_tarski(k10_relat_1(X2,X0),k10_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f15075]) ).
fof(f23974,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20934]) ).
fof(f24798,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,[],[f21147]) ).
fof(f34441,plain,
( ~ m1_group_2(sK153,sK154)
| v3_struct_0(sK148)
| ~ v3_group_1(sK148)
| ~ v4_group_1(sK148)
| ~ l1_group_1(sK148)
| ~ m1_group_2(sK154,sK148) ),
inference(resolution,[],[f22687,f22854]) ).
fof(f34443,plain,
( m1_group_2(sK151,sK152)
| v3_struct_0(sK149)
| ~ v3_group_1(sK149)
| ~ v4_group_1(sK149)
| ~ l1_group_1(sK149)
| ~ m1_group_2(sK152,sK149) ),
inference(resolution,[],[f22853,f22684]) ).
fof(f34445,plain,
( ~ v3_struct_0(sK152)
| v3_struct_0(sK149)
| ~ v3_group_1(sK149)
| ~ l1_group_1(sK149) ),
inference(resolution,[],[f22681,f22803]) ).
fof(f34456,plain,
( v3_group_1(sK152)
| v3_struct_0(sK149)
| ~ v3_group_1(sK149)
| ~ l1_group_1(sK149) ),
inference(resolution,[],[f22802,f22681]) ).
fof(f34467,definition,
( spl1284_47
<=> m1_relset_1(sK150,u1_struct_0(sK148),u1_struct_0(sK149)) ),
introduced(definition,[new_symbols(definition,[spl1284_47])],[avatar_definition]) ).
fof(f34468,plain,
( m1_relset_1(sK150,u1_struct_0(sK148),u1_struct_0(sK149))
| ~ spl1284_47 ),
inference(avatar_component_clause,[],[f34467]) ).
fof(f34469,plain,
( ~ m1_relset_1(sK150,u1_struct_0(sK148),u1_struct_0(sK149))
| spl1284_47 ),
inference(avatar_component_clause,[],[f34467]) ).
fof(f34485,plain,
( l1_group_1(sK152)
| v3_struct_0(sK149)
| ~ v3_group_1(sK149)
| ~ l1_group_1(sK149) ),
inference(resolution,[],[f22801,f22681]) ).
fof(f34487,plain,
m1_relset_1(sK150,u1_struct_0(sK148),u1_struct_0(sK149)),
inference(resolution,[],[f23974,f22676]) ).
fof(f34488,plain,
( $false
| spl1284_47 ),
inference(forward_subsumption_resolution,[],[f34487,f34469]) ).
fof(f34489,plain,
spl1284_47,
inference(avatar_contradiction_clause,[],[f34488]) ).
fof(f34494,plain,
( ! [X0] :
( ~ v1_funct_1(sK150)
| k10_relat_1(sK150,X0) = k3_funct_2(u1_struct_0(sK148),u1_struct_0(sK149),sK150,X0) )
| ~ spl1284_47 ),
inference(resolution,[],[f34468,f22781]) ).
fof(f34495,plain,
( ! [X0] : k10_relat_1(sK150,X0) = k3_funct_2(u1_struct_0(sK148),u1_struct_0(sK149),sK150,X0)
| ~ spl1284_47 ),
inference(forward_subsumption_resolution,[],[f34494,f22679]) ).
fof(f34517,plain,
( u1_struct_0(sK154) = k10_relat_1(sK150,u1_struct_0(sK152))
| ~ spl1284_47 ),
inference(superposition,[],[f22685,f34495]) ).
fof(f34518,plain,
( u1_struct_0(sK153) = k10_relat_1(sK150,u1_struct_0(sK151))
| ~ spl1284_47 ),
inference(superposition,[],[f22686,f34495]) ).
fof(f34949,plain,
( ! [X0] :
( r1_tarski(k10_relat_1(sK150,X0),u1_struct_0(sK154))
| ~ r1_tarski(X0,u1_struct_0(sK152))
| ~ v1_relat_1(sK150) )
| ~ spl1284_47 ),
inference(superposition,[],[f23929,f34517]) ).
fof(f34951,definition,
( spl1284_50
<=> v1_relat_1(sK150) ),
introduced(definition,[new_symbols(definition,[spl1284_50])],[avatar_definition]) ).
fof(f34953,plain,
( ~ v1_relat_1(sK150)
| spl1284_50 ),
inference(avatar_component_clause,[],[f34951]) ).
fof(f34955,definition,
( spl1284_51
<=> ! [X0] :
( r1_tarski(k10_relat_1(sK150,X0),u1_struct_0(sK154))
| ~ r1_tarski(X0,u1_struct_0(sK152)) ) ),
introduced(definition,[new_symbols(definition,[spl1284_51])],[avatar_definition]) ).
fof(f34956,plain,
( ! [X0] :
( r1_tarski(k10_relat_1(sK150,X0),u1_struct_0(sK154))
| ~ r1_tarski(X0,u1_struct_0(sK152)) )
| ~ spl1284_51 ),
inference(avatar_component_clause,[],[f34955]) ).
fof(f34957,plain,
( ~ spl1284_50
| spl1284_51
| ~ spl1284_47 ),
inference(avatar_split_clause,[],[f34949,f34467,f34955,f34951]) ).
fof(f35388,plain,
( ~ v3_struct_0(sK152)
| ~ v3_group_1(sK149)
| ~ l1_group_1(sK149) ),
inference(forward_subsumption_resolution,[],[f34445,f22675]) ).
fof(f35391,plain,
( v3_group_1(sK152)
| ~ v3_group_1(sK149)
| ~ l1_group_1(sK149) ),
inference(forward_subsumption_resolution,[],[f34456,f22675]) ).
fof(f35395,plain,
( l1_group_1(sK152)
| ~ v3_group_1(sK149)
| ~ l1_group_1(sK149) ),
inference(forward_subsumption_resolution,[],[f34485,f22675]) ).
fof(f35420,plain,
( ~ v3_struct_0(sK152)
| ~ l1_group_1(sK149) ),
inference(forward_subsumption_resolution,[],[f35388,f22674]) ).
fof(f35423,plain,
( v3_group_1(sK152)
| ~ l1_group_1(sK149) ),
inference(forward_subsumption_resolution,[],[f35391,f22674]) ).
fof(f35427,plain,
( l1_group_1(sK152)
| ~ l1_group_1(sK149) ),
inference(forward_subsumption_resolution,[],[f35395,f22674]) ).
fof(f35448,plain,
~ v3_struct_0(sK152),
inference(forward_subsumption_resolution,[],[f35420,f22672]) ).
fof(f35451,plain,
v3_group_1(sK152),
inference(forward_subsumption_resolution,[],[f35423,f22672]) ).
fof(f35455,plain,
l1_group_1(sK152),
inference(forward_subsumption_resolution,[],[f35427,f22672]) ).
fof(f35507,plain,
( ~ m1_group_2(sK153,sK154)
| ~ v3_group_1(sK148)
| ~ v4_group_1(sK148)
| ~ l1_group_1(sK148)
| ~ m1_group_2(sK154,sK148) ),
inference(forward_subsumption_resolution,[],[f34441,f22671]) ).
fof(f35508,plain,
( m1_group_2(sK151,sK152)
| ~ v3_group_1(sK149)
| ~ v4_group_1(sK149)
| ~ l1_group_1(sK149)
| ~ m1_group_2(sK152,sK149) ),
inference(forward_subsumption_resolution,[],[f34443,f22675]) ).
fof(f35791,plain,
( ~ m1_group_2(sK153,sK154)
| ~ v4_group_1(sK148)
| ~ l1_group_1(sK148)
| ~ m1_group_2(sK154,sK148) ),
inference(forward_subsumption_resolution,[],[f35507,f22670]) ).
fof(f35792,plain,
( m1_group_2(sK151,sK152)
| ~ v4_group_1(sK149)
| ~ l1_group_1(sK149)
| ~ m1_group_2(sK152,sK149) ),
inference(forward_subsumption_resolution,[],[f35508,f22674]) ).
fof(f36005,plain,
( ~ m1_group_2(sK153,sK154)
| ~ l1_group_1(sK148)
| ~ m1_group_2(sK154,sK148) ),
inference(forward_subsumption_resolution,[],[f35791,f22669]) ).
fof(f36006,plain,
( m1_group_2(sK151,sK152)
| ~ l1_group_1(sK149)
| ~ m1_group_2(sK152,sK149) ),
inference(forward_subsumption_resolution,[],[f35792,f22673]) ).
fof(f36177,plain,
( ~ m1_group_2(sK153,sK154)
| ~ m1_group_2(sK154,sK148) ),
inference(forward_subsumption_resolution,[],[f36005,f22668]) ).
fof(f36178,plain,
( m1_group_2(sK151,sK152)
| ~ m1_group_2(sK152,sK149) ),
inference(forward_subsumption_resolution,[],[f36006,f22672]) ).
fof(f36342,plain,
~ m1_group_2(sK153,sK154),
inference(forward_subsumption_resolution,[],[f36177,f22683]) ).
fof(f36343,plain,
m1_group_2(sK151,sK152),
inference(forward_subsumption_resolution,[],[f36178,f22681]) ).
fof(f51888,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f23024,f22738]) ).
fof(f51891,plain,
v1_relat_1(sK150),
inference(resolution,[],[f51888,f22676]) ).
fof(f51895,plain,
( $false
| spl1284_50 ),
inference(forward_subsumption_resolution,[],[f51891,f34953]) ).
fof(f51896,plain,
spl1284_50,
inference(avatar_contradiction_clause,[],[f51895]) ).
fof(f51901,plain,
( r1_tarski(u1_struct_0(sK153),u1_struct_0(sK154))
| ~ r1_tarski(u1_struct_0(sK151),u1_struct_0(sK152))
| ~ spl1284_47
| ~ spl1284_51 ),
inference(superposition,[],[f34956,f34518]) ).
fof(f51906,definition,
( spl1284_1255
<=> r1_tarski(u1_struct_0(sK151),u1_struct_0(sK152)) ),
introduced(definition,[new_symbols(definition,[spl1284_1255])],[avatar_definition]) ).
fof(f51908,plain,
( ~ r1_tarski(u1_struct_0(sK151),u1_struct_0(sK152))
| spl1284_1255 ),
inference(avatar_component_clause,[],[f51906]) ).
fof(f51910,definition,
( spl1284_1256
<=> r1_tarski(u1_struct_0(sK153),u1_struct_0(sK154)) ),
introduced(definition,[new_symbols(definition,[spl1284_1256])],[avatar_definition]) ).
fof(f51912,plain,
( r1_tarski(u1_struct_0(sK153),u1_struct_0(sK154))
| ~ spl1284_1256 ),
inference(avatar_component_clause,[],[f51910]) ).
fof(f51913,plain,
( ~ spl1284_1255
| spl1284_1256
| ~ spl1284_47
| ~ spl1284_51 ),
inference(avatar_split_clause,[],[f51901,f34955,f34467,f51910,f51906]) ).
fof(f51914,plain,
( ~ m1_group_2(sK151,sK152)
| v3_struct_0(sK151)
| ~ v3_group_1(sK151)
| ~ l1_group_1(sK151)
| v3_struct_0(sK152)
| ~ v3_group_1(sK152)
| ~ l1_group_1(sK152)
| spl1284_1255 ),
inference(resolution,[],[f51908,f24798]) ).
fof(f51915,plain,
( ~ m1_group_2(sK151,sK152)
| ~ v3_group_1(sK151)
| ~ l1_group_1(sK151)
| v3_struct_0(sK152)
| ~ v3_group_1(sK152)
| ~ l1_group_1(sK152)
| spl1284_1255 ),
inference(forward_subsumption_resolution,[],[f51914,f22803]) ).
fof(f51916,plain,
( ~ m1_group_2(sK151,sK152)
| ~ l1_group_1(sK151)
| v3_struct_0(sK152)
| ~ v3_group_1(sK152)
| ~ l1_group_1(sK152)
| spl1284_1255 ),
inference(forward_subsumption_resolution,[],[f51915,f22802]) ).
fof(f51917,plain,
( ~ m1_group_2(sK151,sK152)
| v3_struct_0(sK152)
| ~ v3_group_1(sK152)
| ~ l1_group_1(sK152)
| spl1284_1255 ),
inference(forward_subsumption_resolution,[],[f51916,f22801]) ).
fof(f51918,plain,
( v3_struct_0(sK152)
| ~ v3_group_1(sK152)
| ~ l1_group_1(sK152)
| spl1284_1255 ),
inference(forward_subsumption_resolution,[],[f51917,f36343]) ).
fof(f51919,plain,
( ~ v3_group_1(sK152)
| ~ l1_group_1(sK152)
| spl1284_1255 ),
inference(forward_subsumption_resolution,[],[f51918,f35448]) ).
fof(f51920,plain,
( ~ l1_group_1(sK152)
| spl1284_1255 ),
inference(forward_subsumption_resolution,[],[f51919,f35451]) ).
fof(f51921,plain,
( $false
| spl1284_1255 ),
inference(forward_subsumption_resolution,[],[f51920,f35455]) ).
fof(f51922,plain,
spl1284_1255,
inference(avatar_contradiction_clause,[],[f51921]) ).
fof(f51923,plain,
( ! [X0] :
( m1_group_2(sK153,sK154)
| ~ m1_group_2(sK154,X0)
| ~ m1_group_2(sK153,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl1284_1256 ),
inference(resolution,[],[f51912,f22804]) ).
fof(f51936,plain,
( ! [X0] :
( ~ m1_group_2(sK154,X0)
| ~ m1_group_2(sK153,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl1284_1256 ),
inference(forward_subsumption_resolution,[],[f51923,f36342]) ).
fof(f51943,plain,
( ~ m1_group_2(sK153,sK148)
| v3_struct_0(sK148)
| ~ v3_group_1(sK148)
| ~ v4_group_1(sK148)
| ~ l1_group_1(sK148)
| ~ spl1284_1256 ),
inference(resolution,[],[f51936,f22683]) ).
fof(f51946,plain,
( v3_struct_0(sK148)
| ~ v3_group_1(sK148)
| ~ v4_group_1(sK148)
| ~ l1_group_1(sK148)
| ~ spl1284_1256 ),
inference(forward_subsumption_resolution,[],[f51943,f22682]) ).
fof(f51951,plain,
( ~ v3_group_1(sK148)
| ~ v4_group_1(sK148)
| ~ l1_group_1(sK148)
| ~ spl1284_1256 ),
inference(forward_subsumption_resolution,[],[f51946,f22671]) ).
fof(f51956,plain,
( ~ v4_group_1(sK148)
| ~ l1_group_1(sK148)
| ~ spl1284_1256 ),
inference(forward_subsumption_resolution,[],[f51951,f22670]) ).
fof(f51961,plain,
( ~ l1_group_1(sK148)
| ~ spl1284_1256 ),
inference(forward_subsumption_resolution,[],[f51956,f22669]) ).
fof(f51966,plain,
( $false
| ~ spl1284_1256 ),
inference(forward_subsumption_resolution,[],[f51961,f22668]) ).
fof(f51967,plain,
~ spl1284_1256,
inference(avatar_contradiction_clause,[],[f51966]) ).
cnf(s46,plain,
spl1284_47,
inference(sat_conversion,[],[f34489]) ).
cnf(s47,plain,
( ~ spl1284_47
| ~ spl1284_50
| spl1284_51 ),
inference(sat_conversion,[],[f34957]) ).
cnf(s1103,plain,
spl1284_50,
inference(sat_conversion,[],[f51896]) ).
cnf(s1104,plain,
( ~ spl1284_47
| ~ spl1284_51
| ~ spl1284_1255
| spl1284_1256 ),
inference(sat_conversion,[],[f51913]) ).
cnf(s1105,plain,
spl1284_1255,
inference(sat_conversion,[],[f51922]) ).
cnf(s1107,plain,
~ spl1284_1256,
inference(sat_conversion,[],[f51967]) ).
cnf(s1108,plain,
( ~ spl1284_47
| ~ spl1284_51 ),
inference(rat,[],[s1104,s1107,s1105]) ).
cnf(s1692,plain,
( ~ spl1284_47
| spl1284_51 ),
inference(rat,[],[s47,s1103]) ).
cnf(s1693,plain,
~ spl1284_51,
inference(rat,[],[s1108,s46]) ).
cnf(s1955,plain,
$false,
inference(rat,[],[s1692,s1693,s46]) ).
fof(f51970,plain,
$false,
inference(avatar_sat_refutation,[],[s1955]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP638+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n005.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 10:20:34 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 14.05/3.40 % (3780230)Detected formulas, will run a generic FOF schedule.
% 14.05/3.40 % (3780238)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=367897286:i=109:sd=1:ins=1:gsp=on:ss=axioms_2992 on theBenchmark for (2992ds/109Mi)
% 14.05/3.40 % (3780236)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=3692326478:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2992 on theBenchmark for (2992ds/134677Mi)
% 14.05/3.40 % (3780237)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=35262514:i=141695:sd=1:nm=32:gsp=on:ss=included_2992 on theBenchmark for (2992ds/141695Mi)
% 14.05/3.40 % (3780235)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=1805637790:i=141193_2992 on theBenchmark for (2992ds/141193Mi)
% 14.05/3.40 % (3780240)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1853877048:s2a=on:i=139:gtg=position_2992 on theBenchmark for (2992ds/139Mi)
% 14.05/3.40 % (3780239)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2672134373:i=119:av=off:ss=axioms_2992 on theBenchmark for (2992ds/119Mi)
% 14.05/3.40 % (3780241)dis-21_1_sil=8000:lcm=predicate:random_seed=2019897068:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2992 on theBenchmark for (2992ds/129Mi)
% 14.05/3.40 % (3780238)Instruction limit reached!
% 14.05/3.40 % (3780238)------------------------------
% 14.05/3.40 % (3780238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.05/3.40 % (3780238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.05/3.40 % (3780238)CaDiCaL version: 2.1.3
% 14.05/3.40 % (3780238)Termination reason: Instruction limit
% 14.05/3.40 % (3780238)Termination phase: Saturation
% 14.05/3.40 % (3780238)Time elapsed: 0.052 s
% 14.05/3.40 % (3780238)Peak memory usage: 107 MB
% 14.05/3.40 % (3780238)Instructions burned: 111 (million)
% 14.05/3.40 % (3780240)Instruction limit reached!
% 14.05/3.40 % (3780240)------------------------------
% 14.05/3.40 % (3780240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.05/3.40 % (3780240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.05/3.40 % (3780240)CaDiCaL version: 2.1.3
% 14.05/3.40 % (3780240)Termination reason: Instruction limit
% 14.05/3.40 % (3780240)Termination phase: Property scanning
% 14.05/3.40 % (3780240)Time elapsed: 0.060 s
% 14.05/3.40 % (3780240)Peak memory usage: 103 MB
% 14.05/3.40 % (3780240)Instructions burned: 141 (million)
% 14.05/3.40 % (3780249)lrs+10_1_sil=8000:sp=occurrence:random_seed=3491811158:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 14.05/3.40 % (3780241)Instruction limit reached!
% 14.05/3.40 % (3780241)------------------------------
% 14.05/3.40 % (3780241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.05/3.40 % (3780241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.05/3.40 % (3780241)CaDiCaL version: 2.1.3
% 14.05/3.40 % (3780241)Termination reason: Instruction limit
% 14.05/3.40 % (3780241)Termination phase: Preprocessing 1
% 14.05/3.40 % (3780241)Time elapsed: 0.099 s
% 14.05/3.40 % (3780241)Peak memory usage: 104 MB
% 14.05/3.40 % (3780241)Instructions burned: 129 (million)
% 14.05/3.40 % (3780239)Instruction limit reached!
% 14.05/3.40 % (3780239)------------------------------
% 14.05/3.40 % (3780239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.05/3.40 % (3780239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.05/3.40 % (3780239)CaDiCaL version: 2.1.3
% 14.05/3.40 % (3780239)Termination reason: Instruction limit
% 14.05/3.40 % (3780239)Termination phase: Naming
% 14.05/3.40 % (3780239)Time elapsed: 0.101 s
% 14.05/3.40 % (3780239)Peak memory usage: 106 MB
% 14.05/3.40 % (3780239)Instructions burned: 119 (million)
% 14.05/3.40 % (3780250)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1984402330:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 14.05/3.40 % (3780249)Instruction limit reached!
% 14.05/3.40 % (3780249)------------------------------
% 14.05/3.40 % (3780249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.05/3.40 % (3780249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.05/3.40 % (3780249)CaDiCaL version: 2.1.3
% 14.05/3.40 % (3780249)Termination reason: Instruction limit
% 20.32/4.30 % (3780249)Termination phase: Saturation
% 20.32/4.30 % (3780249)Time elapsed: 0.110 s
% 20.32/4.30 % (3780249)Peak memory usage: 111 MB
% 20.32/4.30 % (3780249)Instructions burned: 288 (million)
% 20.32/4.30 % (3780253)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=542530309:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 20.32/4.30 % (3780252)lrs+1011_1_sil=32000:sp=occurrence:random_seed=219764903:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 20.32/4.30 % (3780250)Instruction limit reached!
% 20.32/4.30 % (3780250)------------------------------
% 20.32/4.30 % (3780250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/4.30 % (3780250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/4.30 % (3780250)CaDiCaL version: 2.1.3
% 20.32/4.30 % (3780250)Termination reason: Instruction limit
% 20.32/4.30 % (3780250)Termination phase: Property scanning
% 20.32/4.30 % (3780250)Time elapsed: 0.068 s
% 20.32/4.30 % (3780250)Peak memory usage: 103 MB
% 20.32/4.30 % (3780250)Instructions burned: 158 (million)
% 20.32/4.30 % (3780255)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3447248204:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 20.32/4.30 % (3780253)Instruction limit reached!
% 20.32/4.30 % (3780253)------------------------------
% 20.32/4.30 % (3780253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/4.30 % (3780253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/4.30 % (3780253)CaDiCaL version: 2.1.3
% 20.32/4.30 % (3780253)Termination reason: Instruction limit
% 20.32/4.30 % (3780253)Termination phase: SInE selection
% 20.32/4.30 % (3780253)Time elapsed: 0.132 s
% 20.32/4.30 % (3780253)Peak memory usage: 103 MB
% 20.32/4.30 % (3780253)Instructions burned: 248 (million)
% 20.32/4.30 % (3780258)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=238006905:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 20.32/4.30 % (3780255)Instruction limit reached!
% 20.32/4.30 % (3780255)------------------------------
% 20.32/4.30 % (3780255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/4.30 % (3780255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/4.30 % (3780255)CaDiCaL version: 2.1.3
% 20.32/4.30 % (3780255)Termination reason: Instruction limit
% 20.32/4.30 % (3780255)Termination phase: Saturation
% 20.32/4.30 % (3780255)Time elapsed: 0.106 s
% 20.32/4.30 % (3780255)Peak memory usage: 111 MB
% 20.32/4.30 % (3780255)Instructions burned: 297 (million)
% 20.32/4.30 % (3780252)Instruction limit reached!
% 20.32/4.30 % (3780252)------------------------------
% 20.32/4.30 % (3780252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/4.30 % (3780252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/4.30 % (3780252)CaDiCaL version: 2.1.3
% 20.32/4.30 % (3780252)Termination reason: Instruction limit
% 20.32/4.30 % (3780252)Termination phase: Saturation
% 20.32/4.30 % (3780252)Time elapsed: 0.225 s
% 20.32/4.30 % (3780252)Peak memory usage: 110 MB
% 20.32/4.30 % (3780252)Instructions burned: 326 (million)
% 20.32/4.30 % (3780262)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2999817301:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 20.32/4.30 % (3780260)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1894239779:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 20.32/4.30 % (3780262)Instruction limit reached!
% 20.32/4.30 % (3780262)------------------------------
% 20.32/4.30 % (3780262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/4.30 % (3780262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/4.30 % (3780262)CaDiCaL version: 2.1.3
% 20.32/4.30 % (3780262)Termination reason: Instruction limit
% 20.32/4.30 % (3780262)Termination phase: Preprocessing 2
% 20.32/4.30 % (3780262)Time elapsed: 0.059 s
% 20.32/4.30 % (3780262)Peak memory usage: 106 MB
% 20.32/4.30 % (3780262)Instructions burned: 129 (million)
% 20.32/4.30 % (3780263)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=310838819:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 20.32/4.30 % (3780260)Instruction limit reached!
% 20.32/4.30 % (3780260)------------------------------
% 20.32/4.30 % (3780260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780260)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780260)Termination reason: Instruction limit
% 30.99/5.87 % (3780260)Termination phase: Preprocessing 2
% 30.99/5.87 % (3780260)Time elapsed: 0.100 s
% 30.99/5.87 % (3780260)Peak memory usage: 106 MB
% 30.99/5.87 % (3780260)Instructions burned: 113 (million)
% 30.99/5.87 % (3780263)Instruction limit reached!
% 30.99/5.87 % (3780263)------------------------------
% 30.99/5.87 % (3780263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780266)lrs+10_1_sil=8000:sp=occurrence:random_seed=997180257:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 30.99/5.87 % (3780263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780263)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780263)Termination reason: Instruction limit
% 30.99/5.87 % (3780263)Termination phase: Property scanning
% 30.99/5.87 % (3780263)Time elapsed: 0.050 s
% 30.99/5.87 % (3780263)Peak memory usage: 103 MB
% 30.99/5.87 % (3780263)Instructions burned: 116 (million)
% 30.99/5.87 % (3780268)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4160616098:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 30.99/5.87 % (3780270)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3378671461:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 30.99/5.87 % (3780266)Instruction limit reached!
% 30.99/5.87 % (3780266)------------------------------
% 30.99/5.87 % (3780266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780266)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780266)Termination reason: Instruction limit
% 30.99/5.87 % (3780266)Termination phase: Saturation
% 30.99/5.87 % (3780266)Time elapsed: 0.299 s
% 30.99/5.87 % (3780266)Peak memory usage: 122 MB
% 30.99/5.87 % (3780266)Instructions burned: 910 (million)
% 30.99/5.87 % (3780268)Instruction limit reached!
% 30.99/5.87 % (3780268)------------------------------
% 30.99/5.87 % (3780268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780268)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780268)Termination reason: Instruction limit
% 30.99/5.87 % (3780268)Termination phase: Saturation
% 30.99/5.87 % (3780268)Time elapsed: 0.268 s
% 30.99/5.87 % (3780268)Peak memory usage: 110 MB
% 30.99/5.87 % (3780268)Instructions burned: 438 (million)
% 30.99/5.87 % (3780273)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=82770681:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 30.99/5.87 % (3780273)Instruction limit reached!
% 30.99/5.87 % (3780273)------------------------------
% 30.99/5.87 % (3780273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780273)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780273)Termination reason: Instruction limit
% 30.99/5.87 % (3780273)Termination phase: Property scanning
% 30.99/5.87 % (3780273)Time elapsed: 0.060 s
% 30.99/5.87 % (3780273)Peak memory usage: 107 MB
% 30.99/5.87 % (3780273)Instructions burned: 138 (million)
% 30.99/5.87 % (3780274)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3759474980:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 30.99/5.87 % (3780276)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2650225638:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 30.99/5.87 % (3780274)Instruction limit reached!
% 30.99/5.87 % (3780274)------------------------------
% 30.99/5.87 % (3780274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780274)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780274)Termination reason: Instruction limit
% 30.99/5.87 % (3780274)Termination phase: Property scanning
% 30.99/5.87 % (3780274)Time elapsed: 0.412 s
% 30.99/5.87 % (3780274)Peak memory usage: 125 MB
% 30.99/5.87 % (3780274)Instructions burned: 592 (million)
% 30.99/5.87 % (3780279)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=3646347470:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/125Mi)
% 30.99/5.87 % (3780279)Instruction limit reached!
% 30.99/5.87 % (3780279)------------------------------
% 30.99/5.87 % (3780279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780279)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780279)Termination reason: Instruction limit
% 30.99/5.87 % (3780279)Termination phase: Property scanning
% 30.99/5.87 % (3780279)Time elapsed: 0.054 s
% 30.99/5.87 % (3780279)Peak memory usage: 103 MB
% 30.99/5.87 % (3780279)Instructions burned: 125 (million)
% 30.99/5.87 % (3780258)Instruction limit reached!
% 30.99/5.87 % (3780258)------------------------------
% 30.99/5.87 % (3780258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780258)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780258)Termination reason: Instruction limit
% 30.99/5.87 % (3780258)Termination phase: Saturation
% 30.99/5.87 % (3780258)Time elapsed: 1.448 s
% 30.99/5.87 % (3780258)Peak memory usage: 223 MB
% 30.99/5.87 % (3780258)Instructions burned: 2350 (million)
% 30.99/5.87 % (3780281)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2799326051:i=134:gtgl=5:slsql=off:gtg=exists_sym_2973 on theBenchmark for (2973ds/134Mi)
% 30.99/5.87 % (3780281)Instruction limit reached!
% 30.99/5.87 % (3780281)------------------------------
% 30.99/5.87 % (3780281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780281)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780281)Termination reason: Instruction limit
% 30.99/5.87 % (3780281)Termination phase: Property scanning
% 30.99/5.87 % (3780281)Time elapsed: 0.058 s
% 30.99/5.87 % (3780281)Peak memory usage: 103 MB
% 30.99/5.87 % (3780281)Instructions burned: 135 (million)
% 30.99/5.87 % (3780282)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1502491449:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 30.99/5.87 % (3780284)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=837302755:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2971 on theBenchmark for (2971ds/431Mi)
% 30.99/5.87 % (3780282)Instruction limit reached!
% 30.99/5.87 % (3780282)------------------------------
% 30.99/5.87 % (3780282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780282)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780282)Termination reason: Instruction limit
% 30.99/5.87 % (3780282)Termination phase: Saturation
% 30.99/5.87 % (3780282)Time elapsed: 0.107 s
% 30.99/5.87 % (3780282)Peak memory usage: 108 MB
% 30.99/5.87 % (3780282)Instructions burned: 141 (million)
% 30.99/5.87 % (3780287)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=3428067962:i=6060:aac=none:ins=25_2970 on theBenchmark for (2970ds/6060Mi)
% 30.99/5.87 % (3780284)Instruction limit reached!
% 30.99/5.87 % (3780284)------------------------------
% 30.99/5.87 % (3780284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780284)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780284)Termination reason: Instruction limit
% 30.99/5.87 % (3780284)Termination phase: Saturation
% 30.99/5.87 % (3780284)Time elapsed: 0.275 s
% 30.99/5.87 % (3780284)Peak memory usage: 113 MB
% 30.99/5.87 % (3780284)Instructions burned: 433 (million)
% 30.99/5.87 % (3780289)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=1603974292:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2967 on theBenchmark for (2967ds/150Mi)
% 30.99/5.87 % (3780289)Instruction limit reached!
% 30.99/5.87 % (3780289)------------------------------
% 30.99/5.87 % (3780289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780289)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780289)Termination reason: Instruction limit
% 30.99/5.87 % (3780289)Termination phase: Preprocessing 1
% 30.99/5.87 % (3780289)Time elapsed: 0.111 s
% 30.99/5.87 % (3780289)Peak memory usage: 104 MB
% 30.99/5.87 % (3780289)Instructions burned: 150 (million)
% 30.99/5.87 % (3780291)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2844488024:i=14155:bd=all_2965 on theBenchmark for (2965ds/14155Mi)
% 30.99/5.87 % (3780270)Instruction limit reached!
% 30.99/5.87 % (3780270)------------------------------
% 30.99/5.87 % (3780270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.87 % (3780270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.87 % (3780270)CaDiCaL version: 2.1.3
% 30.99/5.87 % (3780270)Termination reason: Instruction limit
% 30.99/5.87 % (3780270)Termination phase: Saturation
% 30.99/5.87 % (3780270)Time elapsed: 3.052 s
% 30.99/5.87 % (3780270)Peak memory usage: 224 MB
% 30.99/5.87 % (3780270)Instructions burned: 5202 (million)
% 30.99/5.87 % (3780276)First to succeed.
% 30.99/5.87 % (3780276)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3780230"
% 30.99/5.87 % (3780293)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1029788420:i=667:av=off:fsr=off_2953 on theBenchmark for (2953ds/667Mi)
% 30.99/5.87 % (3780276)Refutation found. Thanks to Tanya!
% 30.99/5.87 % SZS status Theorem for theBenchmark
% 30.99/5.87 % SZS output start Proof for theBenchmark
% See solution above
% 31.61/6.04 % (3780276)------------------------------
% 31.61/6.04 % (3780276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.61/6.04 % (3780276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.61/6.04 % (3780276)CaDiCaL version: 2.1.3
% 31.61/6.04 % (3780276)Termination reason: Refutation
% 31.61/6.04 % (3780276)Time elapsed: 2.760 s
% 31.61/6.04 % (3780276)Peak memory usage: 276 MB
% 31.61/6.04 % (3780276)Instructions burned: 8185 (million)
% 31.61/6.04 % (3780276)------------------------------
% 31.61/6.04 % (3780276)------------------------------
% 31.61/6.04 % (3780230)Success in time 5.025 s
% 31.61/6.04 % Vampire exiting
%------------------------------------------------------------------------------