%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG220+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 : Sun Sep 27 06:49:49 AM UTC 2026
% Result : Theorem 2.30s 0.74s
% Output : CNFRefutation 2.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 5
% Syntax : Number of formulae : 267 ( 39 unt; 0 def)
% Number of atoms : 2822 ( 40 equ)
% Maximal formula atoms : 29 ( 10 avg)
% Number of connectives : 4743 (2188 ~;2358 |; 175 &)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 11 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 301 ( 0 sgn 21 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k1_rmod_5,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
& l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B)
& l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ( m1_rmod_2(k1_rmod_5(A,B,C),A,B)
& v3_vectsp_2(k1_rmod_5(A,B,C),A) ) ),
file('theBenchmark.p',dt_k1_rmod_5) ).
fof(dt_m1_rmod_2,axiom,
! [A,B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B)
& l3_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [C] :
( m1_rmod_2(C,A,B)
=> ( l1_vectsp_2(C,A)
& v5_vectsp_2(C,A)
& v6_rlvect_1(C)
& v5_rlvect_1(C)
& v4_rlvect_1(C)
& v3_rlvect_1(C)
& ~ v3_struct_0(C) ) ) ),
file('theBenchmark.p',dt_m1_rmod_2) ).
fof(t15_rmod_5,axiom,
! [A] :
( ( l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( r1_tarski(C,D)
=> m1_rmod_2(k1_rmod_5(A,B,C),A,k1_rmod_5(A,B,D)) ) ) ) ) ),
file('theBenchmark.p',t15_rmod_5) ).
fof(t33_rmod_2,axiom,
! [A] :
( ( l3_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v3_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( l1_vectsp_2(C,A)
& v5_vectsp_2(C,A)
& v3_vectsp_2(C,A)
& v6_rlvect_1(C)
& v5_rlvect_1(C)
& v4_rlvect_1(C)
& v3_rlvect_1(C)
& ~ v3_struct_0(C) )
=> ( ( m1_rmod_2(B,A,C)
& m1_rmod_2(C,A,B) )
=> C = B ) ) ) ),
file('theBenchmark.p',t33_rmod_2) ).
fof(t16_rmod_5,conjecture,
! [A] :
( ( l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v3_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( r1_tarski(C,D)
& k1_rmod_5(A,B,C) = B )
=> k1_rmod_5(A,B,D) = B ) ) ) ) ),
file('theBenchmark.p',t16_rmod_5) ).
fof(t16_rmod_5_neg,negated_conjecture,
~ ! [A] :
( ( l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v3_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( r1_tarski(C,D)
& k1_rmod_5(A,B,C) = B )
=> k1_rmod_5(A,B,D) = B ) ) ) ) ),
inference(assume_negation,[status(cth)],[t16_rmod_5]) ).
fof(nnf_68,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( k1_rmod_5(A,B,D) != B
& r1_tarski(C,D)
& k1_rmod_5(A,B,C) = B
& m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) )
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
& l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v3_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
& l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t16_rmod_5_neg]) ).
fof(sk_t16_rmod_5_neg,plain,
( k1_rmod_5(sK0,sK3,sK2) != sK3
& r1_tarski(sK1,sK2)
& k1_rmod_5(sK0,sK3,sK1) = sK3
& m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3)))
& m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3)))
& l1_vectsp_2(sK3,sK0)
& v5_vectsp_2(sK3,sK0)
& v3_vectsp_2(sK3,sK0)
& v6_rlvect_1(sK3)
& v5_rlvect_1(sK3)
& v4_rlvect_1(sK3)
& v3_rlvect_1(sK3)
& ~ v3_struct_0(sK3)
& l3_vectsp_1(sK0)
& v2_vectsp_2(sK0)
& ~ v10_vectsp_1(sK0)
& v8_vectsp_1(sK0)
& v7_vectsp_1(sK0)
& v6_vectsp_1(sK0)
& v7_group_1(sK0)
& v4_group_1(sK0)
& v6_rlvect_1(sK0)
& v5_rlvect_1(sK0)
& v4_rlvect_1(sK0)
& v3_rlvect_1(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK3,sK1,sK2]),skolemize(A,sK0),skolemize(B,sK3),skolemize(C,sK1),skolemize(D,sK2)],[nnf_68]) ).
cnf(c_69,negated_conjecture,
v4_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_70,plain,
( C = B
| ~ m1_rmod_2(B,A,C)
| ~ m1_rmod_2(C,A,B)
| ~ l1_vectsp_2(C,A)
| ~ v5_vectsp_2(C,A)
| ~ v3_vectsp_2(C,A)
| ~ v6_rlvect_1(C)
| ~ v5_rlvect_1(C)
| ~ v4_rlvect_1(C)
| ~ v3_rlvect_1(C)
| v3_struct_0(C)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v3_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t33_rmod_2]) ).
cnf(c_71,plain,
( m1_rmod_2(k1_rmod_5(A,B,C),A,k1_rmod_5(A,B,D))
| ~ r1_tarski(C,D)
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v2_vectsp_2(A)
| v10_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v7_group_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t15_rmod_5]) ).
cnf(c_96,plain,
( l1_vectsp_2(C,A)
| ~ m1_rmod_2(C,A,B)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_rmod_2]) ).
cnf(c_97,plain,
( v5_vectsp_2(C,A)
| ~ m1_rmod_2(C,A,B)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_rmod_2]) ).
cnf(c_98,plain,
( v6_rlvect_1(C)
| ~ m1_rmod_2(C,A,B)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_rmod_2]) ).
cnf(c_99,plain,
( v5_rlvect_1(C)
| ~ m1_rmod_2(C,A,B)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_rmod_2]) ).
cnf(c_100,plain,
( v4_rlvect_1(C)
| ~ m1_rmod_2(C,A,B)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_rmod_2]) ).
cnf(c_101,plain,
( v3_rlvect_1(C)
| ~ m1_rmod_2(C,A,B)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_rmod_2]) ).
cnf(c_102,plain,
( ~ v3_struct_0(C)
| ~ m1_rmod_2(C,A,B)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_rmod_2]) ).
cnf(c_103,plain,
( m1_rmod_2(k1_rmod_5(A,B,C),A,B)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v2_vectsp_2(A)
| v10_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v7_group_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_rmod_5]) ).
cnf(c_104,plain,
( v3_vectsp_2(k1_rmod_5(A,B,C),A)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l3_vectsp_1(A)
| ~ v2_vectsp_2(A)
| v10_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v7_group_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_rmod_5]) ).
cnf(c_105,negated_conjecture,
r1_tarski(sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_106,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,k1_rmod_5(sK0,A,C))
| ~ r1_tarski(B,C)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_71]) ).
cnf(c_289,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_105,c_106]) ).
cnf(c_315,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_316,negated_conjecture,
v3_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_317,negated_conjecture,
v4_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_318,negated_conjecture,
v5_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_319,negated_conjecture,
v6_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_320,negated_conjecture,
v7_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_321,negated_conjecture,
v6_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_322,negated_conjecture,
v7_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_323,negated_conjecture,
v8_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_324,negated_conjecture,
~ v10_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_325,negated_conjecture,
v2_vectsp_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_326,negated_conjecture,
l3_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_327,negated_conjecture,
~ v3_struct_0(sK3),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_328,negated_conjecture,
v3_rlvect_1(sK3),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_329,negated_conjecture,
v4_rlvect_1(sK3),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_330,negated_conjecture,
v5_rlvect_1(sK3),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_331,negated_conjecture,
v6_rlvect_1(sK3),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_332,negated_conjecture,
v3_vectsp_2(sK3,sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_333,negated_conjecture,
v5_vectsp_2(sK3,sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_334,negated_conjecture,
l1_vectsp_2(sK3,sK0),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_335,negated_conjecture,
m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3))),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_336,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3))),
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_337,negated_conjecture,
k1_rmod_5(sK0,sK3,sK1) = sK3,
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_338,negated_conjecture,
k1_rmod_5(sK0,sK3,sK2) != sK3,
inference(split_conjunct,[status(thm)],[sk_t16_rmod_5_neg]) ).
cnf(c_339,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_70]) ).
cnf(c_3236,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_339]) ).
cnf(c_3237,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3236]) ).
cnf(c_3238,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3237]) ).
cnf(c_3239,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3238]) ).
cnf(c_3240,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3239]) ).
cnf(c_3241,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3240]) ).
cnf(c_3242,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3241]) ).
cnf(c_3243,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3242]) ).
cnf(c_340,negated_conjecture,
( B = A
| ~ m1_rmod_2(A,sK0,B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(B,sK0)
| ~ v5_vectsp_2(B,sK0)
| ~ v3_vectsp_2(B,sK0)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v3_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3243]) ).
cnf(c_389,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_96]) ).
cnf(c_3244,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_389]) ).
cnf(c_3245,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3244]) ).
cnf(c_3246,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3245]) ).
cnf(c_3247,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3246]) ).
cnf(c_3248,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3247]) ).
cnf(c_3249,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3248]) ).
cnf(c_3250,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3249]) ).
cnf(c_3251,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3250]) ).
cnf(c_390,negated_conjecture,
( l1_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3251]) ).
cnf(c_391,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_97]) ).
cnf(c_3252,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_391]) ).
cnf(c_3253,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3252]) ).
cnf(c_3254,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3253]) ).
cnf(c_3255,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3254]) ).
cnf(c_3256,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3255]) ).
cnf(c_3257,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3256]) ).
cnf(c_3258,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3257]) ).
cnf(c_3259,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3258]) ).
cnf(c_392,negated_conjecture,
( v5_vectsp_2(B,sK0)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3259]) ).
cnf(c_393,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_98]) ).
cnf(c_3260,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_393]) ).
cnf(c_3261,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3260]) ).
cnf(c_3262,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3261]) ).
cnf(c_3263,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3262]) ).
cnf(c_3264,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3263]) ).
cnf(c_3265,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3264]) ).
cnf(c_3266,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3265]) ).
cnf(c_3267,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3266]) ).
cnf(c_394,negated_conjecture,
( v6_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3267]) ).
cnf(c_395,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_99]) ).
cnf(c_3268,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_395]) ).
cnf(c_3269,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3268]) ).
cnf(c_3270,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3269]) ).
cnf(c_3271,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3270]) ).
cnf(c_3272,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3271]) ).
cnf(c_3273,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3272]) ).
cnf(c_3274,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3273]) ).
cnf(c_3275,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3274]) ).
cnf(c_396,negated_conjecture,
( v5_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3275]) ).
cnf(c_397,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_100]) ).
cnf(c_3276,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_397]) ).
cnf(c_3277,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3276]) ).
cnf(c_3278,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3277]) ).
cnf(c_3279,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3278]) ).
cnf(c_3280,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3279]) ).
cnf(c_3281,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3280]) ).
cnf(c_3282,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3281]) ).
cnf(c_3283,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3282]) ).
cnf(c_398,negated_conjecture,
( v4_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3283]) ).
cnf(c_399,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_101]) ).
cnf(c_3284,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_399]) ).
cnf(c_3285,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3284]) ).
cnf(c_3286,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3285]) ).
cnf(c_3287,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3286]) ).
cnf(c_3288,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3287]) ).
cnf(c_3289,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3288]) ).
cnf(c_3290,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3289]) ).
cnf(c_3291,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3290]) ).
cnf(c_400,negated_conjecture,
( v3_rlvect_1(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3291]) ).
cnf(c_401,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_102]) ).
cnf(c_3292,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_401]) ).
cnf(c_3293,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3292]) ).
cnf(c_3294,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3293]) ).
cnf(c_3295,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3294]) ).
cnf(c_3296,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3295]) ).
cnf(c_3297,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3296]) ).
cnf(c_3298,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3297]) ).
cnf(c_3299,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3298]) ).
cnf(c_402,negated_conjecture,
( ~ v3_struct_0(B)
| ~ m1_rmod_2(B,sK0,A)
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3299]) ).
cnf(c_403,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_103]) ).
cnf(c_3300,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_403]) ).
cnf(c_3301,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3300]) ).
cnf(c_3302,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3301]) ).
cnf(c_3303,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3302]) ).
cnf(c_3304,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3303]) ).
cnf(c_3305,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_320,c_3304]) ).
cnf(c_3306,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3305]) ).
cnf(c_3307,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3306]) ).
cnf(c_3308,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3307]) ).
cnf(c_3309,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0) ),
inference(resolve,[status(thm)],[c_324,c_3308]) ).
cnf(c_3310,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_325,c_3309]) ).
cnf(c_404,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,B),sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3310]) ).
cnf(c_405,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_69,c_104]) ).
cnf(c_3311,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_405]) ).
cnf(c_3312,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3311]) ).
cnf(c_3313,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3312]) ).
cnf(c_3314,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3313]) ).
cnf(c_3315,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3314]) ).
cnf(c_3316,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_320,c_3315]) ).
cnf(c_3317,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3316]) ).
cnf(c_3318,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3317]) ).
cnf(c_3319,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3318]) ).
cnf(c_3320,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0) ),
inference(resolve,[status(thm)],[c_324,c_3319]) ).
cnf(c_3321,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_325,c_3320]) ).
cnf(c_406,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,A,B),sK0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3321]) ).
cnf(c_3322,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0)
| ~ v3_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_315,c_289]) ).
cnf(c_3323,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0)
| ~ v4_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_316,c_3322]) ).
cnf(c_3324,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0)
| ~ v5_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_3323]) ).
cnf(c_3325,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_318,c_3324]) ).
cnf(c_3326,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v7_group_1(sK0) ),
inference(resolve,[status(thm)],[c_319,c_3325]) ).
cnf(c_3327,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_320,c_3326]) ).
cnf(c_3328,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_321,c_3327]) ).
cnf(c_3329,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_322,c_3328]) ).
cnf(c_3330,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0)
| v10_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_323,c_3329]) ).
cnf(c_3331,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0)
| ~ v2_vectsp_2(sK0) ),
inference(resolve,[status(thm)],[c_324,c_3330]) ).
cnf(c_3332,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A)
| ~ l3_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_325,c_3331]) ).
cnf(c_590,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,A,sK1),sK0,k1_rmod_5(sK0,A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_vectsp_2(A,sK0)
| ~ v5_vectsp_2(A,sK0)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_326,c_3332]) ).
cnf(c_3333,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,A),sK0,sK3)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_404,c_333]) ).
cnf(c_3334,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,A),sK0,sK3)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3333]) ).
cnf(c_3335,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,A),sK0,sK3)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3334]) ).
cnf(c_3336,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,A),sK0,sK3)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3335]) ).
cnf(c_3337,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,A),sK0,sK3)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3336]) ).
cnf(c_3338,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,A),sK0,sK3)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3337]) ).
cnf(c_774,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,A),sK0,sK3)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3))) ),
inference(resolve,[status(thm)],[c_334,c_3338]) ).
cnf(c_3339,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,sK3,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_406,c_333]) ).
cnf(c_3340,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,sK3,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3339]) ).
cnf(c_3341,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,sK3,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3340]) ).
cnf(c_3342,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,sK3,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3341]) ).
cnf(c_3343,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,sK3,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3342]) ).
cnf(c_3344,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,sK3,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3343]) ).
cnf(c_776,negated_conjecture,
( v3_vectsp_2(k1_rmod_5(sK0,sK3,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK3))) ),
inference(resolve,[status(thm)],[c_334,c_3344]) ).
cnf(c_3345,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_590,c_333]) ).
cnf(c_3346,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3345]) ).
cnf(c_3347,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3346]) ).
cnf(c_3348,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3347]) ).
cnf(c_3349,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3348]) ).
cnf(c_3350,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3349]) ).
cnf(c_3351,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK3))) ),
inference(resolve,[status(thm)],[c_334,c_3350]) ).
cnf(c_3352,negated_conjecture,
( m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK3))) ),
inference(resolve,[status(thm)],[c_335,c_3351]) ).
cnf(c_1156,negated_conjecture,
m1_rmod_2(k1_rmod_5(sK0,sK3,sK1),sK0,k1_rmod_5(sK0,sK3,sK2)),
inference(resolve,[status(thm)],[c_336,c_3352]) ).
cnf(c_2599,plain,
m1_rmod_2(k1_rmod_5(sK0,sK3,sK2),sK0,sK3),
inference(resolve,[status(thm)],[c_774,c_336]) ).
cnf(c_2624,plain,
v3_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0),
inference(resolve,[status(thm)],[c_776,c_336]) ).
cnf(c_3353,negated_conjecture,
( ~ v3_struct_0(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_2599,c_402]) ).
cnf(c_3354,negated_conjecture,
( ~ v3_struct_0(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3353]) ).
cnf(c_3355,negated_conjecture,
( ~ v3_struct_0(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3354]) ).
cnf(c_3356,negated_conjecture,
( ~ v3_struct_0(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3355]) ).
cnf(c_3357,negated_conjecture,
( ~ v3_struct_0(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3356]) ).
cnf(c_3358,negated_conjecture,
( ~ v3_struct_0(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3357]) ).
cnf(c_3359,negated_conjecture,
( ~ v3_struct_0(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_333,c_3358]) ).
cnf(c_2703,negated_conjecture,
~ v3_struct_0(k1_rmod_5(sK0,sK3,sK2)),
inference(resolve,[status(thm)],[c_334,c_3359]) ).
cnf(c_3360,negated_conjecture,
( v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_2599,c_400]) ).
cnf(c_3361,negated_conjecture,
( v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3360]) ).
cnf(c_3362,negated_conjecture,
( v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3361]) ).
cnf(c_3363,negated_conjecture,
( v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3362]) ).
cnf(c_3364,negated_conjecture,
( v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3363]) ).
cnf(c_3365,negated_conjecture,
( v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3364]) ).
cnf(c_3366,negated_conjecture,
( v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_333,c_3365]) ).
cnf(c_2704,negated_conjecture,
v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2)),
inference(resolve,[status(thm)],[c_334,c_3366]) ).
cnf(c_3367,negated_conjecture,
( v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_2599,c_398]) ).
cnf(c_3368,negated_conjecture,
( v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3367]) ).
cnf(c_3369,negated_conjecture,
( v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3368]) ).
cnf(c_3370,negated_conjecture,
( v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3369]) ).
cnf(c_3371,negated_conjecture,
( v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3370]) ).
cnf(c_3372,negated_conjecture,
( v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3371]) ).
cnf(c_3373,negated_conjecture,
( v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_333,c_3372]) ).
cnf(c_2705,negated_conjecture,
v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2)),
inference(resolve,[status(thm)],[c_334,c_3373]) ).
cnf(c_3374,negated_conjecture,
( v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_2599,c_396]) ).
cnf(c_3375,negated_conjecture,
( v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3374]) ).
cnf(c_3376,negated_conjecture,
( v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3375]) ).
cnf(c_3377,negated_conjecture,
( v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3376]) ).
cnf(c_3378,negated_conjecture,
( v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3377]) ).
cnf(c_3379,negated_conjecture,
( v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3378]) ).
cnf(c_3380,negated_conjecture,
( v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_333,c_3379]) ).
cnf(c_2706,negated_conjecture,
v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2)),
inference(resolve,[status(thm)],[c_334,c_3380]) ).
cnf(c_3381,negated_conjecture,
( v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_2599,c_394]) ).
cnf(c_3382,negated_conjecture,
( v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3381]) ).
cnf(c_3383,negated_conjecture,
( v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3382]) ).
cnf(c_3384,negated_conjecture,
( v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3383]) ).
cnf(c_3385,negated_conjecture,
( v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3384]) ).
cnf(c_3386,negated_conjecture,
( v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3385]) ).
cnf(c_3387,negated_conjecture,
( v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_333,c_3386]) ).
cnf(c_2707,negated_conjecture,
v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2)),
inference(resolve,[status(thm)],[c_334,c_3387]) ).
cnf(c_3388,negated_conjecture,
( v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_2599,c_392]) ).
cnf(c_3389,negated_conjecture,
( v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3388]) ).
cnf(c_3390,negated_conjecture,
( v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3389]) ).
cnf(c_3391,negated_conjecture,
( v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3390]) ).
cnf(c_3392,negated_conjecture,
( v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3391]) ).
cnf(c_3393,negated_conjecture,
( v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3392]) ).
cnf(c_3394,negated_conjecture,
( v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_333,c_3393]) ).
cnf(c_2708,negated_conjecture,
v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0),
inference(resolve,[status(thm)],[c_334,c_3394]) ).
cnf(c_3395,negated_conjecture,
( l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_2599,c_390]) ).
cnf(c_3396,negated_conjecture,
( l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3395]) ).
cnf(c_3397,negated_conjecture,
( l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3396]) ).
cnf(c_3398,negated_conjecture,
( l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3397]) ).
cnf(c_3399,negated_conjecture,
( l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3398]) ).
cnf(c_3400,negated_conjecture,
( l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3399]) ).
cnf(c_3401,negated_conjecture,
( l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_333,c_3400]) ).
cnf(c_2709,negated_conjecture,
l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0),
inference(resolve,[status(thm)],[c_334,c_3401]) ).
cnf(c_3402,negated_conjecture,
( sK3 = k1_rmod_5(sK0,sK3,sK2)
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v3_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| v3_struct_0(k1_rmod_5(sK0,sK3,sK2)) ),
inference(resolve,[status(thm)],[c_2599,c_340]) ).
cnf(c_3403,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v3_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| v3_struct_0(k1_rmod_5(sK0,sK3,sK2)) ),
inference(copy,[status(thm)],[c_3402]) ).
cnf(c_3404,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v3_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v3_rlvect_1(k1_rmod_5(sK0,sK3,sK2)) ),
inference(resolve,[status(thm)],[c_2703,c_3403]) ).
cnf(c_3405,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v3_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v4_rlvect_1(k1_rmod_5(sK0,sK3,sK2)) ),
inference(resolve,[status(thm)],[c_2704,c_3404]) ).
cnf(c_3406,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v3_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2))
| ~ v5_rlvect_1(k1_rmod_5(sK0,sK3,sK2)) ),
inference(resolve,[status(thm)],[c_2705,c_3405]) ).
cnf(c_3407,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v3_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v6_rlvect_1(k1_rmod_5(sK0,sK3,sK2)) ),
inference(resolve,[status(thm)],[c_2706,c_3406]) ).
cnf(c_3408,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v3_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0) ),
inference(resolve,[status(thm)],[c_2707,c_3407]) ).
cnf(c_3409,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0)
| ~ v5_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0) ),
inference(resolve,[status(thm)],[c_2624,c_3408]) ).
cnf(c_3410,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3)
| ~ l1_vectsp_2(k1_rmod_5(sK0,sK3,sK2),sK0) ),
inference(resolve,[status(thm)],[c_2708,c_3409]) ).
cnf(c_3411,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3)
| v3_struct_0(sK3) ),
inference(resolve,[status(thm)],[c_2709,c_3410]) ).
cnf(c_3412,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v3_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_327,c_3411]) ).
cnf(c_3413,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_328,c_3412]) ).
cnf(c_3414,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_329,c_3413]) ).
cnf(c_3415,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0)
| ~ v6_rlvect_1(sK3) ),
inference(resolve,[status(thm)],[c_330,c_3414]) ).
cnf(c_3416,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0)
| ~ v3_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_331,c_3415]) ).
cnf(c_3417,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0)
| ~ v5_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_332,c_3416]) ).
cnf(c_3418,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2))
| ~ l1_vectsp_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_333,c_3417]) ).
cnf(c_3419,negated_conjecture,
( k1_rmod_5(sK0,sK3,sK2) = sK3
| ~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2)) ),
inference(resolve,[status(thm)],[c_334,c_3418]) ).
cnf(c_2710,negated_conjecture,
~ m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2)),
inference(resolve,[status(thm)],[c_338,c_3419]) ).
cnf(c_3420,plain,
m1_rmod_2(sK3,sK0,k1_rmod_5(sK0,sK3,sK2)),
inference(paramod,[status(thm)],[c_337,c_1156]) ).
cnf(c_3235,plain,
$false,
inference(resolve,[status(thm)],[c_2710,c_3420]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG220+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n011.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sat Sep 26 21:31:44 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 1576824 was started by sandbox on n011,
% 0.08/0.37 % Sat Sep 26 21:31:44 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.40
% 0.08/0.40 % From the command line: assign(max_seconds, 300).
% 2.30/0.74
% 2.30/0.74 % given #500 (T,wt=13): 1879 l2_struct_0(f12(c5)). [resolve(901,a,267,c),unit_del(b,292)].
% 2.30/0.74
% 2.30/0.74 % SZS status Theorem for theBenchmark
% 2.30/0.74
% 2.30/0.74 % Proof 1 at 0.28 (+ 0.03) seconds.
% 2.30/0.74 % Length of proof is 79.
% 2.30/0.74 % Level of proof is 8.
% 2.30/0.74 % Maximum clause weight is 75.000.
% 2.30/0.74 % Given clauses 795.
% 2.30/0.74
% 2.30/0.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------