%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG220+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:25 AM UTC 2026
% Result : Theorem 17.32s 6.24s
% Output : Refutation 34.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 32
% Syntax : Number of formulae : 318 ( 78 unt; 27 def)
% Number of atoms : 3641 ( 51 equ)
% Maximal formula atoms : 31 ( 11 avg)
% Number of connectives : 5974 (2651 ~;3060 |; 214 &)
% ( 27 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 13 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 28 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 297 ( 0 sgn 289 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24228,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)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_rlvect_1(X2)
& v4_rlvect_1(X2)
& v5_rlvect_1(X2)
& v6_rlvect_1(X2)
& v3_vectsp_2(X2,X0)
& v5_vectsp_2(X2,X0)
& l1_vectsp_2(X2,X0) )
=> ( ( m1_rmod_2(X2,X0,X1)
& m1_rmod_2(X1,X0,X2) )
=> X2 = X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_rmod_2) ).
fof(f24293,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(f24498,axiom,
! [X0,X1,X2] :
( ( ~ 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)
& ~ 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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> ( v3_vectsp_2(k1_rmod_5(X0,X1,X2),X0)
& m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_rmod_5) ).
fof(f24515,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] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ( r1_tarski(X2,X3)
=> m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,k1_rmod_5(X0,X1,X3)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_rmod_5) ).
fof(f24516,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)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ( ( k1_rmod_5(X0,X1,X2) = X1
& r1_tarski(X2,X3) )
=> k1_rmod_5(X0,X1,X3) = X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_rmod_5) ).
fof(f24517,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)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ( ( k1_rmod_5(X0,X1,X2) = X1
& r1_tarski(X2,X3) )
=> k1_rmod_5(X0,X1,X3) = X1 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f24516]) ).
fof(f24543,plain,
! [X0,X1,X2] :
( ( v3_vectsp_2(k1_rmod_5(X0,X1,X2),X0)
& m1_rmod_2(k1_rmod_5(X0,X1,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)
| ~ 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)
| 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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(ennf_transformation,[],[f24498]) ).
fof(f24544,plain,
! [X0,X1,X2] :
( ( v3_vectsp_2(k1_rmod_5(X0,X1,X2),X0)
& m1_rmod_2(k1_rmod_5(X0,X1,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)
| ~ 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)
| 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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(flattening,[],[f24543]) ).
fof(f24571,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,k1_rmod_5(X0,X1,X3))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(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)
| ~ 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,[],[f24515]) ).
fof(f24572,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,k1_rmod_5(X0,X1,X3))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(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)
| ~ 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,[],[f24571]) ).
fof(f24573,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k1_rmod_5(X0,X1,X3) != X1
& k1_rmod_5(X0,X1,X2) = X1
& r1_tarski(X2,X3)
& m1_subset_1(X3,k1_zfmisc_1(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,[],[f24517]) ).
fof(f24574,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k1_rmod_5(X0,X1,X3) != X1
& k1_rmod_5(X0,X1,X2) = X1
& r1_tarski(X2,X3)
& m1_subset_1(X3,k1_zfmisc_1(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,[],[f24573]) ).
fof(f24602,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = X1
| ~ m1_rmod_2(X2,X0,X1)
| ~ m1_rmod_2(X1,X0,X2)
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v3_vectsp_2(X2,X0)
| ~ v5_vectsp_2(X2,X0)
| ~ l1_vectsp_2(X2,X0) )
| 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)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f24228]) ).
fof(f24603,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = X1
| ~ m1_rmod_2(X2,X0,X1)
| ~ m1_rmod_2(X1,X0,X2)
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v3_vectsp_2(X2,X0)
| ~ v5_vectsp_2(X2,X0)
| ~ l1_vectsp_2(X2,X0) )
| 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)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(flattening,[],[f24602]) ).
fof(f24614,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,[],[f24293]) ).
fof(f24615,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,[],[f24614]) ).
fof(f24784,plain,
( sK4 != k1_rmod_5(sK3,sK4,sK6)
& sK4 = k1_rmod_5(sK3,sK4,sK5)
& r1_tarski(sK5,sK6)
& m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4)))
& m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4)))
& ~ v3_struct_0(sK4)
& v3_rlvect_1(sK4)
& v4_rlvect_1(sK4)
& v5_rlvect_1(sK4)
& v6_rlvect_1(sK4)
& v3_vectsp_2(sK4,sK3)
& v5_vectsp_2(sK4,sK3)
& l1_vectsp_2(sK4,sK3)
& ~ v3_struct_0(sK3)
& v3_rlvect_1(sK3)
& v4_rlvect_1(sK3)
& v5_rlvect_1(sK3)
& v6_rlvect_1(sK3)
& v4_group_1(sK3)
& v7_group_1(sK3)
& v6_vectsp_1(sK3)
& v7_vectsp_1(sK3)
& v8_vectsp_1(sK3)
& ~ v10_vectsp_1(sK3)
& v2_vectsp_2(sK3)
& l3_vectsp_1(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6)],[f24574]) ).
fof(f24846,plain,
! [X2,X0,X1] :
( m1_rmod_2(k1_rmod_5(X0,X1,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)
| ~ 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)
| 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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f24544]) ).
fof(f24847,plain,
! [X2,X0,X1] :
( v3_vectsp_2(k1_rmod_5(X0,X1,X2),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)
| 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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f24544]) ).
fof(f24869,plain,
! [X2,X3,X0,X1] :
( m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,k1_rmod_5(X0,X1,X3))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(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)
| ~ 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,[],[f24572]) ).
fof(f24870,plain,
l3_vectsp_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24871,plain,
v2_vectsp_2(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24872,plain,
~ v10_vectsp_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24873,plain,
v8_vectsp_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24874,plain,
v7_vectsp_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24875,plain,
v6_vectsp_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24876,plain,
v7_group_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24877,plain,
v4_group_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24878,plain,
v6_rlvect_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24879,plain,
v5_rlvect_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24880,plain,
v4_rlvect_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24881,plain,
v3_rlvect_1(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24882,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24883,plain,
l1_vectsp_2(sK4,sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24884,plain,
v5_vectsp_2(sK4,sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24885,plain,
v3_vectsp_2(sK4,sK3),
inference(cnf_transformation,[],[f24784]) ).
fof(f24886,plain,
v6_rlvect_1(sK4),
inference(cnf_transformation,[],[f24784]) ).
fof(f24887,plain,
v5_rlvect_1(sK4),
inference(cnf_transformation,[],[f24784]) ).
fof(f24888,plain,
v4_rlvect_1(sK4),
inference(cnf_transformation,[],[f24784]) ).
fof(f24889,plain,
v3_rlvect_1(sK4),
inference(cnf_transformation,[],[f24784]) ).
fof(f24890,plain,
~ v3_struct_0(sK4),
inference(cnf_transformation,[],[f24784]) ).
fof(f24891,plain,
m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4))),
inference(cnf_transformation,[],[f24784]) ).
fof(f24892,plain,
m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4))),
inference(cnf_transformation,[],[f24784]) ).
fof(f24893,plain,
r1_tarski(sK5,sK6),
inference(cnf_transformation,[],[f24784]) ).
fof(f24894,plain,
sK4 = k1_rmod_5(sK3,sK4,sK5),
inference(cnf_transformation,[],[f24784]) ).
fof(f24895,plain,
sK4 != k1_rmod_5(sK3,sK4,sK6),
inference(cnf_transformation,[],[f24784]) ).
fof(f24947,plain,
! [X2,X0,X1] :
( X1 = X2
| ~ m1_rmod_2(X2,X0,X1)
| ~ m1_rmod_2(X1,X0,X2)
| v3_struct_0(X2)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v3_vectsp_2(X2,X0)
| ~ v5_vectsp_2(X2,X0)
| ~ l1_vectsp_2(X2,X0)
| 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)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f24603]) ).
fof(f24977,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,[],[f24615]) ).
fof(f24978,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,[],[f24615]) ).
fof(f24979,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,[],[f24615]) ).
fof(f24980,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,[],[f24615]) ).
fof(f24981,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,[],[f24615]) ).
fof(f24982,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,[],[f24615]) ).
fof(f24983,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,[],[f24615]) ).
fof(f25278,definition,
( spl66_1
<=> v10_vectsp_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_1])],[avatar_definition]) ).
fof(f25280,plain,
( ~ v10_vectsp_1(sK3)
| spl66_1 ),
inference(avatar_component_clause,[],[f25278]) ).
fof(f25281,plain,
~ spl66_1,
inference(avatar_split_clause,[],[f24872,f25278]) ).
fof(f25283,definition,
( spl66_2
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_2])],[avatar_definition]) ).
fof(f25285,plain,
( ~ v3_struct_0(sK3)
| spl66_2 ),
inference(avatar_component_clause,[],[f25283]) ).
fof(f25286,plain,
~ spl66_2,
inference(avatar_split_clause,[],[f24882,f25283]) ).
fof(f25288,definition,
( spl66_3
<=> v3_struct_0(sK4) ),
introduced(definition,[new_symbols(definition,[spl66_3])],[avatar_definition]) ).
fof(f25290,plain,
( ~ v3_struct_0(sK4)
| spl66_3 ),
inference(avatar_component_clause,[],[f25288]) ).
fof(f25291,plain,
~ spl66_3,
inference(avatar_split_clause,[],[f24890,f25288]) ).
fof(f25293,definition,
( spl66_4
<=> sK4 = k1_rmod_5(sK3,sK4,sK6) ),
introduced(definition,[new_symbols(definition,[spl66_4])],[avatar_definition]) ).
fof(f25295,plain,
( sK4 != k1_rmod_5(sK3,sK4,sK6)
| spl66_4 ),
inference(avatar_component_clause,[],[f25293]) ).
fof(f25296,plain,
~ spl66_4,
inference(avatar_split_clause,[],[f24895,f25293]) ).
fof(f25320,definition,
( spl66_5
<=> sK4 = k1_rmod_5(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl66_5])],[avatar_definition]) ).
fof(f25322,plain,
( sK4 = k1_rmod_5(sK3,sK4,sK5)
| ~ spl66_5 ),
inference(avatar_component_clause,[],[f25320]) ).
fof(f25323,plain,
spl66_5,
inference(avatar_split_clause,[],[f24894,f25320]) ).
fof(f25331,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4)))
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| ~ spl66_5 ),
inference(superposition,[],[f24869,f25322]) ).
fof(f25343,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25331,f24891]) ).
fof(f25354,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25343,f25290]) ).
fof(f25365,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25354,f24889]) ).
fof(f25376,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25365,f24888]) ).
fof(f25387,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25376,f24887]) ).
fof(f25398,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25387,f24886]) ).
fof(f25409,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25398,f24884]) ).
fof(f25420,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25409,f24883]) ).
fof(f25431,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25420,f25285]) ).
fof(f25442,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25431,f24881]) ).
fof(f25453,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25442,f24880]) ).
fof(f25464,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25453,f24879]) ).
fof(f25475,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25464,f24878]) ).
fof(f25486,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25475,f24877]) ).
fof(f25497,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25486,f24876]) ).
fof(f25508,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25497,f24875]) ).
fof(f25519,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25508,f24874]) ).
fof(f25530,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25519,f24873]) ).
fof(f25541,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25530,f25280]) ).
fof(f25552,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25541,f24871]) ).
fof(f25563,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(forward_subsumption_resolution,[],[f25552,f24870]) ).
fof(f25576,definition,
( spl66_6
<=> v3_vectsp_2(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl66_6])],[avatar_definition]) ).
fof(f25578,plain,
( v3_vectsp_2(sK4,sK3)
| ~ spl66_6 ),
inference(avatar_component_clause,[],[f25576]) ).
fof(f25579,plain,
spl66_6,
inference(avatar_split_clause,[],[f24885,f25576]) ).
fof(f25881,definition,
( spl66_7
<=> l1_vectsp_2(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl66_7])],[avatar_definition]) ).
fof(f25883,plain,
( l1_vectsp_2(sK4,sK3)
| ~ spl66_7 ),
inference(avatar_component_clause,[],[f25881]) ).
fof(f25884,plain,
spl66_7,
inference(avatar_split_clause,[],[f24883,f25881]) ).
fof(f25885,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| ~ spl66_7 ),
inference(resolution,[],[f25883,f24846]) ).
fof(f26106,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f25885,f25285]) ).
fof(f26214,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26106,f24881]) ).
fof(f26322,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26214,f24880]) ).
fof(f26430,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26322,f24879]) ).
fof(f26538,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26430,f24878]) ).
fof(f26646,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26538,f24877]) ).
fof(f26754,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26646,f24876]) ).
fof(f26862,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26754,f24875]) ).
fof(f26970,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26862,f24874]) ).
fof(f27078,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f26970,f24873]) ).
fof(f27186,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27078,f25280]) ).
fof(f27290,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27186,f24871]) ).
fof(f27394,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27290,f24870]) ).
fof(f27498,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27394,f25290]) ).
fof(f27602,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27498,f24889]) ).
fof(f27706,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27602,f24888]) ).
fof(f27721,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27706,f24887]) ).
fof(f27736,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27721,f24886]) ).
fof(f27750,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_7 ),
inference(forward_subsumption_resolution,[],[f27736,f24884]) ).
fof(f27766,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(resolution,[],[f25285,f24846]) ).
fof(f27768,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(resolution,[],[f25285,f24847]) ).
fof(f28264,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f27768,f24881]) ).
fof(f28266,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f27766,f24881]) ).
fof(f28512,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f28264,f24880]) ).
fof(f28514,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f28266,f24880]) ).
fof(f28760,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f28512,f24879]) ).
fof(f28762,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f28514,f24879]) ).
fof(f29008,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f28760,f24878]) ).
fof(f29010,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f28762,f24878]) ).
fof(f29148,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29008,f24877]) ).
fof(f29149,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29010,f24877]) ).
fof(f29287,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29148,f24876]) ).
fof(f29288,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29149,f24876]) ).
fof(f29421,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29287,f24875]) ).
fof(f29422,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29288,f24875]) ).
fof(f29555,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29421,f24874]) ).
fof(f29556,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29422,f24874]) ).
fof(f29689,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29555,f24873]) ).
fof(f29690,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29556,f24873]) ).
fof(f29708,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_1
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29689,f25280]) ).
fof(f29709,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_1
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29690,f25280]) ).
fof(f29724,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_1
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29708,f24871]) ).
fof(f29725,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,X0)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_1
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29709,f24871]) ).
fof(f29739,plain,
( ! [X0,X1] :
( v3_vectsp_2(k1_rmod_5(sK3,X0,X1),sK3)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_1
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29724,f24870]) ).
fof(f29740,plain,
( ! [X0,X1] :
( m1_rmod_2(k1_rmod_5(sK3,X0,X1),sK3,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,sK3)
| ~ l1_vectsp_2(X0,sK3)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| spl66_1
| spl66_2 ),
inference(forward_subsumption_resolution,[],[f29725,f24870]) ).
fof(f29840,plain,
( ! [X0,X1] :
( l1_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(resolution,[],[f25290,f24977]) ).
fof(f29842,plain,
( ! [X0,X1] :
( v5_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(resolution,[],[f25290,f24978]) ).
fof(f29844,plain,
( ! [X0,X1] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(resolution,[],[f25290,f24979]) ).
fof(f29846,plain,
( ! [X0,X1] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(resolution,[],[f25290,f24980]) ).
fof(f29848,plain,
( ! [X0,X1] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(resolution,[],[f25290,f24981]) ).
fof(f29850,plain,
( ! [X0,X1] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(resolution,[],[f25290,f24982]) ).
fof(f30154,plain,
( ! [X0,X1] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f29850,f24889]) ).
fof(f30156,plain,
( ! [X0,X1] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f29848,f24889]) ).
fof(f30158,plain,
( ! [X0,X1] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f29846,f24889]) ).
fof(f30160,plain,
( ! [X0,X1] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f29844,f24889]) ).
fof(f30162,plain,
( ! [X0,X1] :
( v5_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f29842,f24889]) ).
fof(f30164,plain,
( ! [X0,X1] :
( l1_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f29840,f24889]) ).
fof(f30404,plain,
( ! [X0,X1] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30154,f24888]) ).
fof(f30406,plain,
( ! [X0,X1] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30156,f24888]) ).
fof(f30408,plain,
( ! [X0,X1] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30158,f24888]) ).
fof(f30410,plain,
( ! [X0,X1] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30160,f24888]) ).
fof(f30412,plain,
( ! [X0,X1] :
( v5_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30162,f24888]) ).
fof(f30414,plain,
( ! [X0,X1] :
( l1_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30164,f24888]) ).
fof(f30654,plain,
( ! [X0,X1] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30404,f24887]) ).
fof(f30656,plain,
( ! [X0,X1] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30406,f24887]) ).
fof(f30658,plain,
( ! [X0,X1] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30408,f24887]) ).
fof(f30660,plain,
( ! [X0,X1] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30410,f24887]) ).
fof(f30662,plain,
( ! [X0,X1] :
( v5_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30412,f24887]) ).
fof(f30664,plain,
( ! [X0,X1] :
( l1_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30414,f24887]) ).
fof(f30902,plain,
( ! [X0,X1] :
( v3_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30654,f24886]) ).
fof(f30904,plain,
( ! [X0,X1] :
( v4_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30656,f24886]) ).
fof(f30906,plain,
( ! [X0,X1] :
( v5_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30658,f24886]) ).
fof(f30908,plain,
( ! [X0,X1] :
( v6_rlvect_1(X0)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30660,f24886]) ).
fof(f30910,plain,
( ! [X0,X1] :
( v5_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30662,f24886]) ).
fof(f30912,plain,
( ! [X0,X1] :
( l1_vectsp_2(X0,X1)
| ~ m1_rmod_2(X0,X1,sK4)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(sK4,X1)
| ~ l1_vectsp_2(sK4,X1) )
| spl66_3 ),
inference(forward_subsumption_resolution,[],[f30664,f24886]) ).
fof(f31041,definition,
( spl66_8
<=> v5_vectsp_2(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl66_8])],[avatar_definition]) ).
fof(f31043,plain,
( v5_vectsp_2(sK4,sK3)
| ~ spl66_8 ),
inference(avatar_component_clause,[],[f31041]) ).
fof(f31044,plain,
spl66_8,
inference(avatar_split_clause,[],[f24884,f31041]) ).
fof(f31167,definition,
( spl66_9
<=> l3_vectsp_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_9])],[avatar_definition]) ).
fof(f31169,plain,
( l3_vectsp_1(sK3)
| ~ spl66_9 ),
inference(avatar_component_clause,[],[f31167]) ).
fof(f31170,plain,
spl66_9,
inference(avatar_split_clause,[],[f24870,f31167]) ).
fof(f31192,definition,
( spl66_10
<=> r1_tarski(sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl66_10])],[avatar_definition]) ).
fof(f31194,plain,
( r1_tarski(sK5,sK6)
| ~ spl66_10 ),
inference(avatar_component_clause,[],[f31192]) ).
fof(f31195,plain,
spl66_10,
inference(avatar_split_clause,[],[f24893,f31192]) ).
fof(f31232,definition,
( spl66_11
<=> m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4))) ),
introduced(definition,[new_symbols(definition,[spl66_11])],[avatar_definition]) ).
fof(f31234,plain,
( m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ spl66_11 ),
inference(avatar_component_clause,[],[f31232]) ).
fof(f31235,plain,
spl66_11,
inference(avatar_split_clause,[],[f24892,f31232]) ).
fof(f31429,definition,
( spl66_12
<=> v4_group_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_12])],[avatar_definition]) ).
fof(f31431,plain,
( v4_group_1(sK3)
| ~ spl66_12 ),
inference(avatar_component_clause,[],[f31429]) ).
fof(f31432,plain,
spl66_12,
inference(avatar_split_clause,[],[f24877,f31429]) ).
fof(f31439,definition,
( spl66_14
<=> v7_vectsp_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_14])],[avatar_definition]) ).
fof(f31441,plain,
( v7_vectsp_1(sK3)
| ~ spl66_14 ),
inference(avatar_component_clause,[],[f31439]) ).
fof(f31442,plain,
spl66_14,
inference(avatar_split_clause,[],[f24874,f31439]) ).
fof(f31444,definition,
( spl66_15
<=> v3_rlvect_1(sK4) ),
introduced(definition,[new_symbols(definition,[spl66_15])],[avatar_definition]) ).
fof(f31446,plain,
( v3_rlvect_1(sK4)
| ~ spl66_15 ),
inference(avatar_component_clause,[],[f31444]) ).
fof(f31447,plain,
spl66_15,
inference(avatar_split_clause,[],[f24889,f31444]) ).
fof(f31749,definition,
( spl66_17
<=> v8_vectsp_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_17])],[avatar_definition]) ).
fof(f31751,plain,
( v8_vectsp_1(sK3)
| ~ spl66_17 ),
inference(avatar_component_clause,[],[f31749]) ).
fof(f31752,plain,
spl66_17,
inference(avatar_split_clause,[],[f24873,f31749]) ).
fof(f31754,definition,
( spl66_18
<=> v5_rlvect_1(sK4) ),
introduced(definition,[new_symbols(definition,[spl66_18])],[avatar_definition]) ).
fof(f31756,plain,
( v5_rlvect_1(sK4)
| ~ spl66_18 ),
inference(avatar_component_clause,[],[f31754]) ).
fof(f31757,plain,
spl66_18,
inference(avatar_split_clause,[],[f24887,f31754]) ).
fof(f31759,definition,
( spl66_19
<=> v6_rlvect_1(sK4) ),
introduced(definition,[new_symbols(definition,[spl66_19])],[avatar_definition]) ).
fof(f31761,plain,
( v6_rlvect_1(sK4)
| ~ spl66_19 ),
inference(avatar_component_clause,[],[f31759]) ).
fof(f31762,plain,
spl66_19,
inference(avatar_split_clause,[],[f24886,f31759]) ).
fof(f31907,definition,
( spl66_20
<=> v3_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_20])],[avatar_definition]) ).
fof(f31909,plain,
( v3_rlvect_1(sK3)
| ~ spl66_20 ),
inference(avatar_component_clause,[],[f31907]) ).
fof(f31910,plain,
spl66_20,
inference(avatar_split_clause,[],[f24881,f31907]) ).
fof(f31912,definition,
( spl66_21
<=> v5_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_21])],[avatar_definition]) ).
fof(f31914,plain,
( v5_rlvect_1(sK3)
| ~ spl66_21 ),
inference(avatar_component_clause,[],[f31912]) ).
fof(f31915,plain,
spl66_21,
inference(avatar_split_clause,[],[f24879,f31912]) ).
fof(f32071,definition,
( spl66_22
<=> v6_vectsp_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_22])],[avatar_definition]) ).
fof(f32073,plain,
( v6_vectsp_1(sK3)
| ~ spl66_22 ),
inference(avatar_component_clause,[],[f32071]) ).
fof(f32074,plain,
spl66_22,
inference(avatar_split_clause,[],[f24875,f32071]) ).
fof(f32076,definition,
( spl66_23
<=> v6_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_23])],[avatar_definition]) ).
fof(f32078,plain,
( v6_rlvect_1(sK3)
| ~ spl66_23 ),
inference(avatar_component_clause,[],[f32076]) ).
fof(f32079,plain,
spl66_23,
inference(avatar_split_clause,[],[f24878,f32076]) ).
fof(f32229,definition,
( spl66_25
<=> v4_rlvect_1(sK4) ),
introduced(definition,[new_symbols(definition,[spl66_25])],[avatar_definition]) ).
fof(f32231,plain,
( v4_rlvect_1(sK4)
| ~ spl66_25 ),
inference(avatar_component_clause,[],[f32229]) ).
fof(f32232,plain,
spl66_25,
inference(avatar_split_clause,[],[f24888,f32229]) ).
fof(f33961,definition,
( spl66_27
<=> v4_rlvect_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl66_27])],[avatar_definition]) ).
fof(f33963,plain,
( v4_rlvect_1(sK3)
| ~ spl66_27 ),
inference(avatar_component_clause,[],[f33961]) ).
fof(f33964,plain,
spl66_27,
inference(avatar_split_clause,[],[f24880,f33961]) ).
fof(f35412,definition,
( spl66_30
<=> ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) ) ),
introduced(definition,[new_symbols(definition,[spl66_30])],[avatar_definition]) ).
fof(f35413,plain,
( ! [X0] :
( m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| ~ spl66_30 ),
inference(avatar_component_clause,[],[f35412]) ).
fof(f35414,plain,
( spl66_30
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_7 ),
inference(avatar_split_clause,[],[f27750,f25881,f25288,f25283,f25278,f35412]) ).
fof(f35451,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| ~ spl66_30 ),
inference(resolution,[],[f35413,f24983]) ).
fof(f35539,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f35451,f25285]) ).
fof(f35615,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_20
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f35539,f31909]) ).
fof(f35690,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_20
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f35615,f33963]) ).
fof(f35765,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_20
| ~ spl66_21
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f35690,f31914]) ).
fof(f35840,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_20
| ~ spl66_21
| ~ spl66_23
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f35765,f32078]) ).
fof(f35915,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_12
| ~ spl66_20
| ~ spl66_21
| ~ spl66_23
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f35840,f31431]) ).
fof(f35990,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_12
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f35915,f32073]) ).
fof(f36065,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_12
| ~ spl66_14
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f35990,f31441]) ).
fof(f36140,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ l3_vectsp_1(sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_12
| ~ spl66_14
| ~ spl66_17
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36065,f31751]) ).
fof(f36215,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_17
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36140,f31169]) ).
fof(f36289,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| spl66_3
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_17
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36215,f25290]) ).
fof(f36359,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| spl66_3
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36289,f31446]) ).
fof(f36425,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| spl66_3
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36359,f32231]) ).
fof(f36491,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| spl66_3
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36425,f31756]) ).
fof(f36557,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| spl66_3
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36491,f31761]) ).
fof(f36623,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ l1_vectsp_2(sK4,sK3) )
| spl66_2
| spl66_3
| ~ spl66_8
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36557,f31043]) ).
fof(f36689,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0)) )
| spl66_2
| spl66_3
| ~ spl66_7
| ~ spl66_8
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_30 ),
inference(forward_subsumption_resolution,[],[f36623,f25883]) ).
fof(f37559,definition,
( spl66_44
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl66_44])],[avatar_definition]) ).
fof(f37560,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_struct_0(k1_rmod_5(sK3,sK4,X0)) )
| ~ spl66_44 ),
inference(avatar_component_clause,[],[f37559]) ).
fof(f37561,plain,
( spl66_44
| spl66_2
| spl66_3
| ~ spl66_7
| ~ spl66_8
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_30 ),
inference(avatar_split_clause,[],[f36689,f35412,f33961,f32229,f32076,f32071,f31912,f31907,f31759,f31754,f31749,f31444,f31439,f31429,f31167,f31041,f25881,f25288,f25283,f37559]) ).
fof(f37671,definition,
( spl66_51
<=> ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) ) ),
introduced(definition,[new_symbols(definition,[spl66_51])],[avatar_definition]) ).
fof(f37672,plain,
( ! [X0] :
( m1_rmod_2(sK4,sK3,k1_rmod_5(sK3,sK4,X0))
| ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) )
| ~ spl66_51 ),
inference(avatar_component_clause,[],[f37671]) ).
fof(f37673,plain,
( spl66_51
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_5 ),
inference(avatar_split_clause,[],[f25563,f25320,f25288,f25283,f25278,f37671]) ).
fof(f37687,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v3_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v4_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v5_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v6_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v3_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ v5_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| ~ spl66_51 ),
inference(resolution,[],[f37672,f24947]) ).
fof(f37797,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v4_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v5_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v6_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v3_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ v5_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f37687,f30902]) ).
fof(f37849,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v5_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v6_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v3_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ v5_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f37797,f30904]) ).
fof(f37901,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v6_rlvect_1(k1_rmod_5(sK3,sK4,X0))
| ~ v3_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ v5_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f37849,f30906]) ).
fof(f37953,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v3_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ v5_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f37901,f30908]) ).
fof(f38005,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v3_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f37953,f30910]) ).
fof(f38057,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ m1_rmod_2(k1_rmod_5(sK3,sK4,X0),sK3,sK4)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v3_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_3
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38005,f30912]) ).
fof(f38109,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| ~ v3_vectsp_2(k1_rmod_5(sK3,sK4,X0),sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38057,f29740]) ).
fof(f38161,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| v3_struct_0(k1_rmod_5(sK3,sK4,X0))
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38109,f29739]) ).
fof(f38213,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38161,f37560]) ).
fof(f38265,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38213,f25290]) ).
fof(f38316,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_15
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38265,f31446]) ).
fof(f38367,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_15
| ~ spl66_25
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38316,f32231]) ).
fof(f38414,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v6_rlvect_1(sK4)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_15
| ~ spl66_18
| ~ spl66_25
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38367,f31756]) ).
fof(f38461,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v3_vectsp_2(sK4,sK3)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_25
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38414,f31761]) ).
fof(f38508,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_25
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38461,f25578]) ).
fof(f38555,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_8
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_25
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38508,f31043]) ).
fof(f38602,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_25
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38555,f25883]) ).
fof(f38627,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_25
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38602,f25285]) ).
fof(f38644,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_25
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38627,f31909]) ).
fof(f38653,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38644,f33963]) ).
fof(f38659,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38653,f31914]) ).
fof(f38664,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v4_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38659,f32078]) ).
fof(f38668,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_12
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38664,f31431]) ).
fof(f38672,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_12
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38668,f32073]) ).
fof(f38675,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ v8_vectsp_1(sK3)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38672,f31441]) ).
fof(f38678,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ l3_vectsp_1(sK3) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38675,f31751]) ).
fof(f38681,plain,
( ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0) )
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(forward_subsumption_resolution,[],[f38678,f31169]) ).
fof(f38688,definition,
( spl66_52
<=> ! [X0] :
( ~ r1_tarski(sK5,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| sK4 = k1_rmod_5(sK3,sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl66_52])],[avatar_definition]) ).
fof(f38689,plain,
( ! [X0] :
( sK4 = k1_rmod_5(sK3,sK4,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ r1_tarski(sK5,X0) )
| ~ spl66_52 ),
inference(avatar_component_clause,[],[f38688]) ).
fof(f38690,plain,
( spl66_52
| spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51 ),
inference(avatar_split_clause,[],[f38681,f37671,f37559,f33961,f32229,f32076,f32071,f31912,f31907,f31759,f31754,f31749,f31444,f31439,f31429,f31167,f31041,f25881,f25576,f25288,f25283,f25278,f38688]) ).
fof(f38699,plain,
( sK4 != sK4
| ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ r1_tarski(sK5,sK6)
| spl66_4
| ~ spl66_52 ),
inference(superposition,[],[f25295,f38689]) ).
fof(f38729,plain,
( ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ r1_tarski(sK5,sK6)
| spl66_4
| ~ spl66_52 ),
inference(trivial_inequality_removal,[],[f38699]) ).
fof(f38748,plain,
( ~ r1_tarski(sK5,sK6)
| spl66_4
| ~ spl66_11
| ~ spl66_52 ),
inference(forward_subsumption_resolution,[],[f38729,f31234]) ).
fof(f38762,plain,
( $false
| spl66_4
| ~ spl66_10
| ~ spl66_11
| ~ spl66_52 ),
inference(forward_subsumption_resolution,[],[f38748,f31194]) ).
fof(f38763,plain,
( spl66_4
| ~ spl66_10
| ~ spl66_11
| ~ spl66_52 ),
inference(avatar_contradiction_clause,[],[f38762]) ).
cnf(s1,plain,
~ spl66_1,
inference(sat_conversion,[],[f25281]) ).
cnf(s2,plain,
~ spl66_2,
inference(sat_conversion,[],[f25286]) ).
cnf(s3,plain,
~ spl66_3,
inference(sat_conversion,[],[f25291]) ).
cnf(s4,plain,
~ spl66_4,
inference(sat_conversion,[],[f25296]) ).
cnf(s5,plain,
spl66_5,
inference(sat_conversion,[],[f25323]) ).
cnf(s6,plain,
spl66_6,
inference(sat_conversion,[],[f25579]) ).
cnf(s7,plain,
spl66_7,
inference(sat_conversion,[],[f25884]) ).
cnf(s8,plain,
spl66_8,
inference(sat_conversion,[],[f31044]) ).
cnf(s9,plain,
spl66_9,
inference(sat_conversion,[],[f31170]) ).
cnf(s10,plain,
spl66_10,
inference(sat_conversion,[],[f31195]) ).
cnf(s11,plain,
spl66_11,
inference(sat_conversion,[],[f31235]) ).
cnf(s12,plain,
spl66_12,
inference(sat_conversion,[],[f31432]) ).
cnf(s14,plain,
spl66_14,
inference(sat_conversion,[],[f31442]) ).
cnf(s15,plain,
spl66_15,
inference(sat_conversion,[],[f31447]) ).
cnf(s17,plain,
spl66_17,
inference(sat_conversion,[],[f31752]) ).
cnf(s18,plain,
spl66_18,
inference(sat_conversion,[],[f31757]) ).
cnf(s19,plain,
spl66_19,
inference(sat_conversion,[],[f31762]) ).
cnf(s20,plain,
spl66_20,
inference(sat_conversion,[],[f31910]) ).
cnf(s21,plain,
spl66_21,
inference(sat_conversion,[],[f31915]) ).
cnf(s22,plain,
spl66_22,
inference(sat_conversion,[],[f32074]) ).
cnf(s23,plain,
spl66_23,
inference(sat_conversion,[],[f32079]) ).
cnf(s25,plain,
spl66_25,
inference(sat_conversion,[],[f32232]) ).
cnf(s27,plain,
spl66_27,
inference(sat_conversion,[],[f33964]) ).
cnf(s30,plain,
( spl66_1
| spl66_2
| spl66_3
| ~ spl66_7
| spl66_30 ),
inference(sat_conversion,[],[f35414]) ).
cnf(s43,plain,
( spl66_2
| spl66_3
| ~ spl66_7
| ~ spl66_8
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_30
| spl66_44 ),
inference(sat_conversion,[],[f37561]) ).
cnf(s50,plain,
( spl66_1
| spl66_2
| spl66_3
| ~ spl66_5
| spl66_51 ),
inference(sat_conversion,[],[f37673]) ).
cnf(s51,plain,
( spl66_1
| spl66_2
| spl66_3
| ~ spl66_6
| ~ spl66_7
| ~ spl66_8
| ~ spl66_9
| ~ spl66_12
| ~ spl66_14
| ~ spl66_15
| ~ spl66_17
| ~ spl66_18
| ~ spl66_19
| ~ spl66_20
| ~ spl66_21
| ~ spl66_22
| ~ spl66_23
| ~ spl66_25
| ~ spl66_27
| ~ spl66_44
| ~ spl66_51
| spl66_52 ),
inference(sat_conversion,[],[f38690]) ).
cnf(s52,plain,
( spl66_4
| ~ spl66_10
| ~ spl66_11
| ~ spl66_52 ),
inference(sat_conversion,[],[f38763]) ).
cnf(s54,plain,
~ spl66_52,
inference(rat,[],[s52,s10,s11,s4]) ).
cnf(s56,plain,
spl66_51,
inference(rat,[],[s50,s2,s5,s3,s1]) ).
cnf(s57,plain,
spl66_30,
inference(rat,[],[s30,s2,s7,s3,s1]) ).
cnf(s59,plain,
~ spl66_44,
inference(rat,[],[s51,s54,s1,s2,s27,s25,s23,s22,s21,s20,s19,s18,s17,s15,s14,s12,s9,s8,s7,s6,s3,s56]) ).
cnf(s60,plain,
$false,
inference(rat,[],[s43,s2,s3,s27,s25,s23,s22,s21,s20,s19,s18,s17,s15,s14,s12,s9,s8,s7,s59,s57]) ).
fof(f38963,plain,
$false,
inference(avatar_sat_refutation,[],[s60]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG220+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 % Computer : n015.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.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Mon Sep 28 19:50:39 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.29 Running first-order theorem proving
% 0.09/0.29 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
% 20.46/4.34 % (2945863)Detected formulas, will run a generic FOF schedule.
% 20.46/4.34 % (2945873)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1371609119:s2a=on:i=139:gtg=position_2991 on theBenchmark for (2991ds/139Mi)
% 20.46/4.34 % (2945873)Instruction limit reached!
% 20.46/4.34 % (2945873)------------------------------
% 20.46/4.34 % (2945873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/4.34 % (2945873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/4.34 % (2945873)CaDiCaL version: 2.1.3
% 20.46/4.34 % (2945873)Termination reason: Instruction limit
% 20.46/4.34 % (2945873)Termination phase: Property scanning
% 20.46/4.34 % (2945873)Time elapsed: 0.062 s
% 20.46/4.34 % (2945873)Peak memory usage: 119 MB
% 20.46/4.34 % (2945873)Instructions burned: 140 (million)
% 20.46/4.34 % (2945871)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3991076459:i=109:sd=1:ins=1:gsp=on:ss=axioms_2991 on theBenchmark for (2991ds/109Mi)
% 20.46/4.34 % (2945872)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2178988106:i=119:av=off:ss=axioms_2991 on theBenchmark for (2991ds/119Mi)
% 20.46/4.34 % (2945869)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=1632779393:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2991 on theBenchmark for (2991ds/134677Mi)
% 20.46/4.34 % (2945868)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=3625686349:i=141193_2991 on theBenchmark for (2991ds/141193Mi)
% 20.46/4.34 % (2945870)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=1638044586:i=141695:sd=1:nm=32:gsp=on:ss=included_2991 on theBenchmark for (2991ds/141695Mi)
% 20.46/4.34 % (2945874)dis-21_1_sil=8000:lcm=predicate:random_seed=4083771030:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2991 on theBenchmark for (2991ds/129Mi)
% 20.46/4.34 % (2945871)Instruction limit reached!
% 20.46/4.34 % (2945871)------------------------------
% 20.46/4.34 % (2945871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/4.34 % (2945871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/4.34 % (2945871)CaDiCaL version: 2.1.3
% 20.46/4.34 % (2945871)Termination reason: Instruction limit
% 20.46/4.34 % (2945871)Termination phase: SInE selection
% 20.46/4.34 % (2945871)Time elapsed: 0.106 s
% 20.46/4.34 % (2945871)Peak memory usage: 118 MB
% 20.46/4.34 % (2945871)Instructions burned: 109 (million)
% 20.46/4.34 % (2945872)Instruction limit reached!
% 20.46/4.34 % (2945872)------------------------------
% 20.46/4.34 % (2945872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/4.34 % (2945872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/4.34 % (2945872)CaDiCaL version: 2.1.3
% 20.46/4.34 % (2945872)Termination reason: Instruction limit
% 20.46/4.34 % (2945872)Termination phase: SInE selection
% 20.46/4.34 % (2945872)Time elapsed: 0.116 s
% 20.46/4.34 % (2945872)Peak memory usage: 118 MB
% 20.46/4.34 % (2945872)Instructions burned: 119 (million)
% 20.46/4.34 % (2945874)Instruction limit reached!
% 20.46/4.34 % (2945874)------------------------------
% 20.46/4.34 % (2945874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/4.34 % (2945874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/4.34 % (2945874)CaDiCaL version: 2.1.3
% 20.46/4.34 % (2945874)Termination reason: Instruction limit
% 20.46/4.34 % (2945874)Termination phase: SInE selection
% 20.46/4.34 % (2945874)Time elapsed: 0.117 s
% 20.46/4.34 % (2945874)Peak memory usage: 119 MB
% 20.46/4.34 % (2945874)Instructions burned: 129 (million)
% 20.46/4.34 % (2945876)lrs+10_1_sil=8000:sp=occurrence:random_seed=3074097749:i=285:sd=3:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/285Mi)
% 20.46/4.34 % (2945876)Instruction limit reached!
% 20.46/4.34 % (2945876)------------------------------
% 20.46/4.34 % (2945876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/4.34 % (2945876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/4.34 % (2945876)CaDiCaL version: 2.1.3
% 20.46/4.34 % (2945876)Termination reason: Instruction limit
% 20.46/4.34 % (2945876)Termination phase: Saturation
% 20.46/4.34 % (2945876)Time elapsed: 0.156 s
% 20.46/4.34 % (2945876)Peak memory usage: 125 MB
% 20.46/4.34 % (2945876)Instructions burned: 287 (million)
% 31.05/5.87 % (2945884)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3192890526:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 31.05/5.87 % (2945883)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1454737077:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 31.05/5.87 % (2945885)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=179509279:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 31.05/5.87 % (2945883)Instruction limit reached!
% 31.05/5.87 % (2945883)------------------------------
% 31.05/5.87 % (2945883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.05/5.87 % (2945883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.05/5.87 % (2945883)CaDiCaL version: 2.1.3
% 31.05/5.87 % (2945883)Termination reason: Instruction limit
% 31.05/5.87 % (2945883)Termination phase: Property scanning
% 31.05/5.87 % (2945883)Time elapsed: 0.107 s
% 31.05/5.87 % (2945883)Peak memory usage: 119 MB
% 31.05/5.87 % (2945883)Instructions burned: 157 (million)
% 31.05/5.87 % (2945887)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4263356095:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2985 on theBenchmark for (2985ds/294Mi)
% 31.05/5.87 % (2945885)Instruction limit reached!
% 31.05/5.87 % (2945885)------------------------------
% 31.05/5.87 % (2945885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.05/5.87 % (2945885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.05/5.87 % (2945885)CaDiCaL version: 2.1.3
% 31.05/5.87 % (2945885)Termination reason: Instruction limit
% 31.05/5.87 % (2945885)Termination phase: Property scanning
% 31.05/5.87 % (2945885)Time elapsed: 0.166 s
% 31.05/5.87 % (2945885)Peak memory usage: 118 MB
% 31.05/5.87 % (2945885)Instructions burned: 249 (million)
% 31.05/5.87 % (2945887)Instruction limit reached!
% 31.05/5.87 % (2945887)------------------------------
% 31.05/5.87 % (2945887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.05/5.87 % (2945887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.05/5.87 % (2945887)CaDiCaL version: 2.1.3
% 31.05/5.87 % (2945887)Termination reason: Instruction limit
% 31.05/5.87 % (2945887)Termination phase: Preprocessing 3
% 31.05/5.87 % (2945887)Time elapsed: 0.177 s
% 31.05/5.87 % (2945887)Peak memory usage: 124 MB
% 31.05/5.87 % (2945887)Instructions burned: 296 (million)
% 31.05/5.87 % (2945884)Instruction limit reached!
% 31.05/5.87 % (2945884)------------------------------
% 31.05/5.87 % (2945884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.05/5.87 % (2945884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.05/5.87 % (2945884)CaDiCaL version: 2.1.3
% 31.05/5.87 % (2945884)Termination reason: Instruction limit
% 31.05/5.87 % (2945884)Termination phase: Saturation
% 31.05/5.87 % (2945884)Time elapsed: 0.354 s
% 31.05/5.87 % (2945884)Peak memory usage: 125 MB
% 31.05/5.87 % (2945884)Instructions burned: 326 (million)
% 31.05/5.87 % (2945891)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1655213270:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 31.05/5.87 % (2945893)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3817980332:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 31.05/5.87 % (2945894)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=868341036:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 31.05/5.87 % (2945893)Instruction limit reached!
% 31.05/5.87 % (2945893)------------------------------
% 31.05/5.87 % (2945893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.05/5.87 % (2945893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.05/5.87 % (2945893)CaDiCaL version: 2.1.3
% 31.05/5.87 % (2945893)Termination reason: Instruction limit
% 31.05/5.87 % (2945893)Termination phase: SInE selection
% 31.05/5.87 % (2945893)Time elapsed: 0.115 s
% 31.05/5.87 % (2945893)Peak memory usage: 119 MB
% 31.05/5.87 % (2945893)Instructions burned: 113 (million)
% 31.05/5.87 % (2945894)Instruction limit reached!
% 31.05/5.87 % (2945894)------------------------------
% 31.05/5.87 % (2945894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.05/5.87 % (2945894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.05/5.87 % (2945894)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945894)Termination reason: Instruction limit
% 17.32/6.24 % (2945894)Termination phase: Preprocessing 1
% 17.32/6.24 % (2945894)Time elapsed: 0.093 s
% 17.32/6.24 % (2945894)Peak memory usage: 120 MB
% 17.32/6.24 % (2945894)Instructions burned: 127 (million)
% 17.32/6.24 % (2945895)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1621709347:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 17.32/6.24 % (2945895)Instruction limit reached!
% 17.32/6.24 % (2945895)------------------------------
% 17.32/6.24 % (2945895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945895)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945895)Termination reason: Instruction limit
% 17.32/6.24 % (2945895)Termination phase: Property scanning
% 17.32/6.24 % (2945895)Time elapsed: 0.093 s
% 17.32/6.24 % (2945895)Peak memory usage: 118 MB
% 17.32/6.24 % (2945895)Instructions burned: 115 (million)
% 17.32/6.24 % (2945899)lrs+10_1_sil=8000:sp=occurrence:random_seed=317604774:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2979 on theBenchmark for (2979ds/907Mi)
% 17.32/6.24 % (2945900)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3833373427:i=437:sd=1:aac=none:ss=included_2979 on theBenchmark for (2979ds/437Mi)
% 17.32/6.24 % (2945902)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=285862303:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 17.32/6.24 % (2945900)Instruction limit reached!
% 17.32/6.24 % (2945900)------------------------------
% 17.32/6.24 % (2945900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945900)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945900)Termination reason: Instruction limit
% 17.32/6.24 % (2945900)Termination phase: Saturation
% 17.32/6.24 % (2945900)Time elapsed: 0.373 s
% 17.32/6.24 % (2945900)Peak memory usage: 125 MB
% 17.32/6.24 % (2945900)Instructions burned: 437 (million)
% 17.32/6.24 % (2945899)Instruction limit reached!
% 17.32/6.24 % (2945899)------------------------------
% 17.32/6.24 % (2945899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945899)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945899)Termination reason: Instruction limit
% 17.32/6.24 % (2945899)Termination phase: Function definition elimination
% 17.32/6.24 % (2945899)Time elapsed: 0.498 s
% 17.32/6.24 % (2945899)Peak memory usage: 142 MB
% 17.32/6.24 % (2945899)Instructions burned: 909 (million)
% 17.32/6.24 % (2945907)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2052762968:st=8:i=592:sd=3:ep=RST:ss=axioms_2972 on theBenchmark for (2972ds/592Mi)
% 17.32/6.24 % (2945906)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2092246749:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2973 on theBenchmark for (2973ds/134Mi)
% 17.32/6.24 % (2945906)Instruction limit reached!
% 17.32/6.24 % (2945906)------------------------------
% 17.32/6.24 % (2945906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945906)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945906)Termination reason: Instruction limit
% 17.32/6.24 % (2945906)Termination phase: SInE selection
% 17.32/6.24 % (2945906)Time elapsed: 0.143 s
% 17.32/6.24 % (2945906)Peak memory usage: 118 MB
% 17.32/6.24 % (2945906)Instructions burned: 134 (million)
% 17.32/6.24 % (2945907)Instruction limit reached!
% 17.32/6.24 % (2945907)------------------------------
% 17.32/6.24 % (2945907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945907)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945907)Termination reason: Instruction limit
% 17.32/6.24 % (2945907)Termination phase: Preprocessing 3
% 17.32/6.24 % (2945907)Time elapsed: 0.385 s
% 17.32/6.24 % (2945907)Peak memory usage: 141 MB
% 17.32/6.24 % (2945907)Instructions burned: 592 (million)
% 17.32/6.24 % (2945910)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3172637188:st=3:i=13193:sd=3:ss=axioms_2969 on theBenchmark for (2969ds/13193Mi)
% 17.32/6.24 % (2945912)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=108899451:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/125Mi)
% 17.32/6.24 % (2945912)Instruction limit reached!
% 17.32/6.24 % (2945912)------------------------------
% 17.32/6.24 % (2945912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945912)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945912)Termination reason: Instruction limit
% 17.32/6.24 % (2945912)Termination phase: Property scanning
% 17.32/6.24 % (2945912)Time elapsed: 0.085 s
% 17.32/6.24 % (2945912)Peak memory usage: 119 MB
% 17.32/6.24 % (2945912)Instructions burned: 126 (million)
% 17.32/6.24 % (2945891)Instruction limit reached!
% 17.32/6.24 % (2945891)------------------------------
% 17.32/6.24 % (2945891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945891)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945891)Termination reason: Instruction limit
% 17.32/6.24 % (2945891)Termination phase: Function definition elimination
% 17.32/6.24 % (2945891)Time elapsed: 1.931 s
% 17.32/6.24 % (2945891)Peak memory usage: 186 MB
% 17.32/6.24 % (2945891)Instructions burned: 2351 (million)
% 17.32/6.24 % (2945915)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=255898897:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/141Mi)
% 17.32/6.24 % (2945914)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3316896615:i=134:gtgl=5:slsql=off:gtg=exists_sym_2962 on theBenchmark for (2962ds/134Mi)
% 17.32/6.24 % (2945914)Instruction limit reached!
% 17.32/6.24 % (2945914)------------------------------
% 17.32/6.24 % (2945914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945914)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945914)Termination reason: Instruction limit
% 17.32/6.24 % (2945914)Termination phase: Property scanning
% 17.32/6.24 % (2945914)Time elapsed: 0.101 s
% 17.32/6.24 % (2945914)Peak memory usage: 119 MB
% 17.32/6.24 % (2945914)Instructions burned: 134 (million)
% 17.32/6.24 % (2945915)Instruction limit reached!
% 17.32/6.24 % (2945915)------------------------------
% 17.32/6.24 % (2945915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945915)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945915)Termination reason: Instruction limit
% 17.32/6.24 % (2945915)Termination phase: NewCNF
% 17.32/6.24 % (2945915)Time elapsed: 0.136 s
% 17.32/6.24 % (2945915)Peak memory usage: 121 MB
% 17.32/6.24 % (2945915)Instructions burned: 141 (million)
% 17.32/6.24 % (2945919)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=677160635:i=6060:aac=none:ins=25_2959 on theBenchmark for (2959ds/6060Mi)
% 17.32/6.24 % (2945918)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4142211714:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2959 on theBenchmark for (2959ds/431Mi)
% 17.32/6.24 % (2945918)Instruction limit reached!
% 17.32/6.24 % (2945918)------------------------------
% 17.32/6.24 % (2945918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945918)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945918)Termination reason: Instruction limit
% 17.32/6.24 % (2945918)Termination phase: Saturation
% 17.32/6.24 % (2945918)Time elapsed: 0.436 s
% 17.32/6.24 % (2945918)Peak memory usage: 126 MB
% 17.32/6.24 % (2945918)Instructions burned: 431 (million)
% 17.32/6.24 % (2945922)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1821238061:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2952 on theBenchmark for (2952ds/150Mi)
% 17.32/6.24 % (2945870)First to succeed.
% 17.32/6.24 % (2945870)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2945863"
% 17.32/6.24 % (2945922)Instruction limit reached!
% 17.32/6.24 % (2945922)------------------------------
% 17.32/6.24 % (2945922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/6.24 % (2945922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/6.24 % (2945922)CaDiCaL version: 2.1.3
% 17.32/6.24 % (2945922)Termination reason: Instruction limit
% 17.32/6.24 % (2945922)Termination phase: Preprocessing 1
% 17.32/6.24 % (2945922)Time elapsed: 0.160 s
% 17.32/6.24 % (2945922)Peak memory usage: 119 MB
% 17.32/6.24 % (2945922)Instructions burned: 151 (million)
% 17.32/6.24 % (2945924)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1442641102:i=14155:bd=all_2948 on theBenchmark for (2948ds/14155Mi)
% 17.32/6.24 % (2945870)Refutation found. Thanks to Tanya!
% 17.32/6.24 % SZS status Theorem for theBenchmark
% 17.32/6.24 % SZS output start Proof for theBenchmark
% See solution above
% 34.51/6.55 % (2945870)------------------------------
% 34.51/6.55 % (2945870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.51/6.55 % (2945870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.51/6.55 % (2945870)CaDiCaL version: 2.1.3
% 34.51/6.55 % (2945870)Termination reason: Refutation
% 34.51/6.55 % (2945870)Time elapsed: 3.955 s
% 34.51/6.55 % (2945870)Peak memory usage: 183 MB
% 34.51/6.55 % (2945870)Instructions burned: 4159 (million)
% 34.51/6.55 % (2945870)------------------------------
% 34.51/6.55 % (2945870)------------------------------
% 34.51/6.55 % (2945863)Success in time 5.517 s
% 34.51/6.55 % Vampire exiting
%------------------------------------------------------------------------------