%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP650+2 : 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 : n003.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:18 AM UTC 2026
% Result : Theorem 33.94s 6.36s
% Output : Refutation 37.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 25
% Syntax : Number of formulae : 257 ( 24 unt; 4 def)
% Number of atoms : 1688 ( 223 equ)
% Maximal formula atoms : 26 ( 6 avg)
% Number of connectives : 2527 (1096 ~;1257 |; 128 &)
% ( 17 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 8 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 5 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 1 con; 0-4 aty)
% Number of variables : 344 ( 0 sgn 335 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f917,axiom,
! [X0] :
( v1_relat_1(k6_relat_1(X0))
& v1_funct_1(k6_relat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_funct_1) ).
fof(f966,axiom,
! [X0,X1] :
( r2_hidden(X1,X0)
=> k1_funct_1(k6_relat_1(X0),X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_funct_1) ).
fof(f1101,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> k9_relat_1(k6_relat_1(X0),X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t162_funct_1) ).
fof(f1287,axiom,
! [X0] : m2_relset_1(k6_relat_1(X0),X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_relset_1) ).
fof(f1318,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(f1559,axiom,
! [X0] :
( v1_partfun1(k6_partfun1(X0),X0,X0)
& m2_relset_1(k6_partfun1(X0),X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_partfun1) ).
fof(f1560,axiom,
! [X0] : k6_partfun1(X0) = k6_relat_1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_partfun1) ).
fof(f1691,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> ( ( v1_funct_1(X2)
& v1_partfun1(X2,X0,X1) )
=> ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_funct_2) ).
fof(f1890,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1) )
=> k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f3812,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(f4433,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/sandbox2/benchmark/theBenchmark.p',d9_group_2) ).
fof(f4485,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/sandbox2/benchmark/theBenchmark.p',t132_group_2) ).
fof(f4544,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& v1_group_1(X1)
& m1_group_2(X1,X0)
& v1_group_1(X2)
& m1_group_2(X2,X0) )
=> ( r1_group_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_group_2) ).
fof(f4558,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0)
& m1_subset_1(X2,u1_struct_0(X0)) )
=> m1_subset_1(k12_group_2(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k12_group_2) ).
fof(f4810,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_group_3) ).
fof(f5102,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> u1_struct_0(k11_group_4(X0)) = k1_group_3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t92_group_4) ).
fof(f5116,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( v1_group_1(k5_group_4(X0,X1))
& m1_group_2(k5_group_4(X0,X1),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_group_4) ).
fof(f5294,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t47_group_6) ).
fof(f5641,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X2] :
( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
=> ( X1 = u1_struct_0(X2)
=> r1_group_2(X0,k5_group_4(X0,X1),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_latsubgr) ).
fof(f5673,axiom,
! [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))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
& m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
=> ( X3 = k3_latsubgr(X0,X1,X2)
<=> ! [X4] :
( ( v1_group_1(X4)
& m1_group_2(X4,X0) )
=> ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
=> ( X5 = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
=> k1_funct_1(X3,X4) = k5_group_4(X1,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_latsubgr) ).
fof(f5674,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) = k6_partfun1(u1_struct_0(k11_group_4(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_latsubgr) ).
fof(f5675,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) = k6_partfun1(u1_struct_0(k11_group_4(X0))) ),
inference(negated_conjecture,[status(cth)],[f5674]) ).
fof(f5776,plain,
? [X0] :
( k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) != k6_partfun1(u1_struct_0(k11_group_4(X0)))
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f5675]) ).
fof(f5777,plain,
? [X0] :
( k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) != k6_partfun1(u1_struct_0(k11_group_4(X0)))
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f5776]) ).
fof(f5778,plain,
! [X0] :
( ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f5294]) ).
fof(f5779,plain,
! [X0] :
( ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f5778]) ).
fof(f5823,plain,
! [X0] :
( u1_struct_0(k11_group_4(X0)) = k1_group_3(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f5102]) ).
fof(f5824,plain,
! [X0] :
( u1_struct_0(k11_group_4(X0)) = k1_group_3(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f5823]) ).
fof(f5827,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k3_latsubgr(X0,X1,X2)
<=> ! [X4] :
( ! [X5] :
( k1_funct_1(X3,X4) = k5_group_4(X1,X5)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X4)
| ~ m1_group_2(X4,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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,[],[f5673]) ).
fof(f5828,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k3_latsubgr(X0,X1,X2)
<=> ! [X4] :
( ! [X5] :
( k1_funct_1(X3,X4) = k5_group_4(X1,X5)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X4)
| ~ m1_group_2(X4,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f5827]) ).
fof(f6107,plain,
! [X0,X1,X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_partfun1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1691]) ).
fof(f6108,plain,
! [X0,X1,X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_partfun1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f6107]) ).
fof(f6600,plain,
! [X0,X1] :
( k9_relat_1(k6_relat_1(X0),X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f1101]) ).
fof(f6601,plain,
! [X0,X1] :
( k1_funct_1(k6_relat_1(X0),X1) = X1
| ~ r2_hidden(X1,X0) ),
inference(ennf_transformation,[],[f966]) ).
fof(f6943,plain,
! [X0] :
( ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f4810]) ).
fof(f6944,plain,
! [X0] :
( ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f6943]) ).
fof(f7049,plain,
! [X0,X1,X2,X3] :
( k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1890]) ).
fof(f7050,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,[],[f7049]) ).
fof(f7073,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_group_2(X0,k5_group_4(X0,X1),X2)
| u1_struct_0(X2) != X1
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f5641]) ).
fof(f7074,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_group_2(X0,k5_group_4(X0,X1),X2)
| u1_struct_0(X2) != X1
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f7073]) ).
fof(f7075,plain,
! [X0,X1] :
( ( v1_group_1(k5_group_4(X0,X1))
& m1_group_2(k5_group_4(X0,X1),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f5116]) ).
fof(f7076,plain,
! [X0,X1] :
( ( v1_group_1(k5_group_4(X0,X1))
& m1_group_2(k5_group_4(X0,X1),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f7075]) ).
fof(f7446,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,[],[f4485]) ).
fof(f7447,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,[],[f7446]) ).
fof(f7460,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f3812]) ).
fof(f7461,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f7460]) ).
fof(f8678,plain,
! [X0,X1,X2] :
( m1_subset_1(k12_group_2(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f4558]) ).
fof(f8679,plain,
! [X0,X1,X2] :
( m1_subset_1(k12_group_2(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f8678]) ).
fof(f8748,plain,
! [X0,X1,X2] :
( ( r1_group_2(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(ennf_transformation,[],[f4544]) ).
fof(f8749,plain,
! [X0,X1,X2] :
( ( r1_group_2(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(flattening,[],[f8748]) ).
fof(f8957,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,[],[f4433]) ).
fof(f8958,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,[],[f8957]) ).
fof(f9483,plain,
( k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) != k6_partfun1(u1_struct_0(k11_group_4(sK52)))
& ~ v3_struct_0(sK52)
& v3_group_1(sK52)
& v4_group_1(sK52)
& l1_group_1(sK52) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(X0,sK52)],[f5777]) ).
fof(f9490,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k3_latsubgr(X0,X1,X2)
| ? [X4] :
( ? [X5] :
( k1_funct_1(X3,X4) != k5_group_4(X1,X5)
& k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) = X5
& m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
& v1_group_1(X4)
& m1_group_2(X4,X0) ) )
& ( ! [X4] :
( ! [X5] :
( k1_funct_1(X3,X4) = k5_group_4(X1,X5)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X4)
| ~ m1_group_2(X4,X0) )
| k3_latsubgr(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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(nnf_transformation,[],[f5828]) ).
fof(f9491,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k3_latsubgr(X0,X1,X2)
| ? [X4] :
( ? [X5] :
( k1_funct_1(X3,X4) != k5_group_4(X1,X5)
& k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) = X5
& m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
& v1_group_1(X4)
& m1_group_2(X4,X0) ) )
& ( ! [X6] :
( ! [X7] :
( k1_funct_1(X3,X6) = k5_group_4(X1,X7)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6)) != X7
| ~ m1_subset_1(X7,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X6)
| ~ m1_group_2(X6,X0) )
| k3_latsubgr(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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(rectify,[],[f9490]) ).
fof(f9492,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k3_latsubgr(X0,X1,X2)
| ( k1_funct_1(X3,sK55(X0,X1,X2,X3)) != k5_group_4(X1,sK56(X0,X1,X2,X3))
& sK56(X0,X1,X2,X3) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(sK55(X0,X1,X2,X3)))
& m1_subset_1(sK56(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
& v1_group_1(sK55(X0,X1,X2,X3))
& m1_group_2(sK55(X0,X1,X2,X3),X0) ) )
& ( ! [X6] :
( ! [X7] :
( k1_funct_1(X3,X6) = k5_group_4(X1,X7)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6)) != X7
| ~ m1_subset_1(X7,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X6)
| ~ m1_group_2(X6,X0) )
| k3_latsubgr(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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(skolemize,[status(esa),new_symbols(skolem,[sK55,sK56]),skolemize(X4,sK55(X0,X1,X2,X3)),skolemize(X5,sK56(X0,X1,X2,X3))],[f9491]) ).
fof(f9805,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| ~ r2_hidden(X2,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f6944]) ).
fof(f9806,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| ~ r2_hidden(X2,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f9805]) ).
fof(f9807,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0) )
& ( ( v1_group_1(X3)
& m1_group_2(X3,X0) )
| ~ r2_hidden(X3,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f9806]) ).
fof(f9808,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ( ( ~ v1_group_1(sK226(X0,X1))
| ~ m1_group_2(sK226(X0,X1),X0)
| ~ r2_hidden(sK226(X0,X1),X1) )
& ( ( v1_group_1(sK226(X0,X1))
& m1_group_2(sK226(X0,X1),X0) )
| r2_hidden(sK226(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0) )
& ( ( v1_group_1(X3)
& m1_group_2(X3,X0) )
| ~ r2_hidden(X3,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK226]),skolemize(X2,sK226(X0,X1))],[f9807]) ).
fof(f9877,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1318]) ).
fof(f10447,plain,
! [X0,X1,X2] :
( ( ( r1_group_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_group_2(X0,X1,X2) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(nnf_transformation,[],[f8749]) ).
fof(f10616,plain,
l1_group_1(sK52),
inference(cnf_transformation,[],[f9483]) ).
fof(f10617,plain,
v4_group_1(sK52),
inference(cnf_transformation,[],[f9483]) ).
fof(f10618,plain,
v3_group_1(sK52),
inference(cnf_transformation,[],[f9483]) ).
fof(f10619,plain,
~ v3_struct_0(sK52),
inference(cnf_transformation,[],[f9483]) ).
fof(f10620,plain,
k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) != k6_partfun1(u1_struct_0(k11_group_4(sK52))),
inference(cnf_transformation,[],[f9483]) ).
fof(f10623,plain,
! [X0] :
( v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f5779]) ).
fof(f10644,plain,
! [X0] : k6_relat_1(X0) = k6_partfun1(X0),
inference(cnf_transformation,[],[f1560]) ).
fof(f10646,plain,
! [X0] : v1_partfun1(k6_partfun1(X0),X0,X0),
inference(cnf_transformation,[],[f1559]) ).
fof(f10672,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| k1_group_3(X0) = u1_struct_0(k11_group_4(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f5824]) ).
fof(f10687,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| m1_group_2(sK55(X0,X1,X2,X3),X0)
| ~ v1_funct_1(X3)
| k3_latsubgr(X0,X1,X2) = X3
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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(cnf_transformation,[],[f9492]) ).
fof(f10688,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| v1_group_1(sK55(X0,X1,X2,X3))
| ~ v1_funct_1(X3)
| k3_latsubgr(X0,X1,X2) = X3
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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(cnf_transformation,[],[f9492]) ).
fof(f10690,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| sK56(X0,X1,X2,X3) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(sK55(X0,X1,X2,X3)))
| ~ v1_funct_1(X3)
| k3_latsubgr(X0,X1,X2) = X3
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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(cnf_transformation,[],[f9492]) ).
fof(f10691,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(X3,sK55(X0,X1,X2,X3)) != k5_group_4(X1,sK56(X0,X1,X2,X3))
| k3_latsubgr(X0,X1,X2) = X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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(cnf_transformation,[],[f9492]) ).
fof(f11090,plain,
! [X2,X0,X1] :
( ~ v1_partfun1(X2,X0,X1)
| ~ v1_funct_1(X2)
| v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f6108]) ).
fof(f11727,plain,
! [X0] : m2_relset_1(k6_relat_1(X0),X0,X0),
inference(cnf_transformation,[],[f1287]) ).
fof(f11735,plain,
! [X0,X1] :
( k9_relat_1(k6_relat_1(X0),X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f6600]) ).
fof(f11736,plain,
! [X0,X1] :
( k1_funct_1(k6_relat_1(X0),X1) = X1
| ~ r2_hidden(X1,X0) ),
inference(cnf_transformation,[],[f6601]) ).
fof(f11741,plain,
! [X0] : v1_funct_1(k6_relat_1(X0)),
inference(cnf_transformation,[],[f917]) ).
fof(f12201,plain,
! [X3,X0,X1] :
( r2_hidden(X3,X1)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0)
| k1_group_3(X0) != X1
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f9808]) ).
fof(f12418,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,[],[f7050]) ).
fof(f12438,plain,
! [X2,X0,X1] :
( r1_group_2(X0,k5_group_4(X0,X1),X2)
| u1_struct_0(X2) != X1
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f7074]) ).
fof(f12439,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| m1_group_2(k5_group_4(X0,X1),X0) ),
inference(cnf_transformation,[],[f7076]) ).
fof(f12440,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v1_group_1(k5_group_4(X0,X1)) ),
inference(cnf_transformation,[],[f7076]) ).
fof(f12468,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f9877]) ).
fof(f12923,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,[],[f7447]) ).
fof(f12945,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f7461]) ).
fof(f14441,plain,
! [X2,X0,X1] :
( m1_subset_1(k12_group_2(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f8679]) ).
fof(f14506,plain,
! [X2,X0,X1] :
( ~ r1_group_2(X0,X1,X2)
| X1 = X2
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(cnf_transformation,[],[f10447]) ).
fof(f14708,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,[],[f8958]) ).
fof(f15478,plain,
! [X0] : m2_relset_1(k6_partfun1(X0),X0,X0),
inference(definition_unfolding,[],[f11727,f10644]) ).
fof(f15486,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k9_relat_1(k6_partfun1(X0),X1) = X1 ),
inference(definition_unfolding,[],[f11735,f10644]) ).
fof(f15487,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| k1_funct_1(k6_partfun1(X0),X1) = X1 ),
inference(definition_unfolding,[],[f11736,f10644]) ).
fof(f15493,plain,
! [X0] : v1_funct_1(k6_partfun1(X0)),
inference(definition_unfolding,[],[f11741,f10644]) ).
fof(f15999,plain,
! [X3,X0] :
( r2_hidden(X3,k1_group_3(X0))
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f12201]) ).
fof(f16009,plain,
! [X2,X0] :
( r1_group_2(X0,k5_group_4(X0,u1_struct_0(X2)),X2)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(u1_struct_0(X2),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f12438]) ).
fof(f16654,plain,
( v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| u1_struct_0(k11_group_4(sK52)) = k1_group_3(sK52)
| ~ l1_group_1(sK52) ),
inference(resolution,[],[f10672,f10617]) ).
fof(f16655,plain,
( ~ v3_group_1(sK52)
| u1_struct_0(k11_group_4(sK52)) = k1_group_3(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f16654,f10619]) ).
fof(f16656,plain,
( u1_struct_0(k11_group_4(sK52)) = k1_group_3(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f16655,f10618]) ).
fof(f16657,plain,
u1_struct_0(k11_group_4(sK52)) = k1_group_3(sK52),
inference(forward_subsumption_resolution,[],[f16656,f10616]) ).
fof(f16735,plain,
! [X0,X1] :
( ~ m1_group_2(X0,X1)
| ~ v1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| k1_funct_1(k6_partfun1(k1_group_3(X1)),X0) = X0 ),
inference(resolution,[],[f15999,f15487]) ).
fof(f16742,plain,
! [X0] : m1_relset_1(k6_partfun1(X0),X0,X0),
inference(resolution,[],[f12468,f15478]) ).
fof(f16804,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| m1_group_2(sK55(X1,sK52,X2,X0),X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(X1,sK52,X2) = X0
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(sK52))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(superposition,[],[f10687,f16657]) ).
fof(f16807,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| m1_group_2(sK55(X1,sK52,X2,X0),X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(X1,sK52,X2) = X0
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(sK52))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(sK52))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f16804,f10619]) ).
fof(f16811,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| m1_group_2(sK55(X1,sK52,X2,X0),X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(X1,sK52,X2) = X0
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(sK52))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(sK52))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f16807,f10618]) ).
fof(f16815,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| m1_group_2(sK55(X1,sK52,X2,X0),X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(X1,sK52,X2) = X0
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(sK52))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(sK52))
| ~ l1_group_1(sK52)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f16811,f10617]) ).
fof(f16818,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| m1_group_2(sK55(X1,sK52,X2,X0),X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(X1,sK52,X2) = X0
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(X1)),k1_group_3(sK52))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(sK52))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(sK52))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f16815,f10616]) ).
fof(f16823,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| sK56(sK52,X1,X2,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(X1),X2,u1_struct_0(sK55(sK52,X1,X2,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(superposition,[],[f10690,f16657]) ).
fof(f16828,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| sK56(sK52,X1,X2,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(X1),X2,u1_struct_0(sK55(sK52,X1,X2,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f16823,f10619]) ).
fof(f16832,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| sK56(sK52,X1,X2,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(X1),X2,u1_struct_0(sK55(sK52,X1,X2,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f16828,f10618]) ).
fof(f16836,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| sK56(sK52,X1,X2,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(X1),X2,u1_struct_0(sK55(sK52,X1,X2,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f16832,f10617]) ).
fof(f16839,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| sK56(sK52,X1,X2,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(X1),X2,u1_struct_0(sK55(sK52,X1,X2,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f16836,f10616]) ).
fof(f16852,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| v1_group_1(sK55(sK52,X1,X2,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(superposition,[],[f10688,f16657]) ).
fof(f16857,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| v1_group_1(sK55(sK52,X1,X2,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f16852,f10619]) ).
fof(f16861,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| v1_group_1(sK55(sK52,X1,X2,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f16857,f10618]) ).
fof(f16865,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| v1_group_1(sK55(sK52,X1,X2,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f16861,f10617]) ).
fof(f16868,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| v1_group_1(sK55(sK52,X1,X2,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,X1,X2) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK52),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK52),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f16865,f10616]) ).
fof(f17201,plain,
! [X0,X1] :
( ~ v1_funct_1(k6_partfun1(u1_struct_0(X0)))
| k9_relat_1(k6_partfun1(u1_struct_0(X0)),X1) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_partfun1(u1_struct_0(X0)),X1)
| ~ m1_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f12418,f10623]) ).
fof(f17207,plain,
! [X0,X1] :
( k9_relat_1(k6_partfun1(u1_struct_0(X0)),X1) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_partfun1(u1_struct_0(X0)),X1)
| ~ m1_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f17201,f15493]) ).
fof(f17209,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| k9_relat_1(k6_partfun1(u1_struct_0(X0)),X1) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_partfun1(u1_struct_0(X0)),X1)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f17207,f16742]) ).
fof(f17242,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| sK56(sK52,sK52,X1,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),X1,u1_struct_0(sK55(sK52,sK52,X1,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(superposition,[],[f16839,f16657]) ).
fof(f17244,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| sK56(sK52,sK52,X1,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),X1,u1_struct_0(sK55(sK52,sK52,X1,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17242,f10619]) ).
fof(f17246,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| sK56(sK52,sK52,X1,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),X1,u1_struct_0(sK55(sK52,sK52,X1,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17244,f10618]) ).
fof(f17247,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| sK56(sK52,sK52,X1,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),X1,u1_struct_0(sK55(sK52,sK52,X1,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17246,f10617]) ).
fof(f17248,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| sK56(sK52,sK52,X1,X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),X1,u1_struct_0(sK55(sK52,sK52,X1,X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52)) ),
inference(forward_subsumption_resolution,[],[f17247,f10616]) ).
fof(f17289,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| v1_group_1(sK55(sK52,sK52,X1,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(superposition,[],[f16868,f16657]) ).
fof(f17291,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| v1_group_1(sK55(sK52,sK52,X1,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17289,f10619]) ).
fof(f17293,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| v1_group_1(sK55(sK52,sK52,X1,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17291,f10618]) ).
fof(f17294,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| v1_group_1(sK55(sK52,sK52,X1,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17293,f10617]) ).
fof(f17295,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| v1_group_1(sK55(sK52,sK52,X1,X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52)) ),
inference(forward_subsumption_resolution,[],[f17294,f10616]) ).
fof(f17296,plain,
! [X0] :
( v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(resolution,[],[f17295,f10623]) ).
fof(f17297,plain,
! [X0] :
( v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17296,f15493]) ).
fof(f17298,plain,
! [X0] :
( v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17297,f15478]) ).
fof(f17299,plain,
! [X0] :
( v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17298,f10619]) ).
fof(f17300,plain,
! [X0] :
( v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17299,f10618]) ).
fof(f17301,plain,
! [X0] :
( v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17300,f10617]) ).
fof(f17302,plain,
! [X0] :
( v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52)) ),
inference(forward_subsumption_resolution,[],[f17301,f10616]) ).
fof(f17366,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| m1_group_2(sK55(sK52,sK52,X1,X0),sK52)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(superposition,[],[f16818,f16657]) ).
fof(f17368,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| m1_group_2(sK55(sK52,sK52,X1,X0),sK52)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17366,f10619]) ).
fof(f17370,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| m1_group_2(sK55(sK52,sK52,X1,X0),sK52)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17368,f10618]) ).
fof(f17371,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| m1_group_2(sK55(sK52,sK52,X1,X0),sK52)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17370,f10617]) ).
fof(f17372,plain,
! [X0,X1] :
( m1_group_2(sK55(sK52,sK52,X1,X0),sK52)
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,X1) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(X1,u1_struct_0(sK52),u1_struct_0(sK52)) ),
inference(forward_subsumption_resolution,[],[f17371,f10616]) ).
fof(f17431,plain,
! [X0,X1] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,X1)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| k5_group_4(X1,u1_struct_0(X0)) = X0
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(k5_group_4(X1,u1_struct_0(X0)))
| ~ m1_group_2(k5_group_4(X1,u1_struct_0(X0)),X1)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,X1) ),
inference(resolution,[],[f16009,f14506]) ).
fof(f17433,plain,
! [X0,X1] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,X1)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| k5_group_4(X1,u1_struct_0(X0)) = X0
| ~ v1_group_1(k5_group_4(X1,u1_struct_0(X0)))
| ~ m1_group_2(k5_group_4(X1,u1_struct_0(X0)),X1) ),
inference(duplicate_literal_removal,[],[f17431]) ).
fof(f17435,plain,
! [X0,X1] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,X1)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| k5_group_4(X1,u1_struct_0(X0)) = X0
| ~ m1_group_2(k5_group_4(X1,u1_struct_0(X0)),X1) ),
inference(forward_subsumption_resolution,[],[f17433,f12440]) ).
fof(f17437,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_group_2(X0,X1)
| ~ v1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| k5_group_4(X1,u1_struct_0(X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f17435,f12439]) ).
fof(f17869,plain,
! [X0] :
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(resolution,[],[f17248,f10623]) ).
fof(f17870,plain,
! [X0] :
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17869,f15493]) ).
fof(f17871,plain,
! [X0] :
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17870,f15478]) ).
fof(f17872,plain,
! [X0] :
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17871,f10619]) ).
fof(f17873,plain,
! [X0] :
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17872,f10618]) ).
fof(f17874,plain,
! [X0] :
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f17873,f10617]) ).
fof(f17875,plain,
! [X0] :
( ~ v1_funct_2(X0,k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = X0
| ~ m2_relset_1(X0,k1_group_3(sK52),k1_group_3(sK52))
| sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),X0))) ),
inference(forward_subsumption_resolution,[],[f17874,f10616]) ).
fof(f18917,plain,
! [X0] :
( v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| k9_relat_1(k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),X0)
| ~ l1_group_1(sK52) ),
inference(resolution,[],[f17209,f10617]) ).
fof(f18922,plain,
! [X0] :
( ~ v3_group_1(sK52)
| k9_relat_1(k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),X0)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f18917,f10619]) ).
fof(f18925,plain,
! [X0] :
( k9_relat_1(k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),X0)
| ~ l1_group_1(sK52) ),
inference(forward_subsumption_resolution,[],[f18922,f10618]) ).
fof(f18928,plain,
! [X0] : k9_relat_1(k6_partfun1(u1_struct_0(sK52)),X0) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),X0),
inference(forward_subsumption_resolution,[],[f18925,f10616]) ).
fof(f20032,plain,
! [X0] :
( ~ v1_funct_1(k6_partfun1(X0))
| v1_funct_2(k6_partfun1(X0),X0,X0)
| ~ m1_relset_1(k6_partfun1(X0),X0,X0) ),
inference(resolution,[],[f11090,f10646]) ).
fof(f20035,plain,
! [X0] :
( v1_funct_2(k6_partfun1(X0),X0,X0)
| ~ m1_relset_1(k6_partfun1(X0),X0,X0) ),
inference(forward_subsumption_resolution,[],[f20032,f15493]) ).
fof(f20036,plain,
! [X0] : v1_funct_2(k6_partfun1(X0),X0,X0),
inference(forward_subsumption_resolution,[],[f20035,f16742]) ).
fof(f20062,plain,
( ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))) ),
inference(resolution,[],[f20036,f17875]) ).
fof(f20079,plain,
( k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))) ),
inference(forward_subsumption_resolution,[],[f20062,f15493]) ).
fof(f20091,plain,
( k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k2_funct_2(u1_struct_0(sK52),u1_struct_0(sK52),k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))) ),
inference(forward_subsumption_resolution,[],[f20079,f15478]) ).
fof(f20106,definition,
( spl646_131
<=> k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52)) ),
introduced(definition,[new_symbols(definition,[spl646_131])],[avatar_definition]) ).
fof(f20107,plain,
( k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) != k6_partfun1(k1_group_3(sK52))
| spl646_131 ),
inference(avatar_component_clause,[],[f20106]) ).
fof(f20108,plain,
( k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ spl646_131 ),
inference(avatar_component_clause,[],[f20106]) ).
fof(f20110,plain,
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k9_relat_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52)) ),
inference(forward_demodulation,[],[f20091,f18928]) ).
fof(f20117,definition,
( spl646_133
<=> sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k9_relat_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))) ),
introduced(definition,[new_symbols(definition,[spl646_133])],[avatar_definition]) ).
fof(f20119,plain,
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k9_relat_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_133 ),
inference(avatar_component_clause,[],[f20117]) ).
fof(f20120,plain,
( spl646_131
| spl646_133 ),
inference(avatar_split_clause,[],[f20110,f20117,f20106]) ).
fof(f20121,plain,
( k6_partfun1(u1_struct_0(k11_group_4(sK52))) != k6_partfun1(k1_group_3(sK52))
| ~ spl646_131 ),
inference(superposition,[],[f10620,f20108]) ).
fof(f20167,plain,
( k6_partfun1(k1_group_3(sK52)) != k6_partfun1(k1_group_3(sK52))
| ~ spl646_131 ),
inference(forward_demodulation,[],[f20121,f16657]) ).
fof(f20168,plain,
( $false
| ~ spl646_131 ),
inference(trivial_inequality_removal,[],[f20167]) ).
fof(f20169,plain,
~ spl646_131,
inference(avatar_contradiction_clause,[],[f20168]) ).
fof(f24304,definition,
( spl646_189
<=> v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) ),
introduced(definition,[new_symbols(definition,[spl646_189])],[avatar_definition]) ).
fof(f24305,plain,
( v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_189 ),
inference(avatar_component_clause,[],[f24304]) ).
fof(f24306,plain,
( ~ v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| spl646_189 ),
inference(avatar_component_clause,[],[f24304]) ).
fof(f24308,definition,
( spl646_190
<=> m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52) ),
introduced(definition,[new_symbols(definition,[spl646_190])],[avatar_definition]) ).
fof(f24309,plain,
( m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| ~ spl646_190 ),
inference(avatar_component_clause,[],[f24308]) ).
fof(f24310,plain,
( ~ m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| spl646_190 ),
inference(avatar_component_clause,[],[f24308]) ).
fof(f24359,plain,
( ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| spl646_189 ),
inference(resolution,[],[f24306,f17302]) ).
fof(f24360,plain,
( k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| spl646_189 ),
inference(forward_subsumption_resolution,[],[f24359,f15493]) ).
fof(f24361,plain,
( ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| spl646_131
| spl646_189 ),
inference(forward_subsumption_resolution,[],[f24360,f20107]) ).
fof(f24362,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| spl646_131
| spl646_189 ),
inference(forward_subsumption_resolution,[],[f24361,f15478]) ).
fof(f24363,plain,
( $false
| spl646_131
| spl646_189 ),
inference(forward_subsumption_resolution,[],[f24362,f20036]) ).
fof(f24364,plain,
( spl646_131
| spl646_189 ),
inference(avatar_contradiction_clause,[],[f24363]) ).
fof(f24375,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ v1_funct_2(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| spl646_190 ),
inference(resolution,[],[f24310,f17372]) ).
fof(f24379,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| spl646_190 ),
inference(forward_subsumption_resolution,[],[f24375,f20036]) ).
fof(f24381,plain,
( ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| spl646_190 ),
inference(forward_subsumption_resolution,[],[f24379,f20036]) ).
fof(f24383,plain,
( ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| spl646_190 ),
inference(forward_subsumption_resolution,[],[f24381,f15493]) ).
fof(f24385,plain,
( k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| spl646_190 ),
inference(forward_subsumption_resolution,[],[f24383,f15493]) ).
fof(f24387,plain,
( ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| spl646_131
| spl646_190 ),
inference(forward_subsumption_resolution,[],[f24385,f20107]) ).
fof(f24389,plain,
( ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| spl646_131
| spl646_190 ),
inference(forward_subsumption_resolution,[],[f24387,f15478]) ).
fof(f24391,plain,
( $false
| spl646_131
| spl646_190 ),
inference(forward_subsumption_resolution,[],[f24389,f15478]) ).
fof(f24392,plain,
( spl646_131
| spl646_190 ),
inference(avatar_contradiction_clause,[],[f24391]) ).
fof(f24399,plain,
( k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k12_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),k2_group_1(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_190 ),
inference(resolution,[],[f24309,f12923]) ).
fof(f24408,plain,
( u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_190 ),
inference(resolution,[],[f24309,f14708]) ).
fof(f24414,plain,
( ~ v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k1_funct_1(k6_partfun1(k1_group_3(sK52)),sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_190 ),
inference(resolution,[],[f24309,f16735]) ).
fof(f24419,plain,
( v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k1_funct_1(k6_partfun1(k1_group_3(sK52)),sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24414,f24305]) ).
fof(f24423,plain,
( u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24408,f10619]) ).
fof(f24429,plain,
( k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k12_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),k2_group_1(sK52))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24399,f10619]) ).
fof(f24437,plain,
( ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k1_funct_1(k6_partfun1(k1_group_3(sK52)),sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24419,f10619]) ).
fof(f24441,plain,
( u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24423,f10618]) ).
fof(f24447,plain,
( k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k12_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),k2_group_1(sK52))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24429,f10618]) ).
fof(f24455,plain,
( ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k1_funct_1(k6_partfun1(k1_group_3(sK52)),sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24437,f10618]) ).
fof(f24459,plain,
( u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ l1_group_1(sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24441,f10617]) ).
fof(f24465,plain,
( k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k12_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),k2_group_1(sK52))
| ~ l1_group_1(sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24447,f10617]) ).
fof(f24473,plain,
( ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k1_funct_1(k6_partfun1(k1_group_3(sK52)),sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24455,f10617]) ).
fof(f24477,plain,
( u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24459,f10616]) ).
fof(f24482,plain,
( k7_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k12_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),k2_group_1(sK52))
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24465,f10616]) ).
fof(f24487,plain,
( sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k1_funct_1(k6_partfun1(k1_group_3(sK52)),sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24473,f10616]) ).
fof(f24490,plain,
( u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k12_group_2(sK52,sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),k2_group_1(sK52))
| ~ spl646_190 ),
inference(forward_demodulation,[],[f24482,f24477]) ).
fof(f24507,plain,
( m1_subset_1(u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))),k1_zfmisc_1(u1_struct_0(sK52)))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| ~ m1_subset_1(k2_group_1(sK52),u1_struct_0(sK52))
| ~ spl646_190 ),
inference(superposition,[],[f14441,f24490]) ).
fof(f24508,plain,
( m1_subset_1(u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))),k1_zfmisc_1(u1_struct_0(sK52)))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24507,f12945]) ).
fof(f24509,plain,
( m1_subset_1(u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))),k1_zfmisc_1(u1_struct_0(sK52)))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24508,f10619]) ).
fof(f24510,plain,
( m1_subset_1(u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))),k1_zfmisc_1(u1_struct_0(sK52)))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24509,f10618]) ).
fof(f24511,plain,
( m1_subset_1(u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))),k1_zfmisc_1(u1_struct_0(sK52)))
| ~ l1_group_1(sK52)
| ~ m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24510,f10617]) ).
fof(f24512,plain,
( m1_subset_1(u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))),k1_zfmisc_1(u1_struct_0(sK52)))
| ~ m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24511,f10616]) ).
fof(f24513,plain,
( m1_subset_1(u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))),k1_zfmisc_1(u1_struct_0(sK52)))
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24512,f24309]) ).
fof(f24522,plain,
( ~ m1_group_2(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))),sK52)
| ~ v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k5_group_4(sK52,u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_190 ),
inference(resolution,[],[f24513,f17437]) ).
fof(f24527,plain,
( u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))) = k9_relat_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_190 ),
inference(resolution,[],[f24513,f15486]) ).
fof(f24534,plain,
( sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_133
| ~ spl646_190 ),
inference(forward_demodulation,[],[f24527,f20119]) ).
fof(f24537,plain,
( ~ v1_group_1(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k5_group_4(sK52,u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24522,f24309]) ).
fof(f24540,plain,
( v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k5_group_4(sK52,u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24537,f24305]) ).
fof(f24543,plain,
( ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k5_group_4(sK52,u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24540,f10619]) ).
fof(f24546,plain,
( ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k5_group_4(sK52,u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24543,f10618]) ).
fof(f24549,plain,
( ~ l1_group_1(sK52)
| sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k5_group_4(sK52,u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24546,f10617]) ).
fof(f24550,plain,
( sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k5_group_4(sK52,u1_struct_0(sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52)))))
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24549,f10616]) ).
fof(f24551,plain,
( sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) = k5_group_4(sK52,sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_demodulation,[],[f24550,f24534]) ).
fof(f24564,plain,
( sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) != k5_group_4(sK52,sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ v1_funct_2(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_189
| ~ spl646_190 ),
inference(superposition,[],[f10691,f24487]) ).
fof(f24565,plain,
( sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) != k5_group_4(sK52,sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ v1_funct_2(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_189
| ~ spl646_190 ),
inference(duplicate_literal_removal,[],[f24564]) ).
fof(f24566,plain,
( sK55(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))) != k5_group_4(sK52,sK56(sK52,sK52,k6_partfun1(u1_struct_0(sK52)),k6_partfun1(k1_group_3(sK52))))
| k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24565,f10623]) ).
fof(f24567,plain,
( k3_latsubgr(sK52,sK52,k6_partfun1(u1_struct_0(sK52))) = k6_partfun1(k1_group_3(sK52))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24566,f24551]) ).
fof(f24568,plain,
( ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK52)))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24567,f20107]) ).
fof(f24569,plain,
( ~ v1_funct_1(k6_partfun1(k1_group_3(sK52)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24568,f15493]) ).
fof(f24570,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(u1_struct_0(sK52)),u1_struct_0(sK52),u1_struct_0(sK52))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24569,f15493]) ).
fof(f24571,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| v3_struct_0(sK52)
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24570,f15478]) ).
fof(f24572,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ v3_group_1(sK52)
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24571,f10619]) ).
fof(f24573,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ v4_group_1(sK52)
| ~ l1_group_1(sK52)
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24572,f10618]) ).
fof(f24574,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ l1_group_1(sK52)
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24573,f10617]) ).
fof(f24575,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24574,f10616]) ).
fof(f24576,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_demodulation,[],[f24575,f16657]) ).
fof(f24577,plain,
( ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),u1_struct_0(k11_group_4(sK52)),u1_struct_0(k11_group_4(sK52)))
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24576,f20036]) ).
fof(f24578,plain,
( ~ m2_relset_1(k6_partfun1(k1_group_3(sK52)),k1_group_3(sK52),k1_group_3(sK52))
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_demodulation,[],[f24577,f16657]) ).
fof(f24579,plain,
( $false
| spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(forward_subsumption_resolution,[],[f24578,f15478]) ).
fof(f24580,plain,
( spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(avatar_contradiction_clause,[],[f24579]) ).
cnf(s111,plain,
( spl646_131
| spl646_133 ),
inference(sat_conversion,[],[f20120]) ).
cnf(s113,plain,
~ spl646_131,
inference(sat_conversion,[],[f20169]) ).
cnf(s163,plain,
( spl646_131
| spl646_189 ),
inference(sat_conversion,[],[f24364]) ).
cnf(s165,plain,
( spl646_131
| spl646_190 ),
inference(sat_conversion,[],[f24392]) ).
cnf(s168,plain,
( spl646_131
| ~ spl646_133
| ~ spl646_189
| ~ spl646_190 ),
inference(sat_conversion,[],[f24580]) ).
cnf(s179,plain,
spl646_190,
inference(rat,[],[s165,s113]) ).
cnf(s180,plain,
spl646_189,
inference(rat,[],[s163,s113]) ).
cnf(s183,plain,
~ spl646_133,
inference(rat,[],[s168,s179,s113,s180]) ).
cnf(s185,plain,
$false,
inference(rat,[],[s111,s183,s113]) ).
fof(f24581,plain,
$false,
inference(avatar_sat_refutation,[],[s185]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP650+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n003.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 10:29:57 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.51/3.25 % (316860)Detected formulas, will run a generic FOF schedule.
% 15.51/3.25 % (316869)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2537781711:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 15.51/3.25 % (316870)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3101368163:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 15.51/3.25 % (316867)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=218870403:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 15.51/3.25 % (316865)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=4199893480:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 15.51/3.25 % (316868)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1845277542:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 15.51/3.25 % (316866)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=4248274631:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 15.51/3.25 % (316869)Instruction limit reached!
% 15.51/3.25 % (316869)------------------------------
% 15.51/3.25 % (316869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.51/3.25 % (316869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/3.25 % (316869)CaDiCaL version: 2.1.3
% 15.51/3.25 % (316869)Termination reason: Instruction limit
% 15.51/3.25 % (316869)Termination phase: Property scanning
% 15.51/3.25 % (316869)Time elapsed: 0.044 s
% 15.51/3.25 % (316869)Peak memory usage: 95 MB
% 15.51/3.25 % (316869)Instructions burned: 120 (million)
% 15.51/3.25 % (316871)dis-21_1_sil=8000:lcm=predicate:random_seed=1970563270:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 15.51/3.25 % (316868)Refutation not found, incomplete strategy
% 15.51/3.25 % (316868)------------------------------
% 15.51/3.25 % (316868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.51/3.25 % (316868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/3.25 % (316868)CaDiCaL version: 2.1.3
% 15.51/3.25 % (316868)Termination reason: Refutation not found, incomplete strategy
% 15.51/3.25 % (316868)Time elapsed: 0.028 s
% 15.51/3.25 % (316868)Peak memory usage: 95 MB
% 15.51/3.25 % (316868)Instructions burned: 35 (million)
% 15.51/3.25 % (316870)Instruction limit reached!
% 15.51/3.25 % (316870)------------------------------
% 15.51/3.25 % (316870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.51/3.25 % (316870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/3.25 % (316870)CaDiCaL version: 2.1.3
% 15.51/3.25 % (316870)Termination reason: Instruction limit
% 15.51/3.25 % (316870)Termination phase: Unused predicate definition removal
% 15.51/3.25 % (316870)Time elapsed: 0.084 s
% 15.51/3.25 % (316870)Peak memory usage: 92 MB
% 15.51/3.25 % (316870)Instructions burned: 139 (million)
% 15.51/3.25 % (316871)Instruction limit reached!
% 15.51/3.25 % (316871)------------------------------
% 15.51/3.25 % (316871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.51/3.25 % (316871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/3.25 % (316871)CaDiCaL version: 2.1.3
% 15.51/3.25 % (316871)Termination reason: Instruction limit
% 15.51/3.25 % (316871)Termination phase: Preprocessing 3
% 15.51/3.25 % (316871)Time elapsed: 0.097 s
% 15.51/3.25 % (316871)Peak memory usage: 97 MB
% 15.51/3.25 % (316871)Instructions burned: 130 (million)
% 15.51/3.25 % (316878)lrs+10_1_sil=8000:sp=occurrence:random_seed=3619961862:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 15.51/3.25 % (316878)Instruction limit reached!
% 15.51/3.25 % (316878)------------------------------
% 15.51/3.25 % (316878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.51/3.25 % (316878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/3.25 % (316878)CaDiCaL version: 2.1.3
% 15.51/3.25 % (316878)Termination reason: Instruction limit
% 15.51/3.25 % (316878)Termination phase: Saturation
% 15.51/3.25 % (316878)Time elapsed: 0.100 s
% 15.51/3.25 % (316878)Peak memory usage: 100 MB
% 15.51/3.25 % (316878)Instructions burned: 287 (million)
% 15.51/3.25 % (316880)lrs+10_1_sil=32000:urr=on:br=off:random_seed=233582746:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 22.13/4.18 % (316868)------------------------------
% 22.13/4.18 % (316868)------------------------------
% 22.13/4.18 % (316881)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3332544377:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 22.13/4.18 % (316880)Refutation not found, incomplete strategy
% 22.13/4.18 % (316880)------------------------------
% 22.13/4.18 % (316880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.13/4.18 % (316880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.13/4.18 % (316880)CaDiCaL version: 2.1.3
% 22.13/4.18 % (316880)Termination reason: Refutation not found, incomplete strategy
% 22.13/4.18 % (316880)Time elapsed: 0.057 s
% 22.13/4.18 % (316880)Peak memory usage: 96 MB
% 22.13/4.18 % (316880)Instructions burned: 100 (million)
% 22.13/4.18 % (316881)Refutation not found, incomplete strategy
% 22.13/4.18 % (316881)------------------------------
% 22.13/4.18 % (316881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.13/4.18 % (316881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.13/4.18 % (316881)CaDiCaL version: 2.1.3
% 22.13/4.18 % (316881)Termination reason: Refutation not found, incomplete strategy
% 22.13/4.18 % (316881)Time elapsed: 0.032 s
% 22.13/4.18 % (316881)Peak memory usage: 96 MB
% 22.13/4.18 % (316881)Instructions burned: 38 (million)
% 22.13/4.18 % (316883)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=2137230838:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 22.13/4.18 % (316883)Instruction limit reached!
% 22.13/4.18 % (316883)------------------------------
% 22.13/4.18 % (316883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.13/4.18 % (316883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.13/4.18 % (316883)CaDiCaL version: 2.1.3
% 22.13/4.18 % (316883)Termination reason: Instruction limit
% 22.13/4.18 % (316883)Termination phase: Preprocessing 3
% 22.13/4.18 % (316883)Time elapsed: 0.088 s
% 22.13/4.18 % (316883)Peak memory usage: 100 MB
% 22.13/4.18 % (316883)Instructions burned: 249 (million)
% 22.13/4.18 % (316886)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1690446188:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 22.13/4.18 % (316880)------------------------------
% 22.13/4.18 % (316880)------------------------------
% 22.13/4.18 % (316881)------------------------------
% 22.13/4.18 % (316881)------------------------------
% 22.13/4.18 % (316888)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=460771195:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 22.13/4.18 % (316886)Instruction limit reached!
% 22.13/4.18 % (316886)------------------------------
% 22.13/4.18 % (316886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.13/4.18 % (316886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.13/4.18 % (316886)CaDiCaL version: 2.1.3
% 22.13/4.18 % (316886)Termination reason: Instruction limit
% 22.13/4.18 % (316886)Termination phase: Saturation
% 22.13/4.18 % (316886)Time elapsed: 0.174 s
% 22.13/4.18 % (316886)Peak memory usage: 98 MB
% 22.13/4.18 % (316886)Instructions burned: 294 (million)
% 22.13/4.18 % (316890)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4066317125:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 22.13/4.18 % (316895)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3258913666:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 22.13/4.18 % (316890)Instruction limit reached!
% 22.13/4.18 % (316890)------------------------------
% 22.13/4.18 % (316890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.13/4.18 % (316890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.13/4.18 % (316890)CaDiCaL version: 2.1.3
% 22.13/4.18 % (316890)Termination reason: Instruction limit
% 22.13/4.18 % (316890)Termination phase: Property scanning
% 22.13/4.18 % (316890)Time elapsed: 0.077 s
% 22.13/4.18 % (316890)Peak memory usage: 95 MB
% 22.13/4.18 % (316890)Instructions burned: 113 (million)
% 22.13/4.18 % (316898)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2733243989:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 22.13/4.18 % (316895)Instruction limit reached!
% 33.94/6.35 % (316895)------------------------------
% 33.94/6.35 % (316895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.35 % (316895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.35 % (316895)CaDiCaL version: 2.1.3
% 33.94/6.35 % (316895)Termination reason: Instruction limit
% 33.94/6.35 % (316895)Termination phase: Preprocessing 3
% 33.94/6.35 % (316895)Time elapsed: 0.088 s
% 33.94/6.35 % (316895)Peak memory usage: 99 MB
% 33.94/6.35 % (316895)Instructions burned: 127 (million)
% 33.94/6.35 % (316898)Instruction limit reached!
% 33.94/6.35 % (316898)------------------------------
% 33.94/6.35 % (316898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.35 % (316898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.35 % (316898)CaDiCaL version: 2.1.3
% 33.94/6.35 % (316898)Termination reason: Instruction limit
% 33.94/6.35 % (316898)Termination phase: Property scanning
% 33.94/6.35 % (316898)Time elapsed: 0.049 s
% 33.94/6.35 % (316898)Peak memory usage: 91 MB
% 33.94/6.35 % (316898)Instructions burned: 116 (million)
% 33.94/6.35 % (316901)lrs+10_1_sil=8000:sp=occurrence:random_seed=3021768649:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 33.94/6.35 % (316903)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1594288071:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 33.94/6.35 % (316904)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2797444559:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 33.94/6.35 % (316903)Refutation not found, incomplete strategy
% 33.94/6.35 % (316903)------------------------------
% 33.94/6.35 % (316903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.35 % (316903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.35 % (316903)CaDiCaL version: 2.1.3
% 33.94/6.35 % (316903)Termination reason: Refutation not found, incomplete strategy
% 33.94/6.35 % (316903)Time elapsed: 0.052 s
% 33.94/6.35 % (316903)Peak memory usage: 96 MB
% 33.94/6.35 % (316903)Instructions burned: 78 (million)
% 33.94/6.35 % (316903)------------------------------
% 33.94/6.35 % (316903)------------------------------
% 33.94/6.36 % (316908)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4273354507:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 33.94/6.36 % (316901)Instruction limit reached!
% 33.94/6.36 % (316901)------------------------------
% 33.94/6.36 % (316901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316901)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316901)Termination reason: Instruction limit
% 33.94/6.36 % (316901)Termination phase: Saturation
% 33.94/6.36 % (316901)Time elapsed: 0.570 s
% 33.94/6.36 % (316901)Peak memory usage: 111 MB
% 33.94/6.36 % (316901)Instructions burned: 908 (million)
% 33.94/6.36 % (316908)Instruction limit reached!
% 33.94/6.36 % (316908)------------------------------
% 33.94/6.36 % (316908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316908)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316908)Termination reason: Instruction limit
% 33.94/6.36 % (316908)Termination phase: Saturation
% 33.94/6.36 % (316908)Time elapsed: 0.084 s
% 33.94/6.36 % (316908)Peak memory usage: 98 MB
% 33.94/6.36 % (316908)Instructions burned: 134 (million)
% 33.94/6.36 % (316910)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1340900023:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 33.94/6.36 % (316911)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1603004807:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 33.94/6.36 % (316910)Instruction limit reached!
% 33.94/6.36 % (316910)------------------------------
% 33.94/6.36 % (316910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316910)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316910)Termination reason: Instruction limit
% 33.94/6.36 % (316910)Termination phase: Saturation
% 33.94/6.36 % (316910)Time elapsed: 0.297 s
% 33.94/6.36 % (316910)Peak memory usage: 104 MB
% 33.94/6.36 % (316910)Instructions burned: 593 (million)
% 33.94/6.36 % (316888)Instruction limit reached!
% 33.94/6.36 % (316888)------------------------------
% 33.94/6.36 % (316888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316888)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316888)Termination reason: Instruction limit
% 33.94/6.36 % (316888)Termination phase: Saturation
% 33.94/6.36 % (316888)Time elapsed: 1.428 s
% 33.94/6.36 % (316888)Peak memory usage: 280 MB
% 33.94/6.36 % (316888)Instructions burned: 2352 (million)
% 33.94/6.36 % (316914)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=3710861250:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/125Mi)
% 33.94/6.36 % (316915)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=168153580:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 33.94/6.36 % (316914)Instruction limit reached!
% 33.94/6.36 % (316914)------------------------------
% 33.94/6.36 % (316914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316914)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316914)Termination reason: Instruction limit
% 33.94/6.36 % (316914)Termination phase: Preprocessing 1
% 33.94/6.36 % (316914)Time elapsed: 0.074 s
% 33.94/6.36 % (316914)Peak memory usage: 92 MB
% 33.94/6.36 % (316914)Instructions burned: 126 (million)
% 33.94/6.36 % (316915)Instruction limit reached!
% 33.94/6.36 % (316915)------------------------------
% 33.94/6.36 % (316915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316915)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316915)Termination reason: Instruction limit
% 33.94/6.36 % (316915)Termination phase: Property scanning
% 33.94/6.36 % (316915)Time elapsed: 0.057 s
% 33.94/6.36 % (316915)Peak memory usage: 91 MB
% 33.94/6.36 % (316915)Instructions burned: 136 (million)
% 33.94/6.36 % (316918)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2444122063:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/141Mi)
% 33.94/6.36 % (316918)Refutation not found, incomplete strategy
% 33.94/6.36 % (316918)------------------------------
% 33.94/6.36 % (316918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316918)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316918)Termination reason: Refutation not found, incomplete strategy
% 33.94/6.36 % (316918)Time elapsed: 0.026 s
% 33.94/6.36 % (316918)Peak memory usage: 95 MB
% 33.94/6.36 % (316918)Instructions burned: 31 (million)
% 33.94/6.36 % (316919)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=642808991:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 33.94/6.36 % (316919)Refutation not found, incomplete strategy
% 33.94/6.36 % (316919)------------------------------
% 33.94/6.36 % (316919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316919)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316919)Termination reason: Refutation not found, incomplete strategy
% 33.94/6.36 % (316919)Time elapsed: 0.027 s
% 33.94/6.36 % (316919)Peak memory usage: 95 MB
% 33.94/6.36 % (316919)Instructions burned: 32 (million)
% 33.94/6.36 % (316918)------------------------------
% 33.94/6.36 % (316918)------------------------------
% 33.94/6.36 % (316919)------------------------------
% 33.94/6.36 % (316919)------------------------------
% 33.94/6.36 % (316922)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=3871582543:i=6060:aac=none:ins=25_2969 on theBenchmark for (2969ds/6060Mi)
% 33.94/6.36 % (316923)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=3248303546:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2969 on theBenchmark for (2969ds/150Mi)
% 33.94/6.36 % (316923)Instruction limit reached!
% 33.94/6.36 % (316923)------------------------------
% 33.94/6.36 % (316923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316923)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316923)Termination reason: Instruction limit
% 33.94/6.36 % (316923)Termination phase: Preprocessing 3
% 33.94/6.36 % (316923)Time elapsed: 0.101 s
% 33.94/6.36 % (316923)Peak memory usage: 99 MB
% 33.94/6.36 % (316923)Instructions burned: 150 (million)
% 33.94/6.36 % (316926)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2006808682:i=14155:bd=all_2966 on theBenchmark for (2966ds/14155Mi)
% 33.94/6.36 % (316904)Instruction limit reached!
% 33.94/6.36 % (316904)------------------------------
% 33.94/6.36 % (316904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316904)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316904)Termination reason: Instruction limit
% 33.94/6.36 % (316904)Termination phase: Saturation
% 33.94/6.36 % (316904)Time elapsed: 3.176 s
% 33.94/6.36 % (316904)Peak memory usage: 175 MB
% 33.94/6.36 % (316904)Instructions burned: 5203 (million)
% 33.94/6.36 % (316928)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4027379037:i=667:av=off:fsr=off_2953 on theBenchmark for (2953ds/667Mi)
% 33.94/6.36 % (316911)First to succeed.
% 33.94/6.36 % (316911)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-316860"
% 33.94/6.36 % (316928)Instruction limit reached!
% 33.94/6.36 % (316928)------------------------------
% 33.94/6.36 % (316928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316928)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316928)Termination reason: Instruction limit
% 33.94/6.36 % (316928)Termination phase: Saturation
% 33.94/6.36 % (316928)Time elapsed: 0.336 s
% 33.94/6.36 % (316928)Peak memory usage: 107 MB
% 33.94/6.36 % (316928)Instructions burned: 667 (million)
% 33.94/6.36 % (316930)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=3615326337:s2a=on:i=185:s2at=1.8:fdi=4_2948 on theBenchmark for (2948ds/185Mi)
% 33.94/6.36 % (316930)Instruction limit reached!
% 33.94/6.36 % (316930)------------------------------
% 33.94/6.36 % (316930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.94/6.36 % (316930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.94/6.36 % (316930)CaDiCaL version: 2.1.3
% 33.94/6.36 % (316930)Termination reason: Instruction limit
% 33.94/6.36 % (316930)Termination phase: NewCNF
% 33.94/6.36 % (316930)Time elapsed: 0.129 s
% 33.94/6.36 % (316930)Peak memory usage: 101 MB
% 33.94/6.36 % (316930)Instructions burned: 186 (million)
% 33.94/6.36 % (316911)Refutation found. Thanks to Tanya!
% 33.94/6.36 % SZS status Theorem for theBenchmark
% 33.94/6.36 % SZS output start Proof for theBenchmark
% See solution above
% 37.89/6.56 % (316911)------------------------------
% 37.89/6.56 % (316911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.89/6.56 % (316911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.89/6.56 % (316911)CaDiCaL version: 2.1.3
% 37.89/6.56 % (316911)Termination reason: Refutation
% 37.89/6.56 % (316911)Time elapsed: 3.015 s
% 37.89/6.56 % (316911)Peak memory usage: 188 MB
% 37.89/6.56 % (316911)Instructions burned: 4911 (million)
% 37.89/6.56 % (316911)------------------------------
% 37.89/6.56 % (316911)------------------------------
% 37.89/6.56 % (316860)Success in time 5.498 s
% 37.89/6.56 % Vampire exiting
%------------------------------------------------------------------------------