%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG219+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 8.31s 2.22s
% Output : Refutation 9.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 13
% Syntax : Number of formulae : 254 ( 45 unt; 9 def)
% Number of atoms : 2853 ( 54 equ)
% Maximal formula atoms : 28 ( 11 avg)
% Number of connectives : 4608 (2009 ~;2395 |; 178 &)
% ( 9 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 13 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 10 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(f3171,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/sandbox/benchmark/theBenchmark.p',t32_rmod_2) ).
fof(f3237,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/sandbox/benchmark/theBenchmark.p',dt_m1_rmod_2) ).
fof(f3457,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/sandbox/benchmark/theBenchmark.p',t13_rmod_5) ).
fof(f3458,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/sandbox/benchmark/theBenchmark.p',t14_rmod_5) ).
fof(f3459,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)],[f3458]) ).
fof(f3514,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,[],[f3457]) ).
fof(f3515,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,[],[f3514]) ).
fof(f3516,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,[],[f3459]) ).
fof(f3517,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,[],[f3516]) ).
fof(f3555,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,[],[f3237]) ).
fof(f3556,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,[],[f3555]) ).
fof(f3561,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,[],[f3171]) ).
fof(f3562,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,[],[f3561]) ).
fof(f3658,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)],[f3517]) ).
fof(f3727,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,[],[f3515]) ).
fof(f3728,plain,
l3_vectsp_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3729,plain,
v2_vectsp_2(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3730,plain,
~ v10_vectsp_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3731,plain,
v8_vectsp_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3732,plain,
v7_vectsp_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3733,plain,
v6_vectsp_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3734,plain,
v7_group_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3735,plain,
v4_group_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3736,plain,
v6_rlvect_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3737,plain,
v5_rlvect_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3738,plain,
v4_rlvect_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3739,plain,
v3_rlvect_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3740,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3741,plain,
l1_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3742,plain,
v5_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3743,plain,
v3_vectsp_2(sK3,sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3744,plain,
v6_rlvect_1(sK3),
inference(cnf_transformation,[],[f3658]) ).
fof(f3745,plain,
v5_rlvect_1(sK3),
inference(cnf_transformation,[],[f3658]) ).
fof(f3746,plain,
v4_rlvect_1(sK3),
inference(cnf_transformation,[],[f3658]) ).
fof(f3747,plain,
v3_rlvect_1(sK3),
inference(cnf_transformation,[],[f3658]) ).
fof(f3748,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f3658]) ).
fof(f3749,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK3))),
inference(cnf_transformation,[],[f3658]) ).
fof(f3750,plain,
sK4 = u1_struct_0(sK3),
inference(cnf_transformation,[],[f3658]) ).
fof(f3751,plain,
sK3 != k1_rmod_5(sK2,sK3,sK4),
inference(cnf_transformation,[],[f3658]) ).
fof(f3752,plain,
k1_rlvect_1(sK2) != k2_group_1(sK2),
inference(cnf_transformation,[],[f3658]) ).
fof(f3836,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,[],[f3556]) ).
fof(f3837,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,[],[f3556]) ).
fof(f3838,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,[],[f3556]) ).
fof(f3839,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,[],[f3556]) ).
fof(f3840,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,[],[f3556]) ).
fof(f3841,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,[],[f3556]) ).
fof(f3842,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,[],[f3556]) ).
fof(f3845,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,[],[f3562]) ).
fof(f3931,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,[],[f3727]) ).
fof(f3963,definition,
( spl41_1
<=> v10_vectsp_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl41_1])],[avatar_definition]) ).
fof(f3965,plain,
( ~ v10_vectsp_1(sK2)
| spl41_1 ),
inference(avatar_component_clause,[],[f3963]) ).
fof(f3966,plain,
~ spl41_1,
inference(avatar_split_clause,[],[f3730,f3963]) ).
fof(f3968,definition,
( spl41_2
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl41_2])],[avatar_definition]) ).
fof(f3970,plain,
( ~ v3_struct_0(sK3)
| spl41_2 ),
inference(avatar_component_clause,[],[f3968]) ).
fof(f3971,plain,
~ spl41_2,
inference(avatar_split_clause,[],[f3748,f3968]) ).
fof(f3973,definition,
( spl41_3
<=> v3_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl41_3])],[avatar_definition]) ).
fof(f3975,plain,
( ~ v3_struct_0(sK2)
| spl41_3 ),
inference(avatar_component_clause,[],[f3973]) ).
fof(f3976,plain,
~ spl41_3,
inference(avatar_split_clause,[],[f3740,f3973]) ).
fof(f3978,definition,
( spl41_4
<=> sK3 = k1_rmod_5(sK2,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl41_4])],[avatar_definition]) ).
fof(f3980,plain,
( sK3 != k1_rmod_5(sK2,sK3,sK4)
| spl41_4 ),
inference(avatar_component_clause,[],[f3978]) ).
fof(f3981,plain,
~ spl41_4,
inference(avatar_split_clause,[],[f3751,f3978]) ).
fof(f4005,definition,
( spl41_5
<=> l1_vectsp_2(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl41_5])],[avatar_definition]) ).
fof(f4007,plain,
( l1_vectsp_2(sK3,sK2)
| ~ spl41_5 ),
inference(avatar_component_clause,[],[f4005]) ).
fof(f4008,plain,
spl41_5,
inference(avatar_split_clause,[],[f3741,f4005]) ).
fof(f4047,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) )
| ~ spl41_5 ),
inference(resolution,[],[f4007,f3836]) ).
fof(f4048,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) )
| ~ spl41_5 ),
inference(resolution,[],[f4007,f3837]) ).
fof(f4049,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) )
| ~ spl41_5 ),
inference(resolution,[],[f4007,f3838]) ).
fof(f4050,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) )
| ~ spl41_5 ),
inference(resolution,[],[f4007,f3839]) ).
fof(f4051,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) )
| ~ spl41_5 ),
inference(resolution,[],[f4007,f3840]) ).
fof(f4052,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) )
| ~ spl41_5 ),
inference(resolution,[],[f4007,f3841]) ).
fof(f4053,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) )
| ~ spl41_5 ),
inference(resolution,[],[f4007,f3842]) ).
fof(f4058,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)
| ~ spl41_5 ),
inference(resolution,[],[f4007,f3845]) ).
fof(f4165,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)
| spl41_2
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4058,f3970]) ).
fof(f4170,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4053,f3975]) ).
fof(f4171,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4052,f3975]) ).
fof(f4172,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4051,f3975]) ).
fof(f4173,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4050,f3975]) ).
fof(f4174,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4049,f3975]) ).
fof(f4175,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4048,f3975]) ).
fof(f4176,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4047,f3975]) ).
fof(f4268,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)
| spl41_2
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4165,f3747]) ).
fof(f4273,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4170,f3739]) ).
fof(f4274,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4171,f3739]) ).
fof(f4275,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4172,f3739]) ).
fof(f4276,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4173,f3739]) ).
fof(f4277,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4174,f3739]) ).
fof(f4278,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4175,f3739]) ).
fof(f4279,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4176,f3739]) ).
fof(f4371,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)
| spl41_2
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4268,f3746]) ).
fof(f4376,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4273,f3738]) ).
fof(f4377,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4274,f3738]) ).
fof(f4378,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4275,f3738]) ).
fof(f4379,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4276,f3738]) ).
fof(f4380,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4277,f3738]) ).
fof(f4381,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4278,f3738]) ).
fof(f4382,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4279,f3738]) ).
fof(f4474,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)
| spl41_2
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4371,f3745]) ).
fof(f4479,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4376,f3737]) ).
fof(f4480,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4377,f3737]) ).
fof(f4481,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4378,f3737]) ).
fof(f4482,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4379,f3737]) ).
fof(f4483,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4380,f3737]) ).
fof(f4484,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4381,f3737]) ).
fof(f4485,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4382,f3737]) ).
fof(f4577,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)
| spl41_2
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4474,f3744]) ).
fof(f4582,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4479,f3736]) ).
fof(f4583,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4480,f3736]) ).
fof(f4584,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4481,f3736]) ).
fof(f4585,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4482,f3736]) ).
fof(f4586,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4483,f3736]) ).
fof(f4587,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4484,f3736]) ).
fof(f4588,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4485,f3736]) ).
fof(f4680,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)
| spl41_2
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4577,f3742]) ).
fof(f4685,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4582,f3735]) ).
fof(f4686,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4583,f3735]) ).
fof(f4687,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4584,f3735]) ).
fof(f4688,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4585,f3735]) ).
fof(f4689,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4586,f3735]) ).
fof(f4690,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4587,f3735]) ).
fof(f4691,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4588,f3735]) ).
fof(f4783,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)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4680,f3975]) ).
fof(f4788,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4685,f3733]) ).
fof(f4789,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4686,f3733]) ).
fof(f4790,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4687,f3733]) ).
fof(f4791,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4688,f3733]) ).
fof(f4792,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4689,f3733]) ).
fof(f4793,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4690,f3733]) ).
fof(f4794,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4691,f3733]) ).
fof(f4886,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)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4783,f3739]) ).
fof(f4891,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4788,f3732]) ).
fof(f4892,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4789,f3732]) ).
fof(f4893,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4790,f3732]) ).
fof(f4894,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4791,f3732]) ).
fof(f4895,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4792,f3732]) ).
fof(f4896,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4793,f3732]) ).
fof(f4897,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4794,f3732]) ).
fof(f4989,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)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4886,f3738]) ).
fof(f4994,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4891,f3731]) ).
fof(f4995,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4892,f3731]) ).
fof(f4996,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4893,f3731]) ).
fof(f4997,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4894,f3731]) ).
fof(f4998,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4895,f3731]) ).
fof(f4999,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4896,f3731]) ).
fof(f5000,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4897,f3731]) ).
fof(f5092,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)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4989,f3737]) ).
fof(f5097,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4994,f3728]) ).
fof(f5098,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4995,f3728]) ).
fof(f5099,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4996,f3728]) ).
fof(f5100,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4997,f3728]) ).
fof(f5101,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4998,f3728]) ).
fof(f5102,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f4999,f3728]) ).
fof(f5103,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) )
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5000,f3728]) ).
fof(f5195,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)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5092,f3736]) ).
fof(f5200,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5097,f3970]) ).
fof(f5201,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5098,f3970]) ).
fof(f5202,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5099,f3970]) ).
fof(f5203,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5100,f3970]) ).
fof(f5204,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5101,f3970]) ).
fof(f5205,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5102,f3970]) ).
fof(f5206,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5103,f3970]) ).
fof(f5298,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v6_vectsp_1(sK2)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5195,f3735]) ).
fof(f5303,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5200,f3747]) ).
fof(f5304,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5201,f3747]) ).
fof(f5305,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5202,f3747]) ).
fof(f5306,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5203,f3747]) ).
fof(f5307,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5204,f3747]) ).
fof(f5308,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5205,f3747]) ).
fof(f5309,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5206,f3747]) ).
fof(f5401,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5298,f3733]) ).
fof(f5406,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5303,f3746]) ).
fof(f5407,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5304,f3746]) ).
fof(f5408,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5305,f3746]) ).
fof(f5409,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5306,f3746]) ).
fof(f5410,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5307,f3746]) ).
fof(f5411,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5308,f3746]) ).
fof(f5412,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) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5309,f3746]) ).
fof(f5504,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ v8_vectsp_1(sK2)
| ~ l3_vectsp_1(sK2)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5401,f3732]) ).
fof(f5509,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5406,f3745]) ).
fof(f5510,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5407,f3745]) ).
fof(f5511,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5408,f3745]) ).
fof(f5512,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5409,f3745]) ).
fof(f5513,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5410,f3745]) ).
fof(f5514,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5411,f3745]) ).
fof(f5515,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v6_rlvect_1(sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5412,f3745]) ).
fof(f5607,plain,
( m1_rmod_2(sK3,sK2,sK3)
| ~ l3_vectsp_1(sK2)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5504,f3731]) ).
fof(f5612,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5509,f3744]) ).
fof(f5613,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5510,f3744]) ).
fof(f5614,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5511,f3744]) ).
fof(f5615,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5512,f3744]) ).
fof(f5616,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5513,f3744]) ).
fof(f5617,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5514,f3744]) ).
fof(f5618,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3)
| ~ v5_vectsp_2(sK3,sK2) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5515,f3744]) ).
fof(f5710,plain,
( m1_rmod_2(sK3,sK2,sK3)
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5607,f3728]) ).
fof(f5715,plain,
( ! [X0] :
( ~ v3_struct_0(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5612,f3742]) ).
fof(f5716,plain,
( ! [X0] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5613,f3742]) ).
fof(f5717,plain,
( ! [X0] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5614,f3742]) ).
fof(f5718,plain,
( ! [X0] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5615,f3742]) ).
fof(f5719,plain,
( ! [X0] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5616,f3742]) ).
fof(f5720,plain,
( ! [X0] :
( v5_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5617,f3742]) ).
fof(f5721,plain,
( ! [X0] :
( l1_vectsp_2(X0,sK2)
| ~ m1_rmod_2(X0,sK2,sK3) )
| spl41_2
| spl41_3
| ~ spl41_5 ),
inference(forward_subsumption_resolution,[],[f5618,f3742]) ).
fof(f6828,definition,
( spl41_7
<=> sK4 = u1_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl41_7])],[avatar_definition]) ).
fof(f6830,plain,
( sK4 = u1_struct_0(sK3)
| ~ spl41_7 ),
inference(avatar_component_clause,[],[f6828]) ).
fof(f6831,plain,
spl41_7,
inference(avatar_split_clause,[],[f3750,f6828]) ).
fof(f6906,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) )
| ~ spl41_7 ),
inference(superposition,[],[f3931,f6830]) ).
fof(f7258,definition,
( spl41_8
<=> v3_vectsp_2(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl41_8])],[avatar_definition]) ).
fof(f7260,plain,
( v3_vectsp_2(sK3,sK2)
| ~ spl41_8 ),
inference(avatar_component_clause,[],[f7258]) ).
fof(f7261,plain,
spl41_8,
inference(avatar_split_clause,[],[f3743,f7258]) ).
fof(f7496,definition,
( spl41_9
<=> k1_rlvect_1(sK2) = k2_group_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl41_9])],[avatar_definition]) ).
fof(f7498,plain,
( k1_rlvect_1(sK2) != k2_group_1(sK2)
| spl41_9 ),
inference(avatar_component_clause,[],[f7496]) ).
fof(f7499,plain,
~ spl41_9,
inference(avatar_split_clause,[],[f3752,f7496]) ).
fof(f7576,definition,
( spl41_10
<=> ! [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,[spl41_10])],[avatar_definition]) ).
fof(f7577,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) )
| ~ spl41_10 ),
inference(avatar_component_clause,[],[f7576]) ).
fof(f7578,plain,
( spl41_10
| ~ spl41_7 ),
inference(avatar_split_clause,[],[f6906,f6828,f7576]) ).
fof(f7591,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)
| spl41_4
| ~ spl41_10 ),
inference(superposition,[],[f3980,f7577]) ).
fof(f7592,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)
| spl41_4
| ~ spl41_10 ),
inference(trivial_inequality_removal,[],[f7591]) ).
fof(f7605,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7592,f5715]) ).
fof(f7609,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7605,f5716]) ).
fof(f7610,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7609,f5717]) ).
fof(f7611,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7610,f5718]) ).
fof(f7612,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7611,f5719]) ).
fof(f7613,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7612,f5720]) ).
fof(f7614,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7613,f5721]) ).
fof(f7615,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7614,f7498]) ).
fof(f7616,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7615,f3749]) ).
fof(f7617,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7616,f7260]) ).
fof(f7618,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7617,f5710]) ).
fof(f7619,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7618,f3975]) ).
fof(f7620,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7619,f3739]) ).
fof(f7621,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7620,f3738]) ).
fof(f7622,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7621,f3737]) ).
fof(f7623,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7622,f3736]) ).
fof(f7624,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7623,f3735]) ).
fof(f7625,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)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7624,f3734]) ).
fof(f7626,plain,
( ~ v7_vectsp_1(sK2)
| ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7625,f3733]) ).
fof(f7627,plain,
( ~ v8_vectsp_1(sK2)
| v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7626,f3732]) ).
fof(f7628,plain,
( v10_vectsp_1(sK2)
| ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7627,f3731]) ).
fof(f7629,plain,
( ~ v2_vectsp_2(sK2)
| ~ l3_vectsp_1(sK2)
| spl41_1
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7628,f3965]) ).
fof(f7630,plain,
( ~ l3_vectsp_1(sK2)
| spl41_1
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7629,f3729]) ).
fof(f7631,plain,
( $false
| spl41_1
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(forward_subsumption_resolution,[],[f7630,f3728]) ).
fof(f7632,plain,
( spl41_1
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(avatar_contradiction_clause,[],[f7631]) ).
cnf(s1,plain,
~ spl41_1,
inference(sat_conversion,[],[f3966]) ).
cnf(s2,plain,
~ spl41_2,
inference(sat_conversion,[],[f3971]) ).
cnf(s3,plain,
~ spl41_3,
inference(sat_conversion,[],[f3976]) ).
cnf(s4,plain,
~ spl41_4,
inference(sat_conversion,[],[f3981]) ).
cnf(s5,plain,
spl41_5,
inference(sat_conversion,[],[f4008]) ).
cnf(s7,plain,
spl41_7,
inference(sat_conversion,[],[f6831]) ).
cnf(s8,plain,
spl41_8,
inference(sat_conversion,[],[f7261]) ).
cnf(s9,plain,
~ spl41_9,
inference(sat_conversion,[],[f7499]) ).
cnf(s10,plain,
( ~ spl41_7
| spl41_10 ),
inference(sat_conversion,[],[f7578]) ).
cnf(s11,plain,
( spl41_1
| spl41_2
| spl41_3
| spl41_4
| ~ spl41_5
| ~ spl41_8
| spl41_9
| ~ spl41_10 ),
inference(sat_conversion,[],[f7632]) ).
cnf(s12,plain,
spl41_10,
inference(rat,[],[s10,s7]) ).
cnf(s13,plain,
spl41_1,
inference(rat,[],[s11,s12,s9,s8,s5,s4,s3,s2]) ).
cnf(s14,plain,
$false,
inference(rat,[],[s1,s13]) ).
fof(f7633,plain,
$false,
inference(avatar_sat_refutation,[],[s14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG219+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 % Computer : n008.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.24 % CPULimit : 300
% 0.09/0.24 % WCLimit : 300
% 0.09/0.24 % DateTime : Mon Sep 28 19:47:25 UTC 2026
% 0.09/0.24 % CPUTime :
% 0.09/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.29 Running first-order theorem proving
% 0.24/0.29 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.31/2.22 % (2558022)Detected formulas, will run a generic FOF schedule.
% 8.31/2.22 % (2558029)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=2542132109:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 8.31/2.22 % (2558031)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3250541579:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 8.31/2.22 % (2558033)dis-21_1_sil=8000:lcm=predicate:random_seed=2974441872:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 8.31/2.22 % (2558027)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=4265542956:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 8.31/2.22 % (2558032)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1200395588:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 8.31/2.22 % (2558030)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=742802061:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 8.31/2.22 % (2558028)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=1792979456:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 8.31/2.22 % (2558030)Refutation not found, incomplete strategy
% 8.31/2.22 % (2558030)------------------------------
% 8.31/2.22 % (2558030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/2.22 % (2558030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/2.22 % (2558030)CaDiCaL version: 2.1.3
% 8.31/2.22 % (2558030)Termination reason: Refutation not found, incomplete strategy
% 8.31/2.22 % (2558030)Time elapsed: 0.046 s
% 8.31/2.22 % (2558030)Peak memory usage: 93 MB
% 8.31/2.22 % (2558030)Instructions burned: 45 (million)
% 8.31/2.22 % (2558031)Instruction limit reached!
% 8.31/2.22 % (2558031)------------------------------
% 8.31/2.22 % (2558031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/2.22 % (2558031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/2.22 % (2558031)CaDiCaL version: 2.1.3
% 8.31/2.22 % (2558031)Termination reason: Instruction limit
% 8.31/2.22 % (2558031)Termination phase: Saturation
% 8.31/2.22 % (2558031)Time elapsed: 0.109 s
% 8.31/2.22 % (2558031)Peak memory usage: 94 MB
% 8.31/2.22 % (2558031)Instructions burned: 120 (million)
% 8.31/2.22 % (2558033)Instruction limit reached!
% 8.31/2.22 % (2558033)------------------------------
% 8.31/2.22 % (2558033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/2.22 % (2558033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/2.22 % (2558033)CaDiCaL version: 2.1.3
% 8.31/2.22 % (2558033)Termination reason: Instruction limit
% 8.31/2.22 % (2558033)Termination phase: Property scanning
% 8.31/2.22 % (2558033)Time elapsed: 0.135 s
% 8.31/2.22 % (2558033)Peak memory usage: 94 MB
% 8.31/2.22 % (2558033)Instructions burned: 129 (million)
% 8.31/2.22 % (2558032)Instruction limit reached!
% 8.31/2.22 % (2558032)------------------------------
% 8.31/2.22 % (2558032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/2.22 % (2558032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/2.22 % (2558032)CaDiCaL version: 2.1.3
% 8.31/2.22 % (2558032)Termination reason: Instruction limit
% 8.31/2.22 % (2558032)Termination phase: Preprocessing 3
% 8.31/2.22 % (2558032)Time elapsed: 0.142 s
% 8.31/2.22 % (2558032)Peak memory usage: 94 MB
% 8.31/2.22 % (2558032)Instructions burned: 139 (million)
% 8.31/2.22 % (2558041)lrs+10_1_sil=8000:sp=occurrence:random_seed=2887384833:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 8.31/2.22 % (2558042)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3805365242:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 8.31/2.22 % (2558043)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2632130862:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 8.31/2.22 % (2558030)------------------------------
% 8.31/2.22 % (2558030)------------------------------
% 8.31/2.22 % (2558042)Instruction limit reached!
% 8.31/2.22 % (2558042)------------------------------
% 8.31/2.22 % (2558042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/2.22 % (2558042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/2.22 % (2558042)CaDiCaL version: 2.1.3
% 8.31/2.22 % (2558042)Termination reason: Instruction limit
% 8.31/2.22 % (2558042)Termination phase: Saturation
% 8.31/2.22 % (2558042)Time elapsed: 0.140 s
% 8.31/2.22 % (2558042)Peak memory usage: 93 MB
% 8.31/2.22 % (2558042)Instructions burned: 157 (million)
% 8.31/2.22 % (2558041)Instruction limit reached!
% 8.31/2.22 % (2558041)------------------------------
% 8.31/2.22 % (2558041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/2.22 % (2558041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/2.22 % (2558041)CaDiCaL version: 2.1.3
% 8.31/2.22 % (2558041)Termination reason: Instruction limit
% 8.31/2.22 % (2558041)Termination phase: Saturation
% 8.31/2.22 % (2558041)Time elapsed: 0.274 s
% 8.31/2.22 % (2558041)Peak memory usage: 96 MB
% 8.31/2.22 % (2558041)Instructions burned: 286 (million)
% 8.31/2.22 % (2558043)Instruction limit reached!
% 8.31/2.22 % (2558043)------------------------------
% 8.31/2.22 % (2558043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/2.22 % (2558043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/2.22 % (2558043)CaDiCaL version: 2.1.3
% 8.31/2.22 % (2558043)Termination reason: Instruction limit
% 8.31/2.22 % (2558043)Termination phase: Saturation
% 8.31/2.22 % (2558043)Time elapsed: 0.294 s
% 8.31/2.22 % (2558043)Peak memory usage: 95 MB
% 8.31/2.22 % (2558043)Instructions burned: 326 (million)
% 8.31/2.22 % (2558047)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=3569112880:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 8.31/2.22 % (2558029)First to succeed.
% 8.31/2.22 % (2558029)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2558022"
% 8.31/2.22 % (2558048)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2772919337:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 8.31/2.22 % (2558049)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2221674145:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 8.31/2.22 % (2558047)Instruction limit reached!
% 8.31/2.22 % (2558047)------------------------------
% 8.31/2.22 % (2558047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/2.22 % (2558047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/2.22 % (2558047)CaDiCaL version: 2.1.3
% 8.31/2.22 % (2558047)Termination reason: Instruction limit
% 8.31/2.22 % (2558047)Termination phase: Function definition elimination
% 8.31/2.22 % (2558047)Time elapsed: 0.232 s
% 8.31/2.22 % (2558047)Peak memory usage: 96 MB
% 8.31/2.22 % (2558047)Instructions burned: 249 (million)
% 8.31/2.22 % (2558048)Also succeeded, but the first one will report.
% 8.31/2.22 % (2558029)Refutation found. Thanks to Tanya!
% 8.31/2.22 % SZS status Theorem for theBenchmark
% 8.31/2.22 % SZS output start Proof for theBenchmark
% See solution above
% 9.92/2.48 % (2558029)------------------------------
% 9.92/2.48 % (2558029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.92/2.48 % (2558029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.92/2.48 % (2558029)CaDiCaL version: 2.1.3
% 9.92/2.48 % (2558029)Termination reason: Refutation
% 9.92/2.48 % (2558029)Time elapsed: 0.803 s
% 9.92/2.48 % (2558029)Peak memory usage: 139 MB
% 9.92/2.48 % (2558029)Instructions burned: 1488 (million)
% 9.92/2.48 % (2558029)------------------------------
% 9.92/2.48 % (2558029)------------------------------
% 9.92/2.48 % (2558022)Success in time 1.43 s
% 9.92/2.48 % Vampire exiting
%------------------------------------------------------------------------------