%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP637+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:11 AM UTC 2026
% Result : Theorem 75.55s 12.47s
% Output : Refutation 77.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 16
% Syntax : Number of formulae : 156 ( 38 unt; 3 def)
% Number of atoms : 641 ( 54 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 813 ( 328 ~; 330 |; 110 &)
% ( 7 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 4 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-4 aty)
% Number of variables : 184 ( 0 sgn 170 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f865,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t156_relat_1) ).
fof(f1333,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(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/sandbox/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/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f2005,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1) )
=> k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f7470,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_group_1) ).
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/sandbox/benchmark/theBenchmark.p',t66_group_2) ).
fof(f8791,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> k7_group_2(X0,X1) = u1_struct_0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_group_2) ).
fof(f8843,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( k12_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1)
& k13_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t132_group_2) ).
fof(f9158,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_group_2(X3,X0)
=> ( m1_group_2(X2,X3)
=> ( r1_tarski(k12_group_2(X0,X2,X1),k12_group_2(X0,X3,X1))
& r1_tarski(k13_group_2(X0,X2,X1),k13_group_2(X0,X3,X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_group_3) ).
fof(f11205,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,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_group_6) ).
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/sandbox/benchmark/theBenchmark.p',redefinition_m1_group_6) ).
fof(f13973,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_group_2(X4,X0)
=> ! [X5] :
( m1_group_2(X5,X1)
=> ! [X6] :
( m1_group_2(X6,X1)
=> ( ( u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X0,X4) )
=> m1_group_6(X5,X1,X6) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_latsubgr) ).
fof(f13974,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_group_2(X4,X0)
=> ! [X5] :
( m1_group_2(X5,X1)
=> ! [X6] :
( m1_group_2(X6,X1)
=> ( ( u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X0,X4) )
=> m1_group_6(X5,X1,X6) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13973]) ).
fof(f14033,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ~ m1_group_6(X5,X1,X6)
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X0,X4)
& m1_group_2(X6,X1) )
& m1_group_2(X5,X1) )
& m1_group_2(X4,X0) )
& m1_group_2(X3,X0) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f13974]) ).
fof(f14034,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ~ m1_group_6(X5,X1,X6)
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X0,X4)
& m1_group_2(X6,X1) )
& m1_group_2(X5,X1) )
& m1_group_2(X4,X0) )
& m1_group_2(X3,X0) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f14033]) ).
fof(f14047,plain,
! [X0,X1,X2,X3] :
( k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f2005]) ).
fof(f14048,plain,
! [X0,X1,X2,X3] :
( k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f14047]) ).
fof(f14067,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(f14068,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,[],[f14067]) ).
fof(f14091,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(f14092,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,[],[f14091]) ).
fof(f14095,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_2(X2,X0)
| ~ 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(ennf_transformation,[],[f11205]) ).
fof(f14096,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_2(X2,X0)
| ~ 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(flattening,[],[f14095]) ).
fof(f14328,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f865]) ).
fof(f14329,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f14328]) ).
fof(f14514,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f7470]) ).
fof(f14515,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14514]) ).
fof(f14617,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r1_tarski(k12_group_2(X0,X2,X1),k12_group_2(X0,X3,X1))
& r1_tarski(k13_group_2(X0,X2,X1),k13_group_2(X0,X3,X1)) )
| ~ m1_group_2(X2,X3)
| ~ m1_group_2(X3,X0) )
| ~ m1_group_2(X2,X0) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f9158]) ).
fof(f14618,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r1_tarski(k12_group_2(X0,X2,X1),k12_group_2(X0,X3,X1))
& r1_tarski(k13_group_2(X0,X2,X1),k13_group_2(X0,X3,X1)) )
| ~ m1_group_2(X2,X3)
| ~ m1_group_2(X3,X0) )
| ~ m1_group_2(X2,X0) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14617]) ).
fof(f14641,plain,
! [X0] :
( ! [X1] :
( ( k12_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1)
& k13_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8843]) ).
fof(f14642,plain,
! [X0] :
( ! [X1] :
( ( k12_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1)
& k13_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14641]) ).
fof(f14918,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(f14919,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(f15452,plain,
! [X0] :
( ! [X1] :
( k7_group_2(X0,X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8791]) ).
fof(f15453,plain,
! [X0] :
( ! [X1] :
( k7_group_2(X0,X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f15452]) ).
fof(f16311,plain,
( ~ m1_group_6(sK36,sK32,sK37)
& u1_struct_0(sK36) = k2_funct_2(u1_struct_0(sK31),u1_struct_0(sK32),sK33,u1_struct_0(sK34))
& u1_struct_0(sK37) = k2_funct_2(u1_struct_0(sK31),u1_struct_0(sK32),sK33,u1_struct_0(sK35))
& m1_group_6(sK34,sK31,sK35)
& m1_group_2(sK37,sK32)
& m1_group_2(sK36,sK32)
& m1_group_2(sK35,sK31)
& m1_group_2(sK34,sK31)
& v1_funct_1(sK33)
& v1_funct_2(sK33,u1_struct_0(sK31),u1_struct_0(sK32))
& v1_group_6(sK33,sK31,sK32)
& m2_relset_1(sK33,u1_struct_0(sK31),u1_struct_0(sK32))
& ~ v3_struct_0(sK32)
& v3_group_1(sK32)
& v4_group_1(sK32)
& l1_group_1(sK32)
& ~ v3_struct_0(sK31)
& v3_group_1(sK31)
& v4_group_1(sK31)
& l1_group_1(sK31) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32,sK33,sK34,sK35,sK36,sK37]),skolemize(X0,sK31),skolemize(X1,sK32),skolemize(X2,sK33),skolemize(X3,sK34),skolemize(X4,sK35),skolemize(X5,sK36),skolemize(X6,sK37)],[f14034]) ).
fof(f16323,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,[],[f14092]) ).
fof(f16410,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(f17048,plain,
l1_group_1(sK31),
inference(cnf_transformation,[],[f16311]) ).
fof(f17049,plain,
v4_group_1(sK31),
inference(cnf_transformation,[],[f16311]) ).
fof(f17050,plain,
v3_group_1(sK31),
inference(cnf_transformation,[],[f16311]) ).
fof(f17051,plain,
~ v3_struct_0(sK31),
inference(cnf_transformation,[],[f16311]) ).
fof(f17052,plain,
l1_group_1(sK32),
inference(cnf_transformation,[],[f16311]) ).
fof(f17053,plain,
v4_group_1(sK32),
inference(cnf_transformation,[],[f16311]) ).
fof(f17054,plain,
v3_group_1(sK32),
inference(cnf_transformation,[],[f16311]) ).
fof(f17055,plain,
~ v3_struct_0(sK32),
inference(cnf_transformation,[],[f16311]) ).
fof(f17056,plain,
m2_relset_1(sK33,u1_struct_0(sK31),u1_struct_0(sK32)),
inference(cnf_transformation,[],[f16311]) ).
fof(f17058,plain,
v1_funct_2(sK33,u1_struct_0(sK31),u1_struct_0(sK32)),
inference(cnf_transformation,[],[f16311]) ).
fof(f17059,plain,
v1_funct_1(sK33),
inference(cnf_transformation,[],[f16311]) ).
fof(f17060,plain,
m1_group_2(sK34,sK31),
inference(cnf_transformation,[],[f16311]) ).
fof(f17061,plain,
m1_group_2(sK35,sK31),
inference(cnf_transformation,[],[f16311]) ).
fof(f17062,plain,
m1_group_2(sK36,sK32),
inference(cnf_transformation,[],[f16311]) ).
fof(f17063,plain,
m1_group_2(sK37,sK32),
inference(cnf_transformation,[],[f16311]) ).
fof(f17064,plain,
m1_group_6(sK34,sK31,sK35),
inference(cnf_transformation,[],[f16311]) ).
fof(f17065,plain,
u1_struct_0(sK37) = k2_funct_2(u1_struct_0(sK31),u1_struct_0(sK32),sK33,u1_struct_0(sK35)),
inference(cnf_transformation,[],[f16311]) ).
fof(f17066,plain,
u1_struct_0(sK36) = k2_funct_2(u1_struct_0(sK31),u1_struct_0(sK32),sK33,u1_struct_0(sK34)),
inference(cnf_transformation,[],[f16311]) ).
fof(f17067,plain,
~ m1_group_6(sK36,sK32,sK37),
inference(cnf_transformation,[],[f16311]) ).
fof(f17079,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k9_relat_1(X2,X3) = k2_funct_2(X0,X1,X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f14048]) ).
fof(f17097,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,[],[f14068]) ).
fof(f17121,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,[],[f16323]) ).
fof(f17122,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,[],[f16323]) ).
fof(f17124,plain,
! [X2,X0,X1] :
( ~ m1_group_6(X2,X0,X1)
| m1_group_2(X2,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f14096]) ).
fof(f17423,plain,
! [X2,X0,X1] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f14329]) ).
fof(f17456,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f16410]) ).
fof(f17636,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14515]) ).
fof(f17774,plain,
! [X2,X3,X0,X1] :
( r1_tarski(k12_group_2(X0,X2,X1),k12_group_2(X0,X3,X1))
| ~ m1_group_2(X2,X3)
| ~ m1_group_2(X3,X0)
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14618]) ).
fof(f17793,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| k7_group_2(X0,X1) = k12_group_2(X0,X1,k2_group_1(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14642]) ).
fof(f18193,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,[],[f14918]) ).
fof(f18194,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f14919]) ).
fof(f19003,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| u1_struct_0(X1) = k7_group_2(X0,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f15453]) ).
fof(f21337,definition,
( spl486_15
<=> m1_relset_1(sK33,u1_struct_0(sK31),u1_struct_0(sK32)) ),
introduced(definition,[new_symbols(definition,[spl486_15])],[avatar_definition]) ).
fof(f21338,plain,
( m1_relset_1(sK33,u1_struct_0(sK31),u1_struct_0(sK32))
| ~ spl486_15 ),
inference(avatar_component_clause,[],[f21337]) ).
fof(f21339,plain,
( ~ m1_relset_1(sK33,u1_struct_0(sK31),u1_struct_0(sK32))
| spl486_15 ),
inference(avatar_component_clause,[],[f21337]) ).
fof(f21350,plain,
( ~ m1_group_2(sK36,sK37)
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_group_2(sK37,sK32) ),
inference(resolution,[],[f17122,f17067]) ).
fof(f21351,plain,
( ~ m1_group_2(sK36,sK37)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_group_2(sK37,sK32) ),
inference(forward_subsumption_resolution,[],[f21350,f17055]) ).
fof(f21352,plain,
( ~ m1_group_2(sK36,sK37)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_group_2(sK37,sK32) ),
inference(forward_subsumption_resolution,[],[f21351,f17054]) ).
fof(f21353,plain,
( ~ m1_group_2(sK36,sK37)
| ~ l1_group_1(sK32)
| ~ m1_group_2(sK37,sK32) ),
inference(forward_subsumption_resolution,[],[f21352,f17053]) ).
fof(f21354,plain,
( ~ m1_group_2(sK36,sK37)
| ~ m1_group_2(sK37,sK32) ),
inference(forward_subsumption_resolution,[],[f21353,f17052]) ).
fof(f21355,plain,
~ m1_group_2(sK36,sK37),
inference(forward_subsumption_resolution,[],[f21354,f17063]) ).
fof(f21356,plain,
! [X0] :
( ~ v1_funct_1(sK33)
| k9_relat_1(sK33,X0) = k2_funct_2(u1_struct_0(sK31),u1_struct_0(sK32),sK33,X0)
| ~ m1_relset_1(sK33,u1_struct_0(sK31),u1_struct_0(sK32)) ),
inference(resolution,[],[f17079,f17058]) ).
fof(f21359,plain,
( u1_struct_0(sK34) = k7_group_2(sK31,sK34)
| v3_struct_0(sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(resolution,[],[f19003,f17060]) ).
fof(f21360,plain,
( u1_struct_0(sK35) = k7_group_2(sK31,sK35)
| v3_struct_0(sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(resolution,[],[f19003,f17061]) ).
fof(f21361,plain,
( u1_struct_0(sK35) = k7_group_2(sK31,sK35)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21360,f17051]) ).
fof(f21362,plain,
( u1_struct_0(sK34) = k7_group_2(sK31,sK34)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21359,f17051]) ).
fof(f21365,plain,
( u1_struct_0(sK35) = k7_group_2(sK31,sK35)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21361,f17050]) ).
fof(f21366,plain,
( u1_struct_0(sK34) = k7_group_2(sK31,sK34)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21362,f17050]) ).
fof(f21369,plain,
( u1_struct_0(sK35) = k7_group_2(sK31,sK35)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21365,f17049]) ).
fof(f21370,plain,
( u1_struct_0(sK34) = k7_group_2(sK31,sK34)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21366,f17049]) ).
fof(f21373,plain,
u1_struct_0(sK35) = k7_group_2(sK31,sK35),
inference(forward_subsumption_resolution,[],[f21369,f17048]) ).
fof(f21374,plain,
u1_struct_0(sK34) = k7_group_2(sK31,sK34),
inference(forward_subsumption_resolution,[],[f21370,f17048]) ).
fof(f21377,plain,
( m1_group_2(sK34,sK35)
| v3_struct_0(sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31)
| ~ m1_group_2(sK35,sK31) ),
inference(resolution,[],[f17121,f17064]) ).
fof(f21380,plain,
( m1_group_2(sK34,sK35)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31)
| ~ m1_group_2(sK35,sK31) ),
inference(forward_subsumption_resolution,[],[f21377,f17051]) ).
fof(f21381,plain,
( m1_group_2(sK34,sK35)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31)
| ~ m1_group_2(sK35,sK31) ),
inference(forward_subsumption_resolution,[],[f21380,f17050]) ).
fof(f21382,plain,
( m1_group_2(sK34,sK35)
| ~ l1_group_1(sK31)
| ~ m1_group_2(sK35,sK31) ),
inference(forward_subsumption_resolution,[],[f21381,f17049]) ).
fof(f21383,plain,
( m1_group_2(sK34,sK35)
| ~ m1_group_2(sK35,sK31) ),
inference(forward_subsumption_resolution,[],[f21382,f17048]) ).
fof(f21384,plain,
m1_group_2(sK34,sK35),
inference(forward_subsumption_resolution,[],[f21383,f17061]) ).
fof(f21407,plain,
m1_relset_1(sK33,u1_struct_0(sK31),u1_struct_0(sK32)),
inference(resolution,[],[f17456,f17056]) ).
fof(f21408,plain,
( $false
| spl486_15 ),
inference(forward_subsumption_resolution,[],[f21407,f21339]) ).
fof(f21409,plain,
spl486_15,
inference(avatar_contradiction_clause,[],[f21408]) ).
fof(f21410,plain,
! [X0] :
( k9_relat_1(sK33,X0) = k2_funct_2(u1_struct_0(sK31),u1_struct_0(sK32),sK33,X0)
| ~ m1_relset_1(sK33,u1_struct_0(sK31),u1_struct_0(sK32)) ),
inference(forward_subsumption_resolution,[],[f21356,f17059]) ).
fof(f21411,plain,
( ! [X0] : k9_relat_1(sK33,X0) = k2_funct_2(u1_struct_0(sK31),u1_struct_0(sK32),sK33,X0)
| ~ spl486_15 ),
inference(forward_subsumption_resolution,[],[f21410,f21338]) ).
fof(f21414,plain,
( u1_struct_0(sK37) = k9_relat_1(sK33,u1_struct_0(sK35))
| ~ spl486_15 ),
inference(superposition,[],[f17065,f21411]) ).
fof(f21415,plain,
( u1_struct_0(sK36) = k9_relat_1(sK33,u1_struct_0(sK34))
| ~ spl486_15 ),
inference(superposition,[],[f17066,f21411]) ).
fof(f21443,plain,
! [X2,X0,X1] :
( m1_group_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X0,X2)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X2,X1) ),
inference(resolution,[],[f17124,f17122]) ).
fof(f21444,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X2,X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| m1_group_2(X0,X1)
| ~ m1_group_2(X0,X2) ),
inference(duplicate_literal_removal,[],[f21443]) ).
fof(f21692,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f18194,f18193]) ).
fof(f21694,plain,
v1_relat_1(sK33),
inference(resolution,[],[f21692,f17056]) ).
fof(f21706,plain,
( k7_group_2(sK31,sK34) = k12_group_2(sK31,sK34,k2_group_1(sK31))
| v3_struct_0(sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(resolution,[],[f17793,f17060]) ).
fof(f21707,plain,
( k7_group_2(sK31,sK35) = k12_group_2(sK31,sK35,k2_group_1(sK31))
| v3_struct_0(sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(resolution,[],[f17793,f17061]) ).
fof(f21709,plain,
( k7_group_2(sK31,sK35) = k12_group_2(sK31,sK35,k2_group_1(sK31))
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21707,f17051]) ).
fof(f21710,plain,
( k7_group_2(sK31,sK34) = k12_group_2(sK31,sK34,k2_group_1(sK31))
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21706,f17051]) ).
fof(f21713,plain,
( k7_group_2(sK31,sK35) = k12_group_2(sK31,sK35,k2_group_1(sK31))
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21709,f17050]) ).
fof(f21714,plain,
( k7_group_2(sK31,sK34) = k12_group_2(sK31,sK34,k2_group_1(sK31))
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21710,f17050]) ).
fof(f21717,plain,
( k7_group_2(sK31,sK35) = k12_group_2(sK31,sK35,k2_group_1(sK31))
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21713,f17049]) ).
fof(f21718,plain,
( k7_group_2(sK31,sK34) = k12_group_2(sK31,sK34,k2_group_1(sK31))
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f21714,f17049]) ).
fof(f21721,plain,
k7_group_2(sK31,sK35) = k12_group_2(sK31,sK35,k2_group_1(sK31)),
inference(forward_subsumption_resolution,[],[f21717,f17048]) ).
fof(f21722,plain,
k7_group_2(sK31,sK34) = k12_group_2(sK31,sK34,k2_group_1(sK31)),
inference(forward_subsumption_resolution,[],[f21718,f17048]) ).
fof(f21725,plain,
u1_struct_0(sK35) = k12_group_2(sK31,sK35,k2_group_1(sK31)),
inference(forward_demodulation,[],[f21721,f21373]) ).
fof(f21726,plain,
u1_struct_0(sK34) = k12_group_2(sK31,sK34,k2_group_1(sK31)),
inference(forward_demodulation,[],[f21722,f21374]) ).
fof(f21982,plain,
( ! [X0] :
( r1_tarski(k9_relat_1(sK33,X0),u1_struct_0(sK37))
| ~ r1_tarski(X0,u1_struct_0(sK35))
| ~ v1_relat_1(sK33) )
| ~ spl486_15 ),
inference(superposition,[],[f17423,f21414]) ).
fof(f21984,plain,
( ! [X0] :
( r1_tarski(k9_relat_1(sK33,X0),u1_struct_0(sK37))
| ~ r1_tarski(X0,u1_struct_0(sK35)) )
| ~ spl486_15 ),
inference(forward_subsumption_resolution,[],[f21982,f21694]) ).
fof(f22010,plain,
( r1_tarski(u1_struct_0(sK36),u1_struct_0(sK37))
| ~ r1_tarski(u1_struct_0(sK34),u1_struct_0(sK35))
| ~ spl486_15 ),
inference(superposition,[],[f21984,f21415]) ).
fof(f22023,definition,
( spl486_54
<=> r1_tarski(u1_struct_0(sK34),u1_struct_0(sK35)) ),
introduced(definition,[new_symbols(definition,[spl486_54])],[avatar_definition]) ).
fof(f22025,plain,
( ~ r1_tarski(u1_struct_0(sK34),u1_struct_0(sK35))
| spl486_54 ),
inference(avatar_component_clause,[],[f22023]) ).
fof(f22027,definition,
( spl486_55
<=> r1_tarski(u1_struct_0(sK36),u1_struct_0(sK37)) ),
introduced(definition,[new_symbols(definition,[spl486_55])],[avatar_definition]) ).
fof(f22029,plain,
( r1_tarski(u1_struct_0(sK36),u1_struct_0(sK37))
| ~ spl486_55 ),
inference(avatar_component_clause,[],[f22027]) ).
fof(f22030,plain,
( ~ spl486_54
| spl486_55
| ~ spl486_15 ),
inference(avatar_split_clause,[],[f22010,f21337,f22027,f22023]) ).
fof(f23998,plain,
! [X0] :
( r1_tarski(u1_struct_0(sK34),k12_group_2(sK31,X0,k2_group_1(sK31)))
| ~ m1_group_2(sK34,X0)
| ~ m1_group_2(X0,sK31)
| ~ m1_group_2(sK34,sK31)
| ~ m1_subset_1(k2_group_1(sK31),u1_struct_0(sK31))
| v3_struct_0(sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(superposition,[],[f17774,f21726]) ).
fof(f24024,plain,
! [X0] :
( r1_tarski(u1_struct_0(sK34),k12_group_2(sK31,X0,k2_group_1(sK31)))
| ~ m1_group_2(sK34,X0)
| ~ m1_group_2(X0,sK31)
| ~ m1_subset_1(k2_group_1(sK31),u1_struct_0(sK31))
| v3_struct_0(sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f23998,f21444]) ).
fof(f24039,plain,
! [X0] :
( r1_tarski(u1_struct_0(sK34),k12_group_2(sK31,X0,k2_group_1(sK31)))
| ~ m1_group_2(sK34,X0)
| ~ m1_group_2(X0,sK31)
| v3_struct_0(sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f24024,f17636]) ).
fof(f24053,plain,
! [X0] :
( r1_tarski(u1_struct_0(sK34),k12_group_2(sK31,X0,k2_group_1(sK31)))
| ~ m1_group_2(sK34,X0)
| ~ m1_group_2(X0,sK31)
| ~ v3_group_1(sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f24039,f17051]) ).
fof(f24067,plain,
! [X0] :
( r1_tarski(u1_struct_0(sK34),k12_group_2(sK31,X0,k2_group_1(sK31)))
| ~ m1_group_2(sK34,X0)
| ~ m1_group_2(X0,sK31)
| ~ v4_group_1(sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f24053,f17050]) ).
fof(f24081,plain,
! [X0] :
( r1_tarski(u1_struct_0(sK34),k12_group_2(sK31,X0,k2_group_1(sK31)))
| ~ m1_group_2(sK34,X0)
| ~ m1_group_2(X0,sK31)
| ~ l1_group_1(sK31) ),
inference(forward_subsumption_resolution,[],[f24067,f17049]) ).
fof(f24095,plain,
! [X0] :
( r1_tarski(u1_struct_0(sK34),k12_group_2(sK31,X0,k2_group_1(sK31)))
| ~ m1_group_2(sK34,X0)
| ~ m1_group_2(X0,sK31) ),
inference(forward_subsumption_resolution,[],[f24081,f17048]) ).
fof(f24111,plain,
( r1_tarski(u1_struct_0(sK34),u1_struct_0(sK35))
| ~ m1_group_2(sK34,sK35)
| ~ m1_group_2(sK35,sK31) ),
inference(superposition,[],[f24095,f21725]) ).
fof(f24113,plain,
( ~ m1_group_2(sK34,sK35)
| ~ m1_group_2(sK35,sK31)
| spl486_54 ),
inference(forward_subsumption_resolution,[],[f24111,f22025]) ).
fof(f24114,plain,
( ~ m1_group_2(sK35,sK31)
| spl486_54 ),
inference(forward_subsumption_resolution,[],[f24113,f21384]) ).
fof(f24115,plain,
( $false
| spl486_54 ),
inference(forward_subsumption_resolution,[],[f24114,f17061]) ).
fof(f24116,plain,
spl486_54,
inference(avatar_contradiction_clause,[],[f24115]) ).
fof(f24119,plain,
( ! [X0] :
( m1_group_2(sK36,sK37)
| ~ m1_group_2(sK37,X0)
| ~ m1_group_2(sK36,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl486_55 ),
inference(resolution,[],[f22029,f17097]) ).
fof(f24126,plain,
( ! [X0] :
( ~ m1_group_2(sK37,X0)
| ~ m1_group_2(sK36,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl486_55 ),
inference(forward_subsumption_resolution,[],[f24119,f21355]) ).
fof(f24130,plain,
( ~ m1_group_2(sK36,sK32)
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ spl486_55 ),
inference(resolution,[],[f24126,f17063]) ).
fof(f24133,plain,
( v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ spl486_55 ),
inference(forward_subsumption_resolution,[],[f24130,f17062]) ).
fof(f24136,plain,
( ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ spl486_55 ),
inference(forward_subsumption_resolution,[],[f24133,f17055]) ).
fof(f24137,plain,
( ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ spl486_55 ),
inference(forward_subsumption_resolution,[],[f24136,f17054]) ).
fof(f24138,plain,
( ~ l1_group_1(sK32)
| ~ spl486_55 ),
inference(forward_subsumption_resolution,[],[f24137,f17053]) ).
fof(f24139,plain,
( $false
| ~ spl486_55 ),
inference(forward_subsumption_resolution,[],[f24138,f17052]) ).
fof(f24140,plain,
~ spl486_55,
inference(avatar_contradiction_clause,[],[f24139]) ).
cnf(s21,plain,
spl486_15,
inference(sat_conversion,[],[f21409]) ).
cnf(s43,plain,
( ~ spl486_15
| ~ spl486_54
| spl486_55 ),
inference(sat_conversion,[],[f22030]) ).
cnf(s124,plain,
spl486_54,
inference(sat_conversion,[],[f24116]) ).
cnf(s126,plain,
~ spl486_55,
inference(sat_conversion,[],[f24140]) ).
cnf(s130,plain,
~ spl486_15,
inference(rat,[],[s43,s126,s124]) ).
cnf(s133,plain,
$false,
inference(rat,[],[s21,s130]) ).
fof(f24141,plain,
$false,
inference(avatar_sat_refutation,[],[s133]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP637+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.22/0.49 % Computer : n009.cluster.edu
% 0.22/0.49 % Model : x86_64 x86_64
% 0.22/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.49 % Memory : 8046.5625MB
% 0.22/0.49 % OS : Linux 6.8.0-71-generic
% 0.22/0.49 % CPULimit : 300
% 0.22/0.49 % WCLimit : 300
% 0.22/0.49 % DateTime : Sun Sep 27 10:20:18 UTC 2026
% 0.22/0.49 % CPUTime :
% 0.22/0.49 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.54 Running first-order theorem proving
% 0.27/0.54 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.74/3.60 % (1818288)Detected formulas, will run a generic FOF schedule.
% 13.74/3.60 % (1818298)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3687424137:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 13.74/3.60 % (1818298)Instruction limit reached!
% 13.74/3.60 % (1818298)------------------------------
% 13.74/3.60 % (1818298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.74/3.60 % (1818298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.74/3.60 % (1818298)CaDiCaL version: 2.1.3
% 13.74/3.60 % (1818298)Termination reason: Instruction limit
% 13.74/3.60 % (1818298)Termination phase: Property scanning
% 13.74/3.60 % (1818298)Time elapsed: 0.033 s
% 13.74/3.60 % (1818298)Peak memory usage: 103 MB
% 13.74/3.60 % (1818298)Instructions burned: 140 (million)
% 13.74/3.60 % (1818294)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=2575129059:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 13.74/3.60 % (1818296)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1447425846:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 13.74/3.60 % (1818301)lrs+10_1_sil=8000:sp=occurrence:random_seed=2844770924:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 13.74/3.60 % (1818293)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=680635673:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 13.74/3.60 % (1818295)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=2826572992:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 13.74/3.60 % (1818297)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1082385193:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 13.74/3.60 % (1818299)dis-21_1_sil=8000:lcm=predicate:random_seed=2358966410:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 13.74/3.60 % (1818296)Instruction limit reached!
% 13.74/3.60 % (1818296)------------------------------
% 13.74/3.60 % (1818296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.74/3.60 % (1818296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.74/3.60 % (1818296)CaDiCaL version: 2.1.3
% 13.74/3.60 % (1818296)Termination reason: Instruction limit
% 13.74/3.60 % (1818296)Termination phase: Saturation
% 13.74/3.60 % (1818296)Time elapsed: 0.126 s
% 13.74/3.60 % (1818296)Peak memory usage: 107 MB
% 13.74/3.60 % (1818296)Instructions burned: 110 (million)
% 13.74/3.60 % (1818301)Instruction limit reached!
% 13.74/3.60 % (1818301)------------------------------
% 13.74/3.60 % (1818301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.74/3.60 % (1818301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.74/3.60 % (1818301)CaDiCaL version: 2.1.3
% 13.74/3.60 % (1818301)Termination reason: Instruction limit
% 13.74/3.60 % (1818301)Termination phase: Saturation
% 13.74/3.60 % (1818301)Time elapsed: 0.108 s
% 13.74/3.60 % (1818301)Peak memory usage: 111 MB
% 13.74/3.60 % (1818301)Instructions burned: 286 (million)
% 13.74/3.60 % (1818299)Instruction limit reached!
% 13.74/3.60 % (1818299)------------------------------
% 13.74/3.60 % (1818299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.74/3.60 % (1818299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.74/3.60 % (1818299)CaDiCaL version: 2.1.3
% 13.74/3.60 % (1818299)Termination reason: Instruction limit
% 13.74/3.60 % (1818299)Termination phase: Preprocessing 1
% 13.74/3.60 % (1818299)Time elapsed: 0.140 s
% 13.74/3.60 % (1818299)Peak memory usage: 104 MB
% 13.74/3.60 % (1818299)Instructions burned: 129 (million)
% 13.74/3.60 % (1818297)Instruction limit reached!
% 13.74/3.60 % (1818297)------------------------------
% 13.74/3.60 % (1818297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.74/3.60 % (1818297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.74/3.60 % (1818297)CaDiCaL version: 2.1.3
% 13.74/3.60 % (1818297)Termination reason: Instruction limit
% 13.74/3.60 % (1818297)Termination phase: Preprocessing 3
% 13.74/3.60 % (1818297)Time elapsed: 0.145 s
% 13.74/3.60 % (1818297)Peak memory usage: 106 MB
% 13.74/3.60 % (1818297)Instructions burned: 119 (million)
% 19.18/4.35 % (1818310)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2576007453:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi)
% 19.18/4.35 % (1818309)lrs+10_1_sil=32000:urr=on:br=off:random_seed=165834614:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 19.18/4.35 % (1818310)Instruction limit reached!
% 19.18/4.35 % (1818310)------------------------------
% 19.18/4.35 % (1818310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.18/4.35 % (1818310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.18/4.35 % (1818310)CaDiCaL version: 2.1.3
% 19.18/4.35 % (1818310)Termination reason: Instruction limit
% 19.18/4.35 % (1818310)Termination phase: Saturation
% 19.18/4.35 % (1818310)Time elapsed: 0.122 s
% 19.18/4.35 % (1818310)Peak memory usage: 110 MB
% 19.18/4.35 % (1818310)Instructions burned: 326 (million)
% 19.18/4.35 % (1818311)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=3419083911:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 19.18/4.35 % (1818312)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2355684122:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 19.18/4.35 % (1818309)Instruction limit reached!
% 19.18/4.35 % (1818309)------------------------------
% 19.18/4.35 % (1818309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.18/4.35 % (1818309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.18/4.35 % (1818309)CaDiCaL version: 2.1.3
% 19.18/4.35 % (1818309)Termination reason: Instruction limit
% 19.18/4.35 % (1818309)Termination phase: Property scanning
% 19.18/4.35 % (1818309)Time elapsed: 0.132 s
% 19.18/4.35 % (1818309)Peak memory usage: 103 MB
% 19.18/4.35 % (1818309)Instructions burned: 157 (million)
% 19.18/4.35 % (1818315)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2235386773:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 19.18/4.35 % (1818311)Instruction limit reached!
% 19.18/4.35 % (1818311)------------------------------
% 19.18/4.35 % (1818311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.18/4.35 % (1818311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.18/4.35 % (1818311)CaDiCaL version: 2.1.3
% 19.18/4.35 % (1818311)Termination reason: Instruction limit
% 19.18/4.35 % (1818311)Termination phase: SInE selection
% 19.18/4.35 % (1818311)Time elapsed: 0.125 s
% 19.18/4.35 % (1818311)Peak memory usage: 103 MB
% 19.18/4.35 % (1818311)Instructions burned: 249 (million)
% 19.18/4.35 % (1818312)Instruction limit reached!
% 19.18/4.35 % (1818312)------------------------------
% 19.18/4.35 % (1818312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.18/4.35 % (1818312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.18/4.35 % (1818312)CaDiCaL version: 2.1.3
% 19.18/4.35 % (1818312)Termination reason: Instruction limit
% 19.18/4.35 % (1818312)Termination phase: Saturation
% 19.18/4.35 % (1818312)Time elapsed: 0.189 s
% 19.18/4.35 % (1818312)Peak memory usage: 110 MB
% 19.18/4.35 % (1818312)Instructions burned: 295 (million)
% 19.18/4.35 % (1818318)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2867282049:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 19.18/4.35 % (1818320)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3293646483:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 19.18/4.35 % (1818318)Instruction limit reached!
% 19.18/4.35 % (1818318)------------------------------
% 19.18/4.35 % (1818318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.18/4.35 % (1818318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.18/4.35 % (1818318)CaDiCaL version: 2.1.3
% 19.18/4.35 % (1818318)Termination reason: Instruction limit
% 19.18/4.35 % (1818318)Termination phase: Preprocessing 2
% 19.18/4.35 % (1818318)Time elapsed: 0.099 s
% 19.18/4.35 % (1818318)Peak memory usage: 106 MB
% 19.18/4.35 % (1818318)Instructions burned: 113 (million)
% 19.18/4.35 % (1818321)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=483580118:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 19.18/4.35 % (1818320)Instruction limit reached!
% 19.18/4.35 % (1818320)------------------------------
% 19.18/4.35 % (1818320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.96/9.66 % (1818320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/9.66 % (1818320)CaDiCaL version: 2.1.3
% 56.96/9.66 % (1818320)Termination reason: Instruction limit
% 56.96/9.66 % (1818320)Termination phase: Preprocessing 2
% 56.96/9.66 % (1818320)Time elapsed: 0.100 s
% 56.96/9.66 % (1818320)Peak memory usage: 106 MB
% 56.96/9.66 % (1818320)Instructions burned: 127 (million)
% 56.96/9.66 % (1818321)Instruction limit reached!
% 56.96/9.66 % (1818321)------------------------------
% 56.96/9.66 % (1818321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.96/9.66 % (1818321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/9.66 % (1818321)CaDiCaL version: 2.1.3
% 56.96/9.66 % (1818321)Termination reason: Instruction limit
% 56.96/9.66 % (1818321)Termination phase: Property scanning
% 56.96/9.66 % (1818321)Time elapsed: 0.051 s
% 56.96/9.66 % (1818321)Peak memory usage: 103 MB
% 56.96/9.66 % (1818321)Instructions burned: 116 (million)
% 56.96/9.66 % (1818324)lrs+10_1_sil=8000:sp=occurrence:random_seed=621841655:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 56.96/9.66 % (1818326)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3285725705:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 56.96/9.66 % (1818327)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2581191640:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 56.96/9.66 % (1818326)Instruction limit reached!
% 56.96/9.66 % (1818326)------------------------------
% 56.96/9.66 % (1818326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.96/9.66 % (1818326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/9.66 % (1818326)CaDiCaL version: 2.1.3
% 56.96/9.66 % (1818326)Termination reason: Instruction limit
% 56.96/9.66 % (1818326)Termination phase: Saturation
% 56.96/9.66 % (1818326)Time elapsed: 0.269 s
% 56.96/9.66 % (1818326)Peak memory usage: 111 MB
% 56.96/9.66 % (1818326)Instructions burned: 438 (million)
% 56.96/9.66 % (1818315)Instruction limit reached!
% 56.96/9.66 % (1818315)------------------------------
% 56.96/9.66 % (1818315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.96/9.66 % (1818315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/9.66 % (1818315)CaDiCaL version: 2.1.3
% 56.96/9.66 % (1818315)Termination reason: Instruction limit
% 56.96/9.66 % (1818315)Termination phase: Saturation
% 56.96/9.66 % (1818315)Time elapsed: 0.802 s
% 56.96/9.66 % (1818315)Peak memory usage: 228 MB
% 56.96/9.66 % (1818315)Instructions burned: 2350 (million)
% 56.96/9.66 % (1818331)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2167780013:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 56.96/9.66 % (1818324)Instruction limit reached!
% 56.96/9.66 % (1818324)------------------------------
% 56.96/9.66 % (1818324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.96/9.66 % (1818324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/9.66 % (1818324)CaDiCaL version: 2.1.3
% 56.96/9.66 % (1818324)Termination reason: Instruction limit
% 56.96/9.66 % (1818324)Termination phase: Saturation
% 56.96/9.66 % (1818324)Time elapsed: 0.538 s
% 56.96/9.66 % (1818324)Peak memory usage: 122 MB
% 56.96/9.66 % (1818324)Instructions burned: 908 (million)
% 56.96/9.66 % (1818332)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2307230564:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 56.96/9.66 % (1818331)Instruction limit reached!
% 56.96/9.66 % (1818331)------------------------------
% 56.96/9.66 % (1818331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.96/9.66 % (1818331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/9.66 % (1818331)CaDiCaL version: 2.1.3
% 56.96/9.66 % (1818331)Termination reason: Instruction limit
% 56.96/9.66 % (1818331)Termination phase: Property scanning
% 56.96/9.66 % (1818331)Time elapsed: 0.104 s
% 56.96/9.66 % (1818331)Peak memory usage: 107 MB
% 56.96/9.66 % (1818331)Instructions burned: 136 (million)
% 56.96/9.66 % (1818335)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4072453932:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 56.96/9.66 % (1818336)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=722031520:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 76.09/12.38 % (1818336)Instruction limit reached!
% 76.09/12.38 % (1818336)------------------------------
% 76.09/12.38 % (1818336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.09/12.38 % (1818336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.09/12.38 % (1818336)CaDiCaL version: 2.1.3
% 76.09/12.38 % (1818336)Termination reason: Instruction limit
% 76.09/12.38 % (1818336)Termination phase: Property scanning
% 76.09/12.38 % (1818336)Time elapsed: 0.054 s
% 76.09/12.38 % (1818336)Peak memory usage: 103 MB
% 76.09/12.38 % (1818336)Instructions burned: 128 (million)
% 76.09/12.38 % (1818332)Instruction limit reached!
% 76.09/12.38 % (1818332)------------------------------
% 76.09/12.38 % (1818332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.09/12.38 % (1818332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.09/12.38 % (1818332)CaDiCaL version: 2.1.3
% 76.09/12.38 % (1818332)Termination reason: Instruction limit
% 76.09/12.38 % (1818332)Termination phase: Property scanning
% 76.09/12.38 % (1818332)Time elapsed: 0.254 s
% 76.09/12.38 % (1818332)Peak memory usage: 126 MB
% 76.09/12.38 % (1818332)Instructions burned: 595 (million)
% 76.09/12.38 % (1818340)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3831066061:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/141Mi)
% 76.09/12.38 % (1818339)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2782503190:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 76.09/12.38 % (1818339)Instruction limit reached!
% 76.09/12.38 % (1818339)------------------------------
% 76.09/12.38 % (1818339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.09/12.38 % (1818339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.09/12.38 % (1818339)CaDiCaL version: 2.1.3
% 76.09/12.38 % (1818339)Termination reason: Instruction limit
% 76.09/12.38 % (1818339)Termination phase: Property scanning
% 76.09/12.38 % (1818339)Time elapsed: 0.058 s
% 76.09/12.38 % (1818339)Peak memory usage: 103 MB
% 76.09/12.38 % (1818339)Instructions burned: 136 (million)
% 76.09/12.38 % (1818340)Instruction limit reached!
% 76.09/12.38 % (1818340)------------------------------
% 76.09/12.38 % (1818340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.09/12.38 % (1818340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.09/12.38 % (1818340)CaDiCaL version: 2.1.3
% 76.09/12.38 % (1818340)Termination reason: Instruction limit
% 76.09/12.38 % (1818340)Termination phase: Saturation
% 76.09/12.38 % (1818340)Time elapsed: 0.060 s
% 76.09/12.38 % (1818340)Peak memory usage: 108 MB
% 76.09/12.38 % (1818340)Instructions burned: 144 (million)
% 76.09/12.38 % (1818343)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3008273905:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 76.09/12.38 % (1818344)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=426129450:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 76.09/12.38 % (1818343)Instruction limit reached!
% 76.09/12.38 % (1818343)------------------------------
% 76.09/12.38 % (1818343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.09/12.38 % (1818343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.09/12.38 % (1818343)CaDiCaL version: 2.1.3
% 76.09/12.38 % (1818343)Termination reason: Instruction limit
% 76.09/12.38 % (1818343)Termination phase: Saturation
% 76.09/12.38 % (1818343)Time elapsed: 0.153 s
% 76.09/12.38 % (1818343)Peak memory usage: 113 MB
% 76.09/12.38 % (1818343)Instructions burned: 433 (million)
% 76.09/12.38 % (1818347)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=3611264762:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 76.09/12.38 % (1818347)Instruction limit reached!
% 76.09/12.38 % (1818347)------------------------------
% 76.09/12.38 % (1818347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.09/12.38 % (1818347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.09/12.38 % (1818347)CaDiCaL version: 2.1.3
% 76.09/12.38 % (1818347)Termination reason: Instruction limit
% 75.55/12.47 % (1818347)Termination phase: Preprocessing 1
% 75.55/12.47 % (1818347)Time elapsed: 0.065 s
% 75.55/12.47 % (1818347)Peak memory usage: 104 MB
% 75.55/12.47 % (1818347)Instructions burned: 151 (million)
% 75.55/12.47 % (1818349)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4137576305:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 75.55/12.47 % (1818327)Instruction limit reached!
% 75.55/12.47 % (1818327)------------------------------
% 75.55/12.47 % (1818327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818327)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818327)Termination reason: Instruction limit
% 75.55/12.47 % (1818327)Termination phase: Saturation
% 75.55/12.47 % (1818327)Time elapsed: 3.168 s
% 75.55/12.47 % (1818327)Peak memory usage: 190 MB
% 75.55/12.47 % (1818327)Instructions burned: 5204 (million)
% 75.55/12.47 % (1818351)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2932882401:i=667:av=off:fsr=off_2951 on theBenchmark for (2951ds/667Mi)
% 75.55/12.47 % (1818351)Instruction limit reached!
% 75.55/12.47 % (1818351)------------------------------
% 75.55/12.47 % (1818351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818351)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818351)Termination reason: Instruction limit
% 75.55/12.47 % (1818351)Termination phase: NewCNF
% 75.55/12.47 % (1818351)Time elapsed: 0.494 s
% 75.55/12.47 % (1818351)Peak memory usage: 136 MB
% 75.55/12.47 % (1818351)Instructions burned: 667 (million)
% 75.55/12.47 % (1818353)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3134409370:s2a=on:i=185:s2at=1.8:fdi=4_2944 on theBenchmark for (2944ds/185Mi)
% 75.55/12.47 % (1818353)Instruction limit reached!
% 75.55/12.47 % (1818353)------------------------------
% 75.55/12.47 % (1818353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818353)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818353)Termination reason: Instruction limit
% 75.55/12.47 % (1818353)Termination phase: Preprocessing 1
% 75.55/12.47 % (1818353)Time elapsed: 0.150 s
% 75.55/12.47 % (1818353)Peak memory usage: 104 MB
% 75.55/12.47 % (1818353)Instructions burned: 185 (million)
% 75.55/12.47 % (1818355)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2020336155:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2941 on theBenchmark for (2941ds/193Mi)
% 75.55/12.47 % (1818355)Instruction limit reached!
% 75.55/12.47 % (1818355)------------------------------
% 75.55/12.47 % (1818355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818355)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818355)Termination reason: Instruction limit
% 75.55/12.47 % (1818355)Termination phase: Preprocessing 3
% 75.55/12.47 % (1818355)Time elapsed: 0.162 s
% 75.55/12.47 % (1818355)Peak memory usage: 106 MB
% 75.55/12.47 % (1818355)Instructions burned: 193 (million)
% 75.55/12.47 % (1818357)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=305146671:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2937 on theBenchmark for (2937ds/4850Mi)
% 75.55/12.47 % (1818344)Instruction limit reached!
% 75.55/12.47 % (1818344)------------------------------
% 75.55/12.47 % (1818344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818344)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818344)Termination reason: Instruction limit
% 75.55/12.47 % (1818344)Termination phase: Saturation
% 75.55/12.47 % (1818344)Time elapsed: 4.629 s
% 75.55/12.47 % (1818344)Peak memory usage: 526 MB
% 75.55/12.47 % (1818344)Instructions burned: 6062 (million)
% 75.55/12.47 % (1818359)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=836099106:i=12111:sd=1:ss=included_2925 on theBenchmark for (2925ds/12111Mi)
% 75.55/12.47 % (1818349)Instruction limit reached!
% 75.55/12.47 % (1818349)------------------------------
% 75.55/12.47 % (1818349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818349)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818349)Termination reason: Instruction limit
% 75.55/12.47 % (1818349)Termination phase: Saturation
% 75.55/12.47 % (1818349)Time elapsed: 5.170 s
% 75.55/12.47 % (1818349)Peak memory usage: 511 MB
% 75.55/12.47 % (1818349)Instructions burned: 14159 (million)
% 75.55/12.47 % (1818362)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2167164842:i=319:kws=precedence:fsr=off_2915 on theBenchmark for (2915ds/319Mi)
% 75.55/12.47 % (1818362)Instruction limit reached!
% 75.55/12.47 % (1818362)------------------------------
% 75.55/12.47 % (1818362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818362)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818362)Termination reason: Instruction limit
% 75.55/12.47 % (1818362)Termination phase: Preprocessing 3
% 75.55/12.47 % (1818362)Time elapsed: 0.133 s
% 75.55/12.47 % (1818362)Peak memory usage: 123 MB
% 75.55/12.47 % (1818362)Instructions burned: 319 (million)
% 75.55/12.47 % (1818364)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2195549623:i=2064:ep=RST_2912 on theBenchmark for (2912ds/2064Mi)
% 75.55/12.47 % (1818357)Instruction limit reached!
% 75.55/12.47 % (1818357)------------------------------
% 75.55/12.47 % (1818357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818357)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818357)Termination reason: Instruction limit
% 75.55/12.47 % (1818357)Termination phase: Saturation
% 75.55/12.47 % (1818357)Time elapsed: 2.609 s
% 75.55/12.47 % (1818357)Peak memory usage: 177 MB
% 75.55/12.47 % (1818357)Instructions burned: 4851 (million)
% 75.55/12.47 % (1818366)dis-1011_128_sil=32000:random_seed=218539402:i=3706:ep=RST:av=off_2909 on theBenchmark for (2909ds/3706Mi)
% 75.55/12.47 % (1818364)Instruction limit reached!
% 75.55/12.47 % (1818364)------------------------------
% 75.55/12.47 % (1818364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818364)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818364)Termination reason: Instruction limit
% 75.55/12.47 % (1818364)Termination phase: Saturation
% 75.55/12.47 % (1818364)Time elapsed: 0.564 s
% 75.55/12.47 % (1818364)Peak memory usage: 147 MB
% 75.55/12.47 % (1818364)Instructions burned: 2066 (million)
% 75.55/12.47 % (1818368)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2792574955:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2905 on theBenchmark for (2905ds/757Mi)
% 75.55/12.47 % (1818368)Instruction limit reached!
% 75.55/12.47 % (1818368)------------------------------
% 75.55/12.47 % (1818368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818368)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818368)Termination reason: Instruction limit
% 75.55/12.47 % (1818368)Termination phase: Saturation
% 75.55/12.47 % (1818368)Time elapsed: 0.312 s
% 75.55/12.47 % (1818368)Peak memory usage: 114 MB
% 75.55/12.47 % (1818368)Instructions burned: 759 (million)
% 75.55/12.47 % (1818335)Instruction limit reached!
% 75.55/12.47 % (1818335)------------------------------
% 75.55/12.47 % (1818335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818335)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818335)Termination reason: Instruction limit
% 75.55/12.47 % (1818335)Termination phase: Saturation
% 75.55/12.47 % (1818335)Time elapsed: 7.653 s
% 75.55/12.47 % (1818335)Peak memory usage: 299 MB
% 75.55/12.47 % (1818335)Instructions burned: 13194 (million)
% 75.55/12.47 % (1818370)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3259928233:i=13913:ss=axioms:sgt=8_2901 on theBenchmark for (2901ds/13913Mi)
% 75.55/12.47 % (1818371)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1617680029:i=9925:aac=none_2899 on theBenchmark for (2899ds/9925Mi)
% 75.55/12.47 % (1818370)First to succeed.
% 75.55/12.47 % (1818370)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1818288"
% 75.55/12.47 % (1818366)Instruction limit reached!
% 75.55/12.47 % (1818366)------------------------------
% 75.55/12.47 % (1818366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.55/12.47 % (1818366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.55/12.47 % (1818366)CaDiCaL version: 2.1.3
% 75.55/12.47 % (1818366)Termination reason: Instruction limit
% 75.55/12.47 % (1818366)Termination phase: Saturation
% 75.55/12.47 % (1818366)Time elapsed: 1.963 s
% 75.55/12.47 % (1818366)Peak memory usage: 165 MB
% 75.55/12.47 % (1818366)Instructions burned: 3707 (million)
% 75.55/12.47 % (1818370)Refutation found. Thanks to Tanya!
% 75.55/12.47 % SZS status Theorem for theBenchmark
% 75.55/12.47 % SZS output start Proof for theBenchmark
% See solution above
% 77.22/12.68 % (1818370)------------------------------
% 77.22/12.68 % (1818370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.22/12.68 % (1818370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.22/12.68 % (1818370)CaDiCaL version: 2.1.3
% 77.22/12.68 % (1818370)Termination reason: Refutation
% 77.22/12.68 % (1818370)Time elapsed: 0.973 s
% 77.22/12.68 % (1818370)Peak memory usage: 189 MB
% 77.22/12.68 % (1818370)Instructions burned: 2774 (million)
% 77.22/12.68 % (1818370)------------------------------
% 77.22/12.68 % (1818370)------------------------------
% 77.22/12.68 % (1818288)Success in time 11.229 s
% 77.22/12.68 % Vampire exiting
%------------------------------------------------------------------------------