%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP624+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:04 AM UTC 2026
% Result : Theorem 30.45s 10.20s
% Output : Refutation 47.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 20
% Syntax : Number of formulae : 166 ( 30 unt; 4 def)
% Number of atoms : 723 ( 65 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 958 ( 401 ~; 438 |; 81 &)
% ( 13 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 5 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 3 con; 0-6 aty)
% Number of variables : 247 ( 0 sgn 237 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f2436,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( ~ v1_xboole_0(X0)
& ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
& m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
& m1_subset_1(X4,X0)
& m1_subset_1(X5,X1) )
=> k2_binop_1(X0,X1,X2,X3,X4,X5) = k1_binop_1(X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_binop_1) ).
fof(f3367,axiom,
! [X0,X1,X2] :
( m1_fraenkel(X2,X0,X1)
=> ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_fraenkel) ).
fof(f3371,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_fraenkel) ).
fof(f18256,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f18620,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( r1_rlvect_1(X0,X1)
<=> r2_hidden(X1,u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_rlvect_1) ).
fof(f18989,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f18993,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_group_1) ).
fof(f21861,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> r1_rlvect_1(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t50_group_2) ).
fof(f21874,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_group_2(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_group_2) ).
fof(f33385,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_autgroup) ).
fof(f33386,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_funct_1(k2_autgroup(X0))
& v1_funct_2(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
& m2_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_autgroup) ).
fof(f33403,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
& m2_relset_1(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) )
=> ( X1 = k2_autgroup(X0)
<=> ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> ! [X3] :
( m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X2,X3) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X3,X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_autgroup) ).
fof(f33410,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_autgroup) ).
fof(f33412,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> k1_binop_1(k2_autgroup(X0),X1,X2) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_autgroup) ).
fof(f33413,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> k1_binop_1(k2_autgroup(X0),X1,X2) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f33412]) ).
fof(f33498,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33385]) ).
fof(f33499,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33498]) ).
fof(f33500,plain,
! [X0] :
( ( v1_funct_1(k2_autgroup(X0))
& v1_funct_2(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
& m2_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33386]) ).
fof(f33501,plain,
! [X0] :
( ( v1_funct_1(k2_autgroup(X0))
& v1_funct_2(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
& m2_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33500]) ).
fof(f33532,plain,
! [X0] :
( ! [X1] :
( ( X1 = k2_autgroup(X0)
<=> ! [X2] :
( ! [X3] :
( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X2,X3) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X3,X2)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33403]) ).
fof(f33533,plain,
! [X0] :
( ! [X1] :
( ( X1 = k2_autgroup(X0)
<=> ! [X2] :
( ! [X3] :
( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X2,X3) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X3,X2)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33532]) ).
fof(f33546,plain,
! [X0] :
( ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33410]) ).
fof(f33547,plain,
! [X0] :
( ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33546]) ).
fof(f33550,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1) != k1_binop_1(k2_autgroup(X0),X1,X2)
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f33413]) ).
fof(f33551,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1) != k1_binop_1(k2_autgroup(X0),X1,X2)
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f33550]) ).
fof(f33554,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3371]) ).
fof(f33555,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(flattening,[],[f33554]) ).
fof(f33560,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) )
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3367]) ).
fof(f33585,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21874]) ).
fof(f33586,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33585]) ).
fof(f33605,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_rlvect_1(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21861]) ).
fof(f33606,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_rlvect_1(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33605]) ).
fof(f33659,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f34025,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18993]) ).
fof(f34026,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34025]) ).
fof(f34085,plain,
! [X0,X1,X2,X3,X4,X5] :
( k2_binop_1(X0,X1,X2,X3,X4,X5) = k1_binop_1(X3,X4,X5)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_subset_1(X4,X0)
| ~ m1_subset_1(X5,X1) ),
inference(ennf_transformation,[],[f2436]) ).
fof(f34086,plain,
! [X0,X1,X2,X3,X4,X5] :
( k2_binop_1(X0,X1,X2,X3,X4,X5) = k1_binop_1(X3,X4,X5)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_subset_1(X4,X0)
| ~ m1_subset_1(X5,X1) ),
inference(flattening,[],[f34085]) ).
fof(f36633,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f36636,plain,
! [X0] :
( ! [X1] :
( r1_rlvect_1(X0,X1)
<=> r2_hidden(X1,u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18620]) ).
fof(f37941,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f39527,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k2_autgroup(X0)
| ? [X2] :
( ? [X3] :
( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X2,X3) != k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X3,X2)
& m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X2,X3) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X3,X2)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| k2_autgroup(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f33533]) ).
fof(f39528,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k2_autgroup(X0)
| ? [X2] :
( ? [X3] :
( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X2,X3) != k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X3,X2)
& m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X4,X5) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X5,X4)
| ~ m2_fraenkel(X5,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| k2_autgroup(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f39527]) ).
fof(f39529,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k2_autgroup(X0)
| ( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,sK37(X0,X1),sK38(X0,X1)) != k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),sK38(X0,X1),sK37(X0,X1))
& m2_fraenkel(sK38(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
& m2_fraenkel(sK37(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X4,X5) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X5,X4)
| ~ m2_fraenkel(X5,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| k2_autgroup(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37,sK38]),skolemize(X2,sK37(X0,X1)),skolemize(X3,sK38(X0,X1))],[f39528]) ).
fof(f39534,plain,
( k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),sK46,sK45) != k1_binop_1(k2_autgroup(sK44),sK45,sK46)
& m2_fraenkel(sK46,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44))
& m2_fraenkel(sK45,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44))
& ~ v3_struct_0(sK44)
& v1_group_1(sK44)
& v3_group_1(sK44)
& v4_group_1(sK44)
& l1_group_1(sK44) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44,sK45,sK46]),skolemize(X0,sK44),skolemize(X1,sK45),skolemize(X2,sK46)],[f33551]) ).
fof(f39535,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( m2_fraenkel(X3,X0,X1,X2)
| ~ m1_subset_1(X3,X2) )
& ( m1_subset_1(X3,X2)
| ~ m2_fraenkel(X3,X0,X1,X2) ) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(nnf_transformation,[],[f33555]) ).
fof(f39859,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1483]) ).
fof(f40412,plain,
! [X0] :
( ! [X1] :
( ( r1_rlvect_1(X0,X1)
| ~ r2_hidden(X1,u1_struct_0(X0)) )
& ( r2_hidden(X1,u1_struct_0(X0))
| ~ r1_rlvect_1(X0,X1) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f36636]) ).
fof(f41235,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33499]) ).
fof(f41236,plain,
! [X0] :
( m2_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33501]) ).
fof(f41237,plain,
! [X0] :
( v1_funct_2(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33501]) ).
fof(f41238,plain,
! [X0] :
( v1_funct_1(k2_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33501]) ).
fof(f41295,plain,
! [X0,X1,X4,X5] :
( k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),X1,X4,X5) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X5,X4)
| ~ m2_fraenkel(X5,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| k2_autgroup(X0) != X1
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f39529]) ).
fof(f41313,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33547]) ).
fof(f41315,plain,
l1_group_1(sK44),
inference(cnf_transformation,[],[f39534]) ).
fof(f41316,plain,
v4_group_1(sK44),
inference(cnf_transformation,[],[f39534]) ).
fof(f41317,plain,
v3_group_1(sK44),
inference(cnf_transformation,[],[f39534]) ).
fof(f41318,plain,
v1_group_1(sK44),
inference(cnf_transformation,[],[f39534]) ).
fof(f41319,plain,
~ v3_struct_0(sK44),
inference(cnf_transformation,[],[f39534]) ).
fof(f41320,plain,
m2_fraenkel(sK45,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44)),
inference(cnf_transformation,[],[f39534]) ).
fof(f41321,plain,
m2_fraenkel(sK46,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44)),
inference(cnf_transformation,[],[f39534]) ).
fof(f41322,plain,
k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),sK46,sK45) != k1_binop_1(k2_autgroup(sK44),sK45,sK46),
inference(cnf_transformation,[],[f39534]) ).
fof(f41325,plain,
! [X2,X3,X0,X1] :
( ~ m1_fraenkel(X2,X0,X1)
| ~ m2_fraenkel(X3,X0,X1,X2)
| v1_xboole_0(X1)
| m1_subset_1(X3,X2) ),
inference(cnf_transformation,[],[f39535]) ).
fof(f41333,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X2)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f33560]) ).
fof(f41366,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33586]) ).
fof(f41412,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| r1_rlvect_1(X0,X2)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33606]) ).
fof(f41452,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f33659]) ).
fof(f42056,plain,
! [X0] :
( ~ l1_group_1(X0)
| v3_struct_0(X0)
| m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f34026]) ).
fof(f42142,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| k2_binop_1(X0,X1,X2,X3,X4,X5) = k1_binop_1(X3,X4,X5)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_subset_1(X4,X0)
| ~ m1_subset_1(X5,X1) ),
inference(cnf_transformation,[],[f34086]) ).
fof(f42772,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f39859]) ).
fof(f45424,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36633]) ).
fof(f45426,plain,
! [X0,X1] :
( ~ l1_struct_0(X0)
| ~ r1_rlvect_1(X0,X1)
| r2_hidden(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f40412]) ).
fof(f47227,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f37941]) ).
fof(f50824,plain,
! [X0,X4,X5] :
( ~ v1_funct_2(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m2_fraenkel(X5,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ v1_funct_1(k2_autgroup(X0))
| k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X5,X4) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X4,X5)
| ~ m2_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f41295]) ).
fof(f52205,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ v1_funct_1(k2_autgroup(X0))
| k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X1,X2) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X2,X1)
| ~ m2_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f41237,f50824]) ).
fof(f52206,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ v1_funct_1(k2_autgroup(X0))
| k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X1,X2) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X2,X1)
| ~ m2_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) ),
inference(duplicate_literal_removal,[],[f52205]) ).
fof(f52207,plain,
! [X0] :
( ~ l1_group_1(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f47227,f45424]) ).
fof(f52208,plain,
u1_struct_0(sK44) = k2_pre_topc(sK44),
inference(resolution,[],[f52207,f41315]) ).
fof(f52209,plain,
m2_fraenkel(sK46,k2_pre_topc(sK44),k2_pre_topc(sK44),k4_autgroup(sK44)),
inference(superposition,[],[f41321,f52208]) ).
fof(f52210,plain,
m2_fraenkel(sK45,k2_pre_topc(sK44),k2_pre_topc(sK44),k4_autgroup(sK44)),
inference(superposition,[],[f41320,f52208]) ).
fof(f52211,plain,
k1_binop_1(k2_autgroup(sK44),sK45,sK46) != k7_funct_2(k2_pre_topc(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44),sK46,sK45),
inference(superposition,[],[f41322,f52208]) ).
fof(f52213,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44))
| v3_struct_0(sK44)
| ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ l1_group_1(sK44) ),
inference(resolution,[],[f41313,f41316]) ).
fof(f52214,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44))
| ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52213,f41319]) ).
fof(f52215,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44))
| ~ v3_group_1(sK44)
| m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52214,f41318]) ).
fof(f52216,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44))
| m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52215,f41317]) ).
fof(f52217,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k4_autgroup(sK44))
| m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44)) ),
inference(forward_subsumption_resolution,[],[f52216,f41315]) ).
fof(f52218,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k4_autgroup(sK44))
| m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44)) ),
inference(forward_demodulation,[],[f52217,f52208]) ).
fof(f52219,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k4_autgroup(sK44))
| m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44)) ),
inference(forward_demodulation,[],[f52218,f52208]) ).
fof(f52220,plain,
m2_fraenkel(sK45,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44)),
inference(resolution,[],[f52219,f52210]) ).
fof(f52221,plain,
m2_fraenkel(sK46,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44)),
inference(resolution,[],[f52219,f52209]) ).
fof(f52233,definition,
( spl1179_50
<=> v1_xboole_0(k2_pre_topc(sK44)) ),
introduced(definition,[new_symbols(definition,[spl1179_50])],[avatar_definition]) ).
fof(f52234,plain,
( v1_xboole_0(k2_pre_topc(sK44))
| ~ spl1179_50 ),
inference(avatar_component_clause,[],[f52233]) ).
fof(f52257,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| m1_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(resolution,[],[f42772,f41236]) ).
fof(f52258,plain,
( v3_struct_0(sK44)
| m1_subset_1(k2_group_1(sK44),u1_struct_0(sK44)) ),
inference(resolution,[],[f42056,f41315]) ).
fof(f52259,plain,
m1_subset_1(k2_group_1(sK44),u1_struct_0(sK44)),
inference(forward_subsumption_resolution,[],[f52258,f41319]) ).
fof(f52260,plain,
m1_subset_1(k2_group_1(sK44),k2_pre_topc(sK44)),
inference(forward_demodulation,[],[f52259,f52208]) ).
fof(f52286,plain,
( v3_struct_0(sK44)
| ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| m1_fraenkel(k1_autgroup(sK44),u1_struct_0(sK44),u1_struct_0(sK44))
| ~ l1_group_1(sK44) ),
inference(resolution,[],[f41235,f41316]) ).
fof(f52287,plain,
( ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| m1_fraenkel(k1_autgroup(sK44),u1_struct_0(sK44),u1_struct_0(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52286,f41319]) ).
fof(f52288,plain,
( ~ v3_group_1(sK44)
| m1_fraenkel(k1_autgroup(sK44),u1_struct_0(sK44),u1_struct_0(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52287,f41318]) ).
fof(f52289,plain,
( m1_fraenkel(k1_autgroup(sK44),u1_struct_0(sK44),u1_struct_0(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52288,f41317]) ).
fof(f52290,plain,
m1_fraenkel(k1_autgroup(sK44),u1_struct_0(sK44),u1_struct_0(sK44)),
inference(forward_subsumption_resolution,[],[f52289,f41315]) ).
fof(f52291,plain,
m1_fraenkel(k1_autgroup(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44)),
inference(forward_demodulation,[],[f52290,f52208]) ).
fof(f52293,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| v1_xboole_0(k2_pre_topc(sK44))
| m1_subset_1(X0,k1_autgroup(sK44)) ),
inference(resolution,[],[f52291,f41325]) ).
fof(f52325,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X1,X2) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X2,X1)
| ~ m2_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0)) ),
inference(forward_subsumption_resolution,[],[f52206,f41238]) ).
fof(f52328,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X1,X2) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X2,X1) ),
inference(forward_subsumption_resolution,[],[f52325,f41236]) ).
fof(f52335,plain,
! [X0,X1] :
( ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| v3_struct_0(sK44)
| ~ l1_group_1(sK44)
| ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ m2_fraenkel(X1,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),X0,X1) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X1,X0) ),
inference(resolution,[],[f52328,f41316]) ).
fof(f52336,plain,
! [X0,X1] :
( ~ v3_group_1(sK44)
| v3_struct_0(sK44)
| ~ l1_group_1(sK44)
| ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ m2_fraenkel(X1,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),X0,X1) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X1,X0) ),
inference(forward_subsumption_resolution,[],[f52335,f41318]) ).
fof(f52337,plain,
! [X0,X1] :
( v3_struct_0(sK44)
| ~ l1_group_1(sK44)
| ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ m2_fraenkel(X1,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),X0,X1) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X1,X0) ),
inference(forward_subsumption_resolution,[],[f52336,f41317]) ).
fof(f52338,plain,
! [X0,X1] :
( ~ l1_group_1(sK44)
| ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ m2_fraenkel(X1,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),X0,X1) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X1,X0) ),
inference(forward_subsumption_resolution,[],[f52337,f41319]) ).
fof(f52339,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| ~ m2_fraenkel(X1,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),X0,X1) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X1,X0) ),
inference(forward_subsumption_resolution,[],[f52338,f41315]) ).
fof(f52340,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| ~ m2_fraenkel(X1,u1_struct_0(sK44),u1_struct_0(sK44),k1_autgroup(sK44))
| k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),X0,X1) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X1,X0) ),
inference(forward_demodulation,[],[f52339,f52208]) ).
fof(f52341,plain,
! [X0,X1] :
( ~ m2_fraenkel(X1,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| k7_funct_2(u1_struct_0(sK44),u1_struct_0(sK44),u1_struct_0(sK44),X0,X1) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X1,X0) ),
inference(forward_demodulation,[],[f52340,f52208]) ).
fof(f52342,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| ~ m2_fraenkel(X1,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X1,X0) = k7_funct_2(k2_pre_topc(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44),X0,X1) ),
inference(forward_demodulation,[],[f52341,f52208]) ).
fof(f52343,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X0,sK46) = k7_funct_2(k2_pre_topc(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44),sK46,X0) ),
inference(resolution,[],[f52342,f52221]) ).
fof(f52387,plain,
k7_funct_2(k2_pre_topc(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44),sK46,sK45) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),sK45,sK46),
inference(resolution,[],[f52343,f52220]) ).
fof(f52463,plain,
! [X2,X0,X1] :
( v1_xboole_0(k1_autgroup(X0))
| v1_xboole_0(k1_autgroup(X0))
| ~ v1_funct_1(k2_autgroup(X0))
| k1_binop_1(k2_autgroup(X0),X1,X2) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X1,X2)
| ~ m1_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m1_subset_1(X1,k1_autgroup(X0))
| ~ m1_subset_1(X2,k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f42142,f41237]) ).
fof(f52464,plain,
! [X2,X0,X1] :
( v1_xboole_0(k1_autgroup(X0))
| ~ v1_funct_1(k2_autgroup(X0))
| k1_binop_1(k2_autgroup(X0),X1,X2) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X1,X2)
| ~ m1_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m1_subset_1(X1,k1_autgroup(X0))
| ~ m1_subset_1(X2,k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(duplicate_literal_removal,[],[f52463]) ).
fof(f52465,plain,
! [X2,X0,X1] :
( v1_xboole_0(k1_autgroup(X0))
| k1_binop_1(k2_autgroup(X0),X1,X2) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X1,X2)
| ~ m1_relset_1(k2_autgroup(X0),k2_zfmisc_1(k1_autgroup(X0),k1_autgroup(X0)),k1_autgroup(X0))
| ~ m1_subset_1(X1,k1_autgroup(X0))
| ~ m1_subset_1(X2,k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f52464,f41238]) ).
fof(f52466,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| k1_binop_1(k2_autgroup(X0),X1,X2) = k2_binop_1(k1_autgroup(X0),k1_autgroup(X0),k1_autgroup(X0),k2_autgroup(X0),X1,X2)
| ~ m1_subset_1(X1,k1_autgroup(X0))
| ~ m1_subset_1(X2,k1_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| v1_xboole_0(k1_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f52465,f52257]) ).
fof(f52467,plain,
! [X0,X1] :
( k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X0,X1) = k1_binop_1(k2_autgroup(sK44),X0,X1)
| ~ m1_subset_1(X0,k1_autgroup(sK44))
| ~ m1_subset_1(X1,k1_autgroup(sK44))
| v3_struct_0(sK44)
| ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| v1_xboole_0(k1_autgroup(sK44))
| ~ l1_group_1(sK44) ),
inference(resolution,[],[f52466,f41316]) ).
fof(f52468,plain,
! [X0,X1] :
( k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X0,X1) = k1_binop_1(k2_autgroup(sK44),X0,X1)
| ~ m1_subset_1(X0,k1_autgroup(sK44))
| ~ m1_subset_1(X1,k1_autgroup(sK44))
| ~ v1_group_1(sK44)
| ~ v3_group_1(sK44)
| v1_xboole_0(k1_autgroup(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52467,f41319]) ).
fof(f52469,plain,
! [X0,X1] :
( k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X0,X1) = k1_binop_1(k2_autgroup(sK44),X0,X1)
| ~ m1_subset_1(X0,k1_autgroup(sK44))
| ~ m1_subset_1(X1,k1_autgroup(sK44))
| ~ v3_group_1(sK44)
| v1_xboole_0(k1_autgroup(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52468,f41318]) ).
fof(f52470,plain,
! [X0,X1] :
( k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X0,X1) = k1_binop_1(k2_autgroup(sK44),X0,X1)
| ~ m1_subset_1(X0,k1_autgroup(sK44))
| ~ m1_subset_1(X1,k1_autgroup(sK44))
| v1_xboole_0(k1_autgroup(sK44))
| ~ l1_group_1(sK44) ),
inference(forward_subsumption_resolution,[],[f52469,f41317]) ).
fof(f52471,plain,
! [X0,X1] :
( k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X0,X1) = k1_binop_1(k2_autgroup(sK44),X0,X1)
| ~ m1_subset_1(X0,k1_autgroup(sK44))
| ~ m1_subset_1(X1,k1_autgroup(sK44))
| v1_xboole_0(k1_autgroup(sK44)) ),
inference(forward_subsumption_resolution,[],[f52470,f41315]) ).
fof(f52473,definition,
( spl1179_62
<=> v1_xboole_0(k1_autgroup(sK44)) ),
introduced(definition,[new_symbols(definition,[spl1179_62])],[avatar_definition]) ).
fof(f52474,plain,
( v1_xboole_0(k1_autgroup(sK44))
| ~ spl1179_62 ),
inference(avatar_component_clause,[],[f52473]) ).
fof(f52476,definition,
( spl1179_63
<=> ! [X0,X1] :
( k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X0,X1) = k1_binop_1(k2_autgroup(sK44),X0,X1)
| ~ m1_subset_1(X1,k1_autgroup(sK44))
| ~ m1_subset_1(X0,k1_autgroup(sK44)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_63])],[avatar_definition]) ).
fof(f52477,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_autgroup(sK44))
| ~ m1_subset_1(X1,k1_autgroup(sK44))
| k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),X0,X1) = k1_binop_1(k2_autgroup(sK44),X0,X1) )
| ~ spl1179_63 ),
inference(avatar_component_clause,[],[f52476]) ).
fof(f52478,plain,
( spl1179_62
| spl1179_63 ),
inference(avatar_split_clause,[],[f52471,f52476,f52473]) ).
fof(f52479,plain,
( $false
| ~ spl1179_62 ),
inference(unit_resulting_resolution,[],[f41333,f52291,f52474]) ).
fof(f52481,plain,
~ spl1179_62,
inference(avatar_contradiction_clause,[],[f52479]) ).
fof(f52571,plain,
( ! [X0] : ~ r2_hidden(X0,k2_pre_topc(sK44))
| ~ spl1179_50 ),
inference(resolution,[],[f41452,f52234]) ).
fof(f53119,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| r1_rlvect_1(X1,X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(resolution,[],[f41412,f41366]) ).
fof(f53120,plain,
! [X0,X1] :
( ~ v4_group_1(X1)
| r1_rlvect_1(X1,X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(duplicate_literal_removal,[],[f53119]) ).
fof(f53121,plain,
! [X0] :
( r1_rlvect_1(sK44,X0)
| v3_struct_0(sK44)
| ~ v3_group_1(sK44)
| ~ l1_group_1(sK44)
| ~ m1_subset_1(X0,u1_struct_0(sK44)) ),
inference(resolution,[],[f53120,f41316]) ).
fof(f53125,plain,
! [X0] :
( r1_rlvect_1(sK44,X0)
| ~ v3_group_1(sK44)
| ~ l1_group_1(sK44)
| ~ m1_subset_1(X0,u1_struct_0(sK44)) ),
inference(forward_subsumption_resolution,[],[f53121,f41319]) ).
fof(f53127,plain,
! [X0] :
( r1_rlvect_1(sK44,X0)
| ~ l1_group_1(sK44)
| ~ m1_subset_1(X0,u1_struct_0(sK44)) ),
inference(forward_subsumption_resolution,[],[f53125,f41317]) ).
fof(f53129,plain,
! [X0] :
( r1_rlvect_1(sK44,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK44)) ),
inference(forward_subsumption_resolution,[],[f53127,f41315]) ).
fof(f53134,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK44))
| r1_rlvect_1(sK44,X0) ),
inference(forward_demodulation,[],[f53129,f52208]) ).
fof(f53135,plain,
r1_rlvect_1(sK44,k2_group_1(sK44)),
inference(resolution,[],[f53134,f52260]) ).
fof(f53439,plain,
! [X0,X1] :
( ~ r1_rlvect_1(X0,X1)
| r2_hidden(X1,u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(resolution,[],[f45426,f45424]) ).
fof(f53440,plain,
( r2_hidden(k2_group_1(sK44),u1_struct_0(sK44))
| ~ l1_group_1(sK44) ),
inference(resolution,[],[f53439,f53135]) ).
fof(f53441,plain,
r2_hidden(k2_group_1(sK44),u1_struct_0(sK44)),
inference(forward_subsumption_resolution,[],[f53440,f41315]) ).
fof(f53442,plain,
r2_hidden(k2_group_1(sK44),k2_pre_topc(sK44)),
inference(forward_demodulation,[],[f53441,f52208]) ).
fof(f53443,plain,
( $false
| ~ spl1179_50 ),
inference(forward_subsumption_resolution,[],[f53442,f52571]) ).
fof(f53444,plain,
~ spl1179_50,
inference(avatar_contradiction_clause,[],[f53443]) ).
fof(f53454,definition,
( spl1179_145
<=> ! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| m1_subset_1(X0,k1_autgroup(sK44)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_145])],[avatar_definition]) ).
fof(f53455,plain,
( ! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK44),k2_pre_topc(sK44),k1_autgroup(sK44))
| m1_subset_1(X0,k1_autgroup(sK44)) )
| ~ spl1179_145 ),
inference(avatar_component_clause,[],[f53454]) ).
fof(f53456,plain,
( spl1179_50
| spl1179_145 ),
inference(avatar_split_clause,[],[f52293,f53454,f52233]) ).
fof(f53470,plain,
( m1_subset_1(sK46,k1_autgroup(sK44))
| ~ spl1179_145 ),
inference(resolution,[],[f53455,f52221]) ).
fof(f53471,plain,
( m1_subset_1(sK45,k1_autgroup(sK44))
| ~ spl1179_145 ),
inference(resolution,[],[f53455,f52220]) ).
fof(f53482,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_autgroup(sK44))
| k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),sK45,X0) = k1_binop_1(k2_autgroup(sK44),sK45,X0) )
| ~ spl1179_63
| ~ spl1179_145 ),
inference(resolution,[],[f53471,f52477]) ).
fof(f53490,plain,
( k1_binop_1(k2_autgroup(sK44),sK45,sK46) = k2_binop_1(k1_autgroup(sK44),k1_autgroup(sK44),k1_autgroup(sK44),k2_autgroup(sK44),sK45,sK46)
| ~ spl1179_63
| ~ spl1179_145 ),
inference(resolution,[],[f53482,f53470]) ).
fof(f53494,plain,
( k1_binop_1(k2_autgroup(sK44),sK45,sK46) = k7_funct_2(k2_pre_topc(sK44),k2_pre_topc(sK44),k2_pre_topc(sK44),sK46,sK45)
| ~ spl1179_63
| ~ spl1179_145 ),
inference(superposition,[],[f53490,f52387]) ).
fof(f53498,plain,
( $false
| ~ spl1179_63
| ~ spl1179_145 ),
inference(forward_subsumption_resolution,[],[f53494,f52211]) ).
fof(f53499,plain,
( ~ spl1179_63
| ~ spl1179_145 ),
inference(avatar_contradiction_clause,[],[f53498]) ).
cnf(s53,plain,
( spl1179_62
| spl1179_63 ),
inference(sat_conversion,[],[f52478]) ).
cnf(s54,plain,
~ spl1179_62,
inference(sat_conversion,[],[f52481]) ).
cnf(s117,plain,
~ spl1179_50,
inference(sat_conversion,[],[f53444]) ).
cnf(s120,plain,
( spl1179_50
| spl1179_145 ),
inference(sat_conversion,[],[f53456]) ).
cnf(s127,plain,
( ~ spl1179_63
| ~ spl1179_145 ),
inference(sat_conversion,[],[f53499]) ).
cnf(s131,plain,
spl1179_145,
inference(rat,[],[s120,s117]) ).
cnf(s134,plain,
~ spl1179_63,
inference(rat,[],[s127,s131]) ).
cnf(s197,plain,
$false,
inference(rat,[],[s53,s134,s54]) ).
fof(f53500,plain,
$false,
inference(avatar_sat_refutation,[],[s197]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP624+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.43 % Computer : n010.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 27 10:10:51 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.48 Running first-order theorem proving
% 0.22/0.48 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
% 28.08/7.35 % (736669)Detected formulas, will run a generic FOF schedule.
% 28.08/7.35 % (736678)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=1410489122:i=141193_2973 on theBenchmark for (2973ds/141193Mi)
% 28.08/7.35 % (736680)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=2220836515:i=141695:sd=1:nm=32:gsp=on:ss=included_2973 on theBenchmark for (2973ds/141695Mi)
% 28.08/7.35 % (736679)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=72702837:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2973 on theBenchmark for (2973ds/134677Mi)
% 28.08/7.35 % (736681)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3386693606:i=109:sd=1:ins=1:gsp=on:ss=axioms_2973 on theBenchmark for (2973ds/109Mi)
% 28.08/7.35 % (736682)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3518366556:i=119:av=off:ss=axioms_2973 on theBenchmark for (2973ds/119Mi)
% 28.08/7.35 % (736683)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2987176661:s2a=on:i=139:gtg=position_2973 on theBenchmark for (2973ds/139Mi)
% 28.08/7.35 % (736684)dis-21_1_sil=8000:lcm=predicate:random_seed=3427438382:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2973 on theBenchmark for (2973ds/129Mi)
% 28.08/7.35 % (736681)Instruction limit reached!
% 28.08/7.35 % (736681)------------------------------
% 28.08/7.35 % (736681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.08/7.35 % (736681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.08/7.35 % (736681)CaDiCaL version: 2.1.3
% 28.08/7.35 % (736681)Termination reason: Instruction limit
% 28.08/7.35 % (736681)Termination phase: SInE selection
% 28.08/7.35 % (736681)Time elapsed: 0.118 s
% 28.08/7.35 % (736681)Peak memory usage: 133 MB
% 28.08/7.35 % (736681)Instructions burned: 109 (million)
% 28.08/7.35 % (736682)Instruction limit reached!
% 28.08/7.35 % (736682)------------------------------
% 28.08/7.35 % (736682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.08/7.35 % (736682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.08/7.35 % (736682)CaDiCaL version: 2.1.3
% 28.08/7.35 % (736682)Termination reason: Instruction limit
% 28.08/7.35 % (736682)Termination phase: SInE selection
% 28.08/7.35 % (736682)Time elapsed: 0.128 s
% 28.08/7.35 % (736682)Peak memory usage: 133 MB
% 28.08/7.35 % (736682)Instructions burned: 119 (million)
% 28.08/7.35 % (736683)Instruction limit reached!
% 28.08/7.35 % (736683)------------------------------
% 28.08/7.35 % (736683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.08/7.35 % (736683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.08/7.35 % (736683)CaDiCaL version: 2.1.3
% 28.08/7.35 % (736683)Termination reason: Instruction limit
% 28.08/7.35 % (736683)Termination phase: Property scanning
% 28.08/7.35 % (736683)Time elapsed: 0.119 s
% 28.08/7.35 % (736683)Peak memory usage: 133 MB
% 28.08/7.35 % (736683)Instructions burned: 139 (million)
% 28.08/7.35 % (736684)Instruction limit reached!
% 28.08/7.35 % (736684)------------------------------
% 28.08/7.35 % (736684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.08/7.35 % (736684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.08/7.35 % (736684)CaDiCaL version: 2.1.3
% 28.08/7.35 % (736684)Termination reason: Instruction limit
% 28.08/7.35 % (736684)Termination phase: SInE selection
% 28.08/7.35 % (736684)Time elapsed: 0.135 s
% 28.08/7.35 % (736684)Peak memory usage: 133 MB
% 28.08/7.35 % (736684)Instructions burned: 129 (million)
% 28.08/7.35 % (736692)lrs+10_1_sil=8000:sp=occurrence:random_seed=262212237:i=285:sd=3:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/285Mi)
% 28.08/7.35 % (736694)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1474873426:i=325:sd=1:ss=axioms:sgt=32_2969 on theBenchmark for (2969ds/325Mi)
% 28.08/7.35 % (736693)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2024360971:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/157Mi)
% 28.08/7.35 % (736695)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=2892428671:s2a=on:i=248:s2at=1.23:gtg=position_2968 on theBenchmark for (2968ds/248Mi)
% 28.08/7.35 % (736693)Instruction limit reached!
% 28.08/7.35 % (736693)------------------------------
% 41.45/9.24 % (736693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.45/9.24 % (736693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.45/9.24 % (736693)CaDiCaL version: 2.1.3
% 41.45/9.24 % (736693)Termination reason: Instruction limit
% 41.45/9.24 % (736693)Termination phase: Property scanning
% 41.45/9.24 % (736693)Time elapsed: 0.135 s
% 41.45/9.24 % (736693)Peak memory usage: 133 MB
% 41.45/9.24 % (736693)Instructions burned: 157 (million)
% 41.45/9.24 % (736695)Instruction limit reached!
% 41.45/9.24 % (736695)------------------------------
% 41.45/9.24 % (736695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.45/9.24 % (736695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.45/9.24 % (736695)CaDiCaL version: 2.1.3
% 41.45/9.24 % (736695)Termination reason: Instruction limit
% 41.45/9.24 % (736695)Termination phase: Property scanning
% 41.45/9.24 % (736695)Time elapsed: 0.157 s
% 41.45/9.24 % (736695)Peak memory usage: 133 MB
% 41.45/9.24 % (736695)Instructions burned: 249 (million)
% 41.45/9.24 % (736694)Refutation not found, incomplete strategy
% 41.45/9.24 % (736694)------------------------------
% 41.45/9.24 % (736694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.45/9.24 % (736694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.45/9.24 % (736694)CaDiCaL version: 2.1.3
% 41.45/9.24 % (736694)Termination reason: Refutation not found, incomplete strategy
% 41.45/9.24 % (736694)Time elapsed: 0.266 s
% 41.45/9.24 % (736694)Peak memory usage: 139 MB
% 41.45/9.24 % (736694)Instructions burned: 235 (million)
% 41.45/9.24 % (736692)Instruction limit reached!
% 41.45/9.24 % (736692)------------------------------
% 41.45/9.24 % (736692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.45/9.24 % (736692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.45/9.24 % (736692)CaDiCaL version: 2.1.3
% 41.45/9.24 % (736692)Termination reason: Instruction limit
% 41.45/9.24 % (736692)Termination phase: Property scanning
% 41.45/9.24 % (736692)Time elapsed: 0.329 s
% 41.45/9.24 % (736692)Peak memory usage: 138 MB
% 41.45/9.24 % (736692)Instructions burned: 286 (million)
% 41.45/9.24 % (736700)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1215350993:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2965 on theBenchmark for (2965ds/294Mi)
% 41.45/9.24 % (736701)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1339805775:i=2350_2964 on theBenchmark for (2964ds/2350Mi)
% 41.45/9.24 % (736702)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4188462057:cts=off:i=113:fsr=off:ss=included:sgt=4_2963 on theBenchmark for (2963ds/113Mi)
% 41.45/9.24 % (736700)Instruction limit reached!
% 41.45/9.24 % (736700)------------------------------
% 41.45/9.24 % (736700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.45/9.24 % (736700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.45/9.24 % (736700)CaDiCaL version: 2.1.3
% 41.45/9.24 % (736700)Termination reason: Instruction limit
% 41.45/9.24 % (736700)Termination phase: SInE selection
% 41.45/9.24 % (736700)Time elapsed: 0.272 s
% 41.45/9.24 % (736700)Peak memory usage: 134 MB
% 41.45/9.24 % (736700)Instructions burned: 294 (million)
% 41.45/9.24 % (736694)------------------------------
% 41.45/9.24 % (736694)------------------------------
% 41.45/9.24 % (736702)Instruction limit reached!
% 41.45/9.24 % (736702)------------------------------
% 41.45/9.24 % (736702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.45/9.24 % (736702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.45/9.24 % (736702)CaDiCaL version: 2.1.3
% 41.45/9.24 % (736702)Termination reason: Instruction limit
% 41.45/9.24 % (736702)Termination phase: SInE selection
% 41.45/9.24 % (736702)Time elapsed: 0.128 s
% 41.45/9.24 % (736702)Peak memory usage: 133 MB
% 41.45/9.24 % (736702)Instructions burned: 113 (million)
% 41.45/9.24 % (736707)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2253591885:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2959 on theBenchmark for (2959ds/114Mi)
% 41.45/9.24 % (736706)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4133897467:i=127:av=off:fsr=off:sup=off_2959 on theBenchmark for (2959ds/127Mi)
% 41.45/9.24 % (736707)Instruction limit reached!
% 41.45/9.24 % (736707)------------------------------
% 41.45/9.24 % (736707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736707)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736707)Termination reason: Instruction limit
% 30.45/10.20 % (736707)Termination phase: Property scanning
% 30.45/10.20 % (736707)Time elapsed: 0.066 s
% 30.45/10.20 % (736707)Peak memory usage: 134 MB
% 30.45/10.20 % (736707)Instructions burned: 115 (million)
% 30.45/10.20 % (736708)lrs+10_1_sil=8000:sp=occurrence:random_seed=3358571730:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2959 on theBenchmark for (2959ds/907Mi)
% 30.45/10.20 % (736706)Instruction limit reached!
% 30.45/10.20 % (736706)------------------------------
% 30.45/10.20 % (736706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736706)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736706)Termination reason: Instruction limit
% 30.45/10.20 % (736706)Termination phase: Preprocessing 1
% 30.45/10.20 % (736706)Time elapsed: 0.155 s
% 30.45/10.20 % (736706)Peak memory usage: 135 MB
% 30.45/10.20 % (736706)Instructions burned: 127 (million)
% 30.45/10.20 % (736711)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2550681947:i=437:sd=1:aac=none:ss=included_2956 on theBenchmark for (2956ds/437Mi)
% 30.45/10.20 % (736713)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2312008055:i=5202:ss=axioms:sgt=16_2955 on theBenchmark for (2955ds/5202Mi)
% 30.45/10.20 % (736711)Instruction limit reached!
% 30.45/10.20 % (736711)------------------------------
% 30.45/10.20 % (736711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736711)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736711)Termination reason: Instruction limit
% 30.45/10.20 % (736711)Termination phase: Saturation
% 30.45/10.20 % (736711)Time elapsed: 0.498 s
% 30.45/10.20 % (736711)Peak memory usage: 142 MB
% 30.45/10.20 % (736711)Instructions burned: 437 (million)
% 30.45/10.20 % (736708)Instruction limit reached!
% 30.45/10.20 % (736708)------------------------------
% 30.45/10.20 % (736708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736708)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736708)Termination reason: Instruction limit
% 30.45/10.20 % (736708)Termination phase: Property scanning
% 30.45/10.20 % (736708)Time elapsed: 0.905 s
% 30.45/10.20 % (736708)Peak memory usage: 154 MB
% 30.45/10.20 % (736708)Instructions burned: 907 (million)
% 30.45/10.20 % (736716)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=571163598:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2949 on theBenchmark for (2949ds/134Mi)
% 30.45/10.20 % (736716)Instruction limit reached!
% 30.45/10.20 % (736716)------------------------------
% 30.45/10.20 % (736716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736716)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736716)Termination reason: Instruction limit
% 30.45/10.20 % (736716)Termination phase: SInE selection
% 30.45/10.20 % (736716)Time elapsed: 0.151 s
% 30.45/10.20 % (736716)Peak memory usage: 133 MB
% 30.45/10.20 % (736716)Instructions burned: 135 (million)
% 30.45/10.20 % (736717)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1925486042:st=8:i=592:sd=3:ep=RST:ss=axioms_2947 on theBenchmark for (2947ds/592Mi)
% 30.45/10.20 % (736719)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2632971471:st=3:i=13193:sd=3:ss=axioms_2945 on theBenchmark for (2945ds/13193Mi)
% 30.45/10.20 % (736717)Instruction limit reached!
% 30.45/10.20 % (736717)------------------------------
% 30.45/10.20 % (736717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736717)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736717)Termination reason: Instruction limit
% 30.45/10.20 % (736717)Termination phase: Preprocessing 2
% 30.45/10.20 % (736717)Time elapsed: 0.669 s
% 30.45/10.20 % (736717)Peak memory usage: 141 MB
% 30.45/10.20 % (736717)Instructions burned: 592 (million)
% 30.45/10.20 % (736701)Instruction limit reached!
% 30.45/10.20 % (736701)------------------------------
% 30.45/10.20 % (736701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736701)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736701)Termination reason: Instruction limit
% 30.45/10.20 % (736701)Termination phase: Property scanning
% 30.45/10.20 % (736701)Time elapsed: 2.439 s
% 30.45/10.20 % (736701)Peak memory usage: 227 MB
% 30.45/10.20 % (736701)Instructions burned: 2351 (million)
% 30.45/10.20 % (736722)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=570574431:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2937 on theBenchmark for (2937ds/125Mi)
% 30.45/10.20 % (736723)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1819334834:i=134:gtgl=5:slsql=off:gtg=exists_sym_2937 on theBenchmark for (2937ds/134Mi)
% 30.45/10.20 % (736722)Instruction limit reached!
% 30.45/10.20 % (736722)------------------------------
% 30.45/10.20 % (736722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736722)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736722)Termination reason: Instruction limit
% 30.45/10.20 % (736722)Termination phase: Property scanning
% 30.45/10.20 % (736722)Time elapsed: 0.107 s
% 30.45/10.20 % (736722)Peak memory usage: 133 MB
% 30.45/10.20 % (736722)Instructions burned: 125 (million)
% 30.45/10.20 % (736723)Instruction limit reached!
% 30.45/10.20 % (736723)------------------------------
% 30.45/10.20 % (736723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736723)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736723)Termination reason: Instruction limit
% 30.45/10.20 % (736723)Termination phase: Property scanning
% 30.45/10.20 % (736723)Time elapsed: 0.115 s
% 30.45/10.20 % (736723)Peak memory usage: 133 MB
% 30.45/10.20 % (736723)Instructions burned: 135 (million)
% 30.45/10.20 % (736726)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2044868779:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2933 on theBenchmark for (2933ds/141Mi)
% 30.45/10.20 % (736727)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3170738715:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2932 on theBenchmark for (2932ds/431Mi)
% 30.45/10.20 % (736726)Instruction limit reached!
% 30.45/10.20 % (736726)------------------------------
% 30.45/10.20 % (736726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736726)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736726)Termination reason: Instruction limit
% 30.45/10.20 % (736726)Termination phase: SInE selection
% 30.45/10.20 % (736726)Time elapsed: 0.160 s
% 30.45/10.20 % (736726)Peak memory usage: 133 MB
% 30.45/10.20 % (736726)Instructions burned: 141 (million)
% 30.45/10.20 % (736727)Refutation not found, incomplete strategy
% 30.45/10.20 % (736727)------------------------------
% 30.45/10.20 % (736727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736727)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736727)Termination reason: Refutation not found, incomplete strategy
% 30.45/10.20 % (736727)Time elapsed: 0.273 s
% 30.45/10.20 % (736727)Peak memory usage: 139 MB
% 30.45/10.20 % (736727)Instructions burned: 233 (million)
% 30.45/10.20 % (736730)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=2709747021:i=6060:aac=none:ins=25_2929 on theBenchmark for (2929ds/6060Mi)
% 30.45/10.20 % (736727)------------------------------
% 30.45/10.20 % (736727)------------------------------
% 30.45/10.20 % (736732)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=4280886522:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2923 on theBenchmark for (2923ds/150Mi)
% 30.45/10.20 % (736732)Instruction limit reached!
% 30.45/10.20 % (736732)------------------------------
% 30.45/10.20 % (736732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.45/10.20 % (736732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.45/10.20 % (736732)CaDiCaL version: 2.1.3
% 30.45/10.20 % (736732)Termination reason: Instruction limit
% 30.45/10.20 % (736732)Termination phase: SInE selection
% 30.45/10.20 % (736732)Time elapsed: 0.164 s
% 30.45/10.20 % (736732)Peak memory usage: 133 MB
% 30.45/10.20 % (736732)Instructions burned: 150 (million)
% 30.45/10.20 % (736679)First to succeed.
% 30.45/10.20 % (736679)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-736669"
% 30.45/10.20 % (736734)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1766599443:i=14155:bd=all_2918 on theBenchmark for (2918ds/14155Mi)
% 30.45/10.20 % (736679)Refutation found. Thanks to Tanya!
% 30.45/10.20 % SZS status Theorem for theBenchmark
% 30.45/10.20 % SZS output start Proof for theBenchmark
% See solution above
% 47.66/10.37 % (736679)------------------------------
% 47.66/10.37 % (736679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.66/10.37 % (736679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.66/10.37 % (736679)CaDiCaL version: 2.1.3
% 47.66/10.37 % (736679)Termination reason: Refutation
% 47.66/10.37 % (736679)Time elapsed: 5.515 s
% 47.66/10.37 % (736679)Peak memory usage: 285 MB
% 47.66/10.37 % (736679)Instructions burned: 5720 (million)
% 47.66/10.37 % (736679)------------------------------
% 47.66/10.37 % (736679)------------------------------
% 47.66/10.37 % (736669)Success in time 9.093 s
% 47.66/10.37 % Vampire exiting
%------------------------------------------------------------------------------