%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG219+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.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 09:19:24 AM UTC 2026
% Result : Theorem 9.54s 2.56s
% Output : Refutation 11.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 12
% Syntax : Number of formulae : 250 ( 43 unt; 8 def)
% Number of atoms : 2828 ( 52 equ)
% Maximal formula atoms : 28 ( 11 avg)
% Number of connectives : 4584 (2006 ~;2375 |; 178 &)
% ( 8 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 13 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 9 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 194 ( 0 sgn 188 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9718,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> m1_rmod_2(X1,X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_rmod_2) ).
fof(f9784,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0)
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_rmod_2(X2,X0,X1)
=> ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X0)
& l1_vectsp_2(X2,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_rmod_2) ).
fof(f10004,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ! [X3] :
( ( v3_vectsp_2(X3,X0)
& m1_rmod_2(X3,X0,X1) )
=> ( X2 = u1_struct_0(X3)
=> ( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_rmod_5) ).
fof(f10005,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( X2 = u1_struct_0(X1)
=> ( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t14_rmod_5) ).
fof(f10006,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( X2 = u1_struct_0(X1)
=> ( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X1 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f10005]) ).
fof(f10060,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X3
| u1_struct_0(X3) != X2
| ~ v3_vectsp_2(X3,X0)
| ~ m1_rmod_2(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v10_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f10004]) ).
fof(f10061,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X3
| u1_struct_0(X3) != X2
| ~ v3_vectsp_2(X3,X0)
| ~ m1_rmod_2(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v10_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0) ),
inference(flattening,[],[f10060]) ).
fof(f10062,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_rlvect_1(X0) != k2_group_1(X0)
& k1_rmod_5(X0,X1,X2) != X1
& X2 = u1_struct_0(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f10006]) ).
fof(f10063,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_rlvect_1(X0) != k2_group_1(X0)
& k1_rmod_5(X0,X1,X2) != X1
& X2 = u1_struct_0(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) ),
inference(flattening,[],[f10062]) ).
fof(f10098,plain,
! [X0,X1] :
( ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X0)
& l1_vectsp_2(X2,X0) )
| ~ m1_rmod_2(X2,X0,X1) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(ennf_transformation,[],[f9784]) ).
fof(f10099,plain,
! [X0,X1] :
( ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v5_vectsp_2(X2,X0)
& l1_vectsp_2(X2,X0) )
| ~ m1_rmod_2(X2,X0,X1) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(flattening,[],[f10098]) ).
fof(f10106,plain,
! [X0] :
( ! [X1] :
( m1_rmod_2(X1,X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f9718]) ).
fof(f10107,plain,
! [X0] :
( ! [X1] :
( m1_rmod_2(X1,X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(flattening,[],[f10106]) ).
fof(f10235,plain,
( k1_rlvect_1(sK2) != k2_group_1(sK2)
& sK3 != k1_rmod_5(sK2,sK3,sK4)
& sK4 = u1_struct_0(sK3)
& m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
& ~ v3_struct_0(sK3)
& v3_rlvect_1(sK3)
& v4_rlvect_1(sK3)
& v5_rlvect_1(sK3)
& v6_rlvect_1(sK3)
& v3_vectsp_2(sK3,sK2)
& v5_vectsp_2(sK3,sK2)
& l1_vectsp_2(sK3,sK2)
& ~ v3_struct_0(sK2)
& v3_rlvect_1(sK2)
& v4_rlvect_1(sK2)
& v5_rlvect_1(sK2)
& v6_rlvect_1(sK2)
& v4_group_1(sK2)
& v7_group_1(sK2)
& v6_vectsp_1(sK2)
& v7_vectsp_1(sK2)
& v8_vectsp_1(sK2)
& ~ v10_vectsp_1(sK2)
& v2_vectsp_2(sK2)
& l3_vectsp_1(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f10063]) ).
fof(f10312,plain,
! [X2,X3,X0,X1] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X3
| u1_struct_0(X3) != X2
| ~ v3_vectsp_2(X3,X0)
| ~ m1_rmod_2(X3,X0,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v10_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f10061]) ).
fof(f10313,plain,
l3_vectsp_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10314,plain,
v2_vectsp_2(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10315,plain,
~ v10_vectsp_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10316,plain,
v8_vectsp_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10317,plain,
v7_vectsp_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10318,plain,
v6_vectsp_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10319,plain,
v7_group_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10320,plain,
v4_group_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10321,plain,
v6_rlvect_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10322,plain,
v5_rlvect_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10323,plain,
v4_rlvect_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10324,plain,
v3_rlvect_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10325,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10326,plain,
l1_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10327,plain,
v5_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10328,plain,
v3_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10329,plain,
v6_rlvect_1(sK3),
inference(cnf_transformation,[],[f10235]) ).
fof(f10330,plain,
v5_rlvect_1(sK3),
inference(cnf_transformation,[],[f10235]) ).
fof(f10331,plain,
v4_rlvect_1(sK3),
inference(cnf_transformation,[],[f10235]) ).
fof(f10332,plain,
v3_rlvect_1(sK3),
inference(cnf_transformation,[],[f10235]) ).
fof(f10333,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f10235]) ).
fof(f10334,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3))),
inference(cnf_transformation,[],[f10235]) ).
fof(f10335,plain,
sK4 = u1_struct_0(sK3),
inference(cnf_transformation,[],[f10235]) ).
fof(f10336,plain,
sK3 != k1_rmod_5(sK2,sK3,sK4),
inference(cnf_transformation,[],[f10235]) ).
fof(f10337,plain,
k1_rlvect_1(sK2) != k2_group_1(sK2),
inference(cnf_transformation,[],[f10235]) ).
fof(f10415,plain,
! [X2,X0,X1] :
( l1_vectsp_2(X2,X0)
| ~ m1_rmod_2(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(cnf_transformation,[],[f10099]) ).
fof(f10416,plain,
! [X2,X0,X1] :
( v5_vectsp_2(X2,X0)
| ~ m1_rmod_2(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(cnf_transformation,[],[f10099]) ).
fof(f10417,plain,
! [X2,X0,X1] :
( v6_rlvect_1(X2)
| ~ m1_rmod_2(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(cnf_transformation,[],[f10099]) ).
fof(f10418,plain,
! [X2,X0,X1] :
( v5_rlvect_1(X2)
| ~ m1_rmod_2(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(cnf_transformation,[],[f10099]) ).
fof(f10419,plain,
! [X2,X0,X1] :
( v4_rlvect_1(X2)
| ~ m1_rmod_2(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(cnf_transformation,[],[f10099]) ).
fof(f10420,plain,
! [X2,X0,X1] :
( v3_rlvect_1(X2)
| ~ m1_rmod_2(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(cnf_transformation,[],[f10099]) ).
fof(f10421,plain,
! [X2,X0,X1] :
( ~ v3_struct_0(X2)
| ~ m1_rmod_2(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) ),
inference(cnf_transformation,[],[f10099]) ).
fof(f10427,plain,
! [X0,X1] :
( m1_rmod_2(X1,X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f10107]) ).
fof(f10562,plain,
! [X3,X0,X1] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,u1_struct_0(X3)) = X3
| ~ v3_vectsp_2(X3,X0)
| ~ m1_rmod_2(X3,X0,X1)
| ~ m1_subset_1(u1_struct_0(X3),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v10_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0) ),
inference(equality_resolution,[],[f10312]) ).
fof(f10613,definition,
( spl52_1
<=> v10_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl52_1])],[avatar_definition]) ).
fof(f10615,plain,
( ~ v10_vectsp_1(sK2)
| spl52_1 ),
inference(avatar_component_clause,[],[f10613]) ).
fof(f10616,plain,
~ spl52_1,
inference(avatar_split_clause,[],[f10315,f10613]) ).
fof(f10618,definition,
( spl52_2
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl52_2])],[avatar_definition]) ).
fof(f10620,plain,
( ~ v3_struct_0(sK3)
| spl52_2 ),
inference(avatar_component_clause,[],[f10618]) ).
fof(f10621,plain,
~ spl52_2,
inference(avatar_split_clause,[],[f10333,f10618]) ).
fof(f10623,definition,
( spl52_3
<=> v3_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl52_3])],[avatar_definition]) ).
fof(f10625,plain,
( ~ v3_struct_0(sK2)
| spl52_3 ),
inference(avatar_component_clause,[],[f10623]) ).
fof(f10626,plain,
~ spl52_3,
inference(avatar_split_clause,[],[f10325,f10623]) ).
fof(f10628,definition,
( spl52_4
<=> v3_vectsp_2(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl52_4])],[avatar_definition]) ).
fof(f10630,plain,
( v3_vectsp_2(sK3,sK2)
| ~ spl52_4 ),
inference(avatar_component_clause,[],[f10628]) ).
fof(f10631,plain,
spl52_4,
inference(avatar_split_clause,[],[f10328,f10628]) ).
fof(f10922,definition,
( spl52_5
<=> sK3 = k1_rmod_5(sK2,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl52_5])],[avatar_definition]) ).
fof(f10924,plain,
( sK3 != k1_rmod_5(sK2,sK3,sK4)
| spl52_5 ),
inference(avatar_component_clause,[],[f10922]) ).
fof(f10925,plain,
~ spl52_5,
inference(avatar_split_clause,[],[f10336,f10922]) ).
fof(f10949,definition,
( spl52_6
<=> l1_vectsp_2(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl52_6])],[avatar_definition]) ).
fof(f10951,plain,
( l1_vectsp_2(sK3,sK2)
| ~ spl52_6 ),
inference(avatar_component_clause,[],[f10949]) ).
fof(f10952,plain,
spl52_6,
inference(avatar_split_clause,[],[f10326,f10949]) ).
fof(f10991,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| ~ spl52_6 ),
inference(resolution,[],[f10951,f10415]) ).
fof(f10992,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| ~ spl52_6 ),
inference(resolution,[],[f10951,f10416]) ).
fof(f10993,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| ~ spl52_6 ),
inference(resolution,[],[f10951,f10417]) ).
fof(f10994,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| ~ spl52_6 ),
inference(resolution,[],[f10951,f10418]) ).
fof(f10995,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| ~ spl52_6 ),
inference(resolution,[],[f10951,f10419]) ).
fof(f10996,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| ~ spl52_6 ),
inference(resolution,[],[f10951,f10420]) ).
fof(f10997,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| ~ spl52_6 ),
inference(resolution,[],[f10951,f10421]) ).
fof(f11005,plain,
( m1_rmod_2(sK3,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| ~ spl52_6 ),
inference(resolution,[],[f10951,f10427]) ).
fof(f11118,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11005,f10620]) ).
fof(f11126,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f10997,f10625]) ).
fof(f11127,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f10996,f10625]) ).
fof(f11128,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f10995,f10625]) ).
fof(f11129,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f10994,f10625]) ).
fof(f11130,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f10993,f10625]) ).
fof(f11131,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f10992,f10625]) ).
fof(f11132,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f10991,f10625]) ).
fof(f11224,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11118,f10332]) ).
fof(f11232,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11126,f10324]) ).
fof(f11233,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11127,f10324]) ).
fof(f11234,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11128,f10324]) ).
fof(f11235,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11129,f10324]) ).
fof(f11236,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11130,f10324]) ).
fof(f11237,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11131,f10324]) ).
fof(f11238,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11132,f10324]) ).
fof(f11330,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11224,f10331]) ).
fof(f11338,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11232,f10323]) ).
fof(f11339,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11233,f10323]) ).
fof(f11340,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11234,f10323]) ).
fof(f11341,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11235,f10323]) ).
fof(f11342,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11236,f10323]) ).
fof(f11343,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11237,f10323]) ).
fof(f11344,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11238,f10323]) ).
fof(f11436,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11330,f10330]) ).
fof(f11444,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11338,f10322]) ).
fof(f11445,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11339,f10322]) ).
fof(f11446,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11340,f10322]) ).
fof(f11447,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11341,f10322]) ).
fof(f11448,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11342,f10322]) ).
fof(f11449,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11343,f10322]) ).
fof(f11450,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11344,f10322]) ).
fof(f11542,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11436,f10329]) ).
fof(f11550,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11444,f10321]) ).
fof(f11551,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11445,f10321]) ).
fof(f11552,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11446,f10321]) ).
fof(f11553,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11447,f10321]) ).
fof(f11554,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11448,f10321]) ).
fof(f11555,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11449,f10321]) ).
fof(f11556,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11450,f10321]) ).
fof(f11648,plain,
( m1_rmod_2(sK3,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11542,f10327]) ).
fof(f11656,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11550,f10320]) ).
fof(f11657,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11551,f10320]) ).
fof(f11658,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11552,f10320]) ).
fof(f11659,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11553,f10320]) ).
fof(f11660,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11554,f10320]) ).
fof(f11661,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11555,f10320]) ).
fof(f11662,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11556,f10320]) ).
fof(f11754,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11648,f10625]) ).
fof(f11762,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11656,f10318]) ).
fof(f11763,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11657,f10318]) ).
fof(f11764,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11658,f10318]) ).
fof(f11765,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11659,f10318]) ).
fof(f11766,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11660,f10318]) ).
fof(f11767,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11661,f10318]) ).
fof(f11768,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11662,f10318]) ).
fof(f11860,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11754,f10324]) ).
fof(f11868,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11762,f10317]) ).
fof(f11869,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11763,f10317]) ).
fof(f11870,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11764,f10317]) ).
fof(f11871,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11765,f10317]) ).
fof(f11872,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11766,f10317]) ).
fof(f11873,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11767,f10317]) ).
fof(f11874,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11768,f10317]) ).
fof(f11966,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11860,f10323]) ).
fof(f11974,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11868,f10316]) ).
fof(f11975,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11869,f10316]) ).
fof(f11976,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11870,f10316]) ).
fof(f11977,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11871,f10316]) ).
fof(f11978,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11872,f10316]) ).
fof(f11979,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11873,f10316]) ).
fof(f11980,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11874,f10316]) ).
fof(f12072,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11966,f10322]) ).
fof(f12080,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11974,f10313]) ).
fof(f12081,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11975,f10313]) ).
fof(f12082,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11976,f10313]) ).
fof(f12083,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11977,f10313]) ).
fof(f12084,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11978,f10313]) ).
fof(f12085,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11979,f10313]) ).
fof(f12086,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f11980,f10313]) ).
fof(f12178,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v4_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12072,f10321]) ).
fof(f12186,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12080,f10620]) ).
fof(f12187,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12081,f10620]) ).
fof(f12188,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12082,f10620]) ).
fof(f12189,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12083,f10620]) ).
fof(f12190,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12084,f10620]) ).
fof(f12191,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12085,f10620]) ).
fof(f12192,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12086,f10620]) ).
fof(f12284,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12178,f10320]) ).
fof(f12292,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12186,f10332]) ).
fof(f12293,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12187,f10332]) ).
fof(f12294,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12188,f10332]) ).
fof(f12295,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12189,f10332]) ).
fof(f12296,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12190,f10332]) ).
fof(f12297,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12191,f10332]) ).
fof(f12298,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12192,f10332]) ).
fof(f12390,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12284,f10318]) ).
fof(f12398,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12292,f10331]) ).
fof(f12399,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12293,f10331]) ).
fof(f12400,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12294,f10331]) ).
fof(f12401,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12295,f10331]) ).
fof(f12402,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12296,f10331]) ).
fof(f12403,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12297,f10331]) ).
fof(f12404,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12298,f10331]) ).
fof(f12496,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12390,f10317]) ).
fof(f12504,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12398,f10330]) ).
fof(f12505,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12399,f10330]) ).
fof(f12506,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12400,f10330]) ).
fof(f12507,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12401,f10330]) ).
fof(f12508,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12402,f10330]) ).
fof(f12509,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12403,f10330]) ).
fof(f12510,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12404,f10330]) ).
fof(f12602,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12496,f10316]) ).
fof(f12610,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12504,f10329]) ).
fof(f12611,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12505,f10329]) ).
fof(f12612,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12506,f10329]) ).
fof(f12613,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12507,f10329]) ).
fof(f12614,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12508,f10329]) ).
fof(f12615,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12509,f10329]) ).
fof(f12616,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12510,f10329]) ).
fof(f12708,plain,
( m1_rmod_2(sK3,sK2,sK3)
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12602,f10313]) ).
fof(f12716,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12610,f10327]) ).
fof(f12717,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12611,f10327]) ).
fof(f12718,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12612,f10327]) ).
fof(f12719,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12613,f10327]) ).
fof(f12720,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12614,f10327]) ).
fof(f12721,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12615,f10327]) ).
fof(f12722,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl52_2
| spl52_3
| ~ spl52_6 ),
inference(forward_subsumption_resolution,[],[f12616,f10327]) ).
fof(f12889,definition,
( spl52_7
<=> sK4 = u1_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl52_7])],[avatar_definition]) ).
fof(f12891,plain,
( sK4 = u1_struct_0(sK3)
| ~ spl52_7 ),
inference(avatar_component_clause,[],[f12889]) ).
fof(f12892,plain,
spl52_7,
inference(avatar_split_clause,[],[f10335,f12889]) ).
fof(f12979,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(X0)))
| k1_rlvect_1(X1) = k2_group_1(X1)
| sK3 = k1_rmod_5(X1,X0,sK4)
| ~ v3_vectsp_2(sK3,X1)
| ~ m1_rmod_2(sK3,X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,X1)
| ~ l1_vectsp_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) )
| ~ spl52_7 ),
inference(superposition,[],[f10562,f12891]) ).
fof(f13383,definition,
( spl52_8
<=> ! [X0,X1] :
( ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(X0)))
| k1_rlvect_1(X1) = k2_group_1(X1)
| sK3 = k1_rmod_5(X1,X0,sK4)
| ~ v3_vectsp_2(sK3,X1)
| ~ m1_rmod_2(sK3,X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,X1)
| ~ l1_vectsp_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl52_8])],[avatar_definition]) ).
fof(f13384,plain,
( ! [X0,X1] :
( sK3 = k1_rmod_5(X1,X0,sK4)
| k1_rlvect_1(X1) = k2_group_1(X1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_vectsp_2(sK3,X1)
| ~ m1_rmod_2(sK3,X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,X1)
| ~ l1_vectsp_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) )
| ~ spl52_8 ),
inference(avatar_component_clause,[],[f13383]) ).
fof(f13385,plain,
( spl52_8
| ~ spl52_7 ),
inference(avatar_split_clause,[],[f12979,f12889,f13383]) ).
fof(f13398,plain,
( sK3 != sK3
| k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_5
| ~ spl52_8 ),
inference(superposition,[],[f10924,f13384]) ).
fof(f13399,plain,
( k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_5
| ~ spl52_8 ),
inference(trivial_inequality_removal,[],[f13398]) ).
fof(f13412,plain,
( k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13399,f12716]) ).
fof(f13416,plain,
( k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13412,f12717]) ).
fof(f13417,plain,
( k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13416,f12718]) ).
fof(f13418,plain,
( k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13417,f12719]) ).
fof(f13419,plain,
( k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13418,f12720]) ).
fof(f13420,plain,
( k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| ~ l1_vectsp_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13419,f12721]) ).
fof(f13421,plain,
( k1_rlvect_1(sK2) = k2_group_1(sK2)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13420,f12722]) ).
fof(f13422,plain,
( ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13421,f10337]) ).
fof(f13423,plain,
( ~ v3_vectsp_2(sK3,sK2)
| ~ m1_rmod_2(sK3,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13422,f10334]) ).
fof(f13424,plain,
( ~ m1_rmod_2(sK3,sK2,sK3)
| v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13423,f10630]) ).
fof(f13425,plain,
( v3_struct_0(sK2)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13424,f12708]) ).
fof(f13426,plain,
( ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13425,f10625]) ).
fof(f13427,plain,
( ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13426,f10324]) ).
fof(f13428,plain,
( ~ v5_rlvect_1(sK2)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13427,f10323]) ).
fof(f13429,plain,
( ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13428,f10322]) ).
fof(f13430,plain,
( ~ v4_group_1(sK2)
| ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13429,f10321]) ).
fof(f13431,plain,
( ~ v7_group_1(sK2)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13430,f10320]) ).
fof(f13432,plain,
( ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13431,f10319]) ).
fof(f13433,plain,
( ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13432,f10318]) ).
fof(f13434,plain,
( ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13433,f10317]) ).
fof(f13435,plain,
( v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13434,f10316]) ).
fof(f13436,plain,
( ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl52_1
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13435,f10615]) ).
fof(f13437,plain,
( ~ l3_vectsp_1(sK2)
| spl52_1
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13436,f10314]) ).
fof(f13438,plain,
( $false
| spl52_1
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(forward_subsumption_resolution,[],[f13437,f10313]) ).
fof(f13439,plain,
( spl52_1
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(avatar_contradiction_clause,[],[f13438]) ).
cnf(s1,plain,
~ spl52_1,
inference(sat_conversion,[],[f10616]) ).
cnf(s2,plain,
~ spl52_2,
inference(sat_conversion,[],[f10621]) ).
cnf(s3,plain,
~ spl52_3,
inference(sat_conversion,[],[f10626]) ).
cnf(s4,plain,
spl52_4,
inference(sat_conversion,[],[f10631]) ).
cnf(s5,plain,
~ spl52_5,
inference(sat_conversion,[],[f10925]) ).
cnf(s6,plain,
spl52_6,
inference(sat_conversion,[],[f10952]) ).
cnf(s7,plain,
spl52_7,
inference(sat_conversion,[],[f12892]) ).
cnf(s8,plain,
( ~ spl52_7
| spl52_8 ),
inference(sat_conversion,[],[f13385]) ).
cnf(s9,plain,
( spl52_1
| spl52_2
| spl52_3
| ~ spl52_4
| spl52_5
| ~ spl52_6
| ~ spl52_8 ),
inference(sat_conversion,[],[f13439]) ).
cnf(s10,plain,
spl52_8,
inference(rat,[],[s8,s7]) ).
cnf(s11,plain,
spl52_1,
inference(rat,[],[s9,s10,s6,s5,s4,s3,s2]) ).
cnf(s12,plain,
$false,
inference(rat,[],[s1,s11]) ).
fof(f13440,plain,
$false,
inference(avatar_sat_refutation,[],[s12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG219+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n013.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:46:08 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 9.54/2.56 % (1490521)Detected formulas, will run a generic FOF schedule.
% 9.54/2.56 % (1490527)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=1610004664:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 9.54/2.56 % (1490528)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=3860177905:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 9.54/2.56 % (1490530)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2796528766:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 9.54/2.56 % (1490531)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1751039965:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 9.54/2.56 % (1490526)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=3470601723:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 9.54/2.56 % (1490529)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1277521249:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 9.54/2.56 % (1490532)dis-21_1_sil=8000:lcm=predicate:random_seed=1752464855:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 9.54/2.56 % (1490529)Refutation not found, incomplete strategy
% 9.54/2.56 % (1490529)------------------------------
% 9.54/2.56 % (1490529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490529)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490529)Termination reason: Refutation not found, incomplete strategy
% 9.54/2.56 % (1490529)Time elapsed: 0.054 s
% 9.54/2.56 % (1490529)Peak memory usage: 101 MB
% 9.54/2.56 % (1490529)Instructions burned: 74 (million)
% 9.54/2.56 % (1490531)Instruction limit reached!
% 9.54/2.56 % (1490531)------------------------------
% 9.54/2.56 % (1490531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490531)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490531)Termination reason: Instruction limit
% 9.54/2.56 % (1490531)Termination phase: SInE selection
% 9.54/2.56 % (1490531)Time elapsed: 0.066 s
% 9.54/2.56 % (1490531)Peak memory usage: 96 MB
% 9.54/2.56 % (1490531)Instructions burned: 139 (million)
% 9.54/2.56 % (1490530)Instruction limit reached!
% 9.54/2.56 % (1490530)------------------------------
% 9.54/2.56 % (1490530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490530)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490530)Termination reason: Instruction limit
% 9.54/2.56 % (1490530)Termination phase: Preprocessing 3
% 9.54/2.56 % (1490530)Time elapsed: 0.090 s
% 9.54/2.56 % (1490530)Peak memory usage: 100 MB
% 9.54/2.56 % (1490530)Instructions burned: 120 (million)
% 9.54/2.56 % (1490532)Instruction limit reached!
% 9.54/2.56 % (1490532)------------------------------
% 9.54/2.56 % (1490532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490532)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490532)Termination reason: Instruction limit
% 9.54/2.56 % (1490532)Termination phase: Unused predicate definition removal
% 9.54/2.56 % (1490532)Time elapsed: 0.102 s
% 9.54/2.56 % (1490532)Peak memory usage: 98 MB
% 9.54/2.56 % (1490532)Instructions burned: 129 (million)
% 9.54/2.56 % (1490540)lrs+10_1_sil=8000:sp=occurrence:random_seed=831361487:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 9.54/2.56 % (1490541)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3532644365:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/157Mi)
% 9.54/2.56 % (1490542)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1378357962:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi)
% 9.54/2.56 % (1490529)------------------------------
% 9.54/2.56 % (1490529)------------------------------
% 9.54/2.56 % (1490541)Instruction limit reached!
% 9.54/2.56 % (1490541)------------------------------
% 9.54/2.56 % (1490541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490541)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490541)Termination reason: Instruction limit
% 9.54/2.56 % (1490541)Termination phase: SInE selection
% 9.54/2.56 % (1490541)Time elapsed: 0.077 s
% 9.54/2.56 % (1490541)Peak memory usage: 97 MB
% 9.54/2.56 % (1490541)Instructions burned: 157 (million)
% 9.54/2.56 % (1490540)Instruction limit reached!
% 9.54/2.56 % (1490540)------------------------------
% 9.54/2.56 % (1490540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490540)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490540)Termination reason: Instruction limit
% 9.54/2.56 % (1490540)Termination phase: Saturation
% 9.54/2.56 % (1490540)Time elapsed: 0.198 s
% 9.54/2.56 % (1490540)Peak memory usage: 105 MB
% 9.54/2.56 % (1490540)Instructions burned: 285 (million)
% 9.54/2.56 % (1490547)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=1184465055:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 9.54/2.56 % (1490548)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3548501879:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 9.54/2.56 % (1490542)Instruction limit reached!
% 9.54/2.56 % (1490542)------------------------------
% 9.54/2.56 % (1490542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490542)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490542)Termination reason: Instruction limit
% 9.54/2.56 % (1490542)Termination phase: Saturation
% 9.54/2.56 % (1490542)Time elapsed: 0.208 s
% 9.54/2.56 % (1490542)Peak memory usage: 104 MB
% 9.54/2.56 % (1490542)Instructions burned: 325 (million)
% 9.54/2.56 % (1490549)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3397560:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 9.54/2.56 % (1490547)Instruction limit reached!
% 9.54/2.56 % (1490547)------------------------------
% 9.54/2.56 % (1490547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490547)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490547)Termination reason: Instruction limit
% 9.54/2.56 % (1490547)Termination phase: Preprocessing 1
% 9.54/2.56 % (1490547)Time elapsed: 0.139 s
% 9.54/2.56 % (1490547)Peak memory usage: 98 MB
% 9.54/2.56 % (1490547)Instructions burned: 249 (million)
% 9.54/2.56 % (1490548)Instruction limit reached!
% 9.54/2.56 % (1490548)------------------------------
% 9.54/2.56 % (1490548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490548)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490548)Termination reason: Instruction limit
% 9.54/2.56 % (1490548)Termination phase: Saturation
% 9.54/2.56 % (1490548)Time elapsed: 0.175 s
% 9.54/2.56 % (1490548)Peak memory usage: 105 MB
% 9.54/2.56 % (1490548)Instructions burned: 295 (million)
% 9.54/2.56 % (1490552)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1515067307:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 9.54/2.56 % (1490552)Instruction limit reached!
% 9.54/2.56 % (1490552)------------------------------
% 9.54/2.56 % (1490552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490552)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490552)Termination reason: Instruction limit
% 9.54/2.56 % (1490552)Termination phase: Preprocessing 3
% 9.54/2.56 % (1490552)Time elapsed: 0.093 s
% 9.54/2.56 % (1490552)Peak memory usage: 101 MB
% 9.54/2.56 % (1490552)Instructions burned: 114 (million)
% 9.54/2.56 % (1490554)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=826303488:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 9.54/2.56 % (1490555)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=542730516:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 9.54/2.56 % (1490555)Instruction limit reached!
% 9.54/2.56 % (1490555)------------------------------
% 9.54/2.56 % (1490555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490555)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490555)Termination reason: Instruction limit
% 9.54/2.56 % (1490555)Termination phase: Property scanning
% 9.54/2.56 % (1490555)Time elapsed: 0.049 s
% 9.54/2.56 % (1490555)Peak memory usage: 97 MB
% 9.54/2.56 % (1490555)Instructions burned: 117 (million)
% 9.54/2.56 % (1490554)Instruction limit reached!
% 9.54/2.56 % (1490554)------------------------------
% 9.54/2.56 % (1490554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/2.56 % (1490554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/2.56 % (1490554)CaDiCaL version: 2.1.3
% 9.54/2.56 % (1490554)Termination reason: Instruction limit
% 9.54/2.56 % (1490554)Termination phase: Naming
% 9.54/2.56 % (1490554)Time elapsed: 0.101 s
% 9.54/2.56 % (1490554)Peak memory usage: 106 MB
% 9.54/2.56 % (1490554)Instructions burned: 128 (million)
% 9.54/2.56 % (1490558)lrs+10_1_sil=8000:sp=occurrence:random_seed=1678749160:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 9.54/2.56 % (1490528)First to succeed.
% 9.54/2.56 % (1490528)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1490521"
% 9.54/2.56 % (1490560)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=211229551:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 9.54/2.56 % (1490561)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1043015741:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 9.54/2.56 % (1490560)Also succeeded, but the first one will report.
% 9.54/2.56 % (1490528)Refutation found. Thanks to Tanya!
% 9.54/2.56 % SZS status Theorem for theBenchmark
% 9.54/2.56 % SZS output start Proof for theBenchmark
% See solution above
% 11.13/2.79 % (1490528)------------------------------
% 11.13/2.79 % (1490528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.79 % (1490528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.79 % (1490528)CaDiCaL version: 2.1.3
% 11.13/2.79 % (1490528)Termination reason: Refutation
% 11.13/2.79 % (1490528)Time elapsed: 0.986 s
% 11.13/2.79 % (1490528)Peak memory usage: 150 MB
% 11.13/2.79 % (1490528)Instructions burned: 1544 (million)
% 11.13/2.79 % (1490528)------------------------------
% 11.13/2.79 % (1490528)------------------------------
% 11.13/2.79 % (1490521)Success in time 1.885 s
% 11.13/2.79 % Vampire exiting
%------------------------------------------------------------------------------