%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG219+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Sun Sep 27 06:49:49 AM UTC 2026
% Result : Theorem 2.33s 0.79s
% Output : CNFRefutation 2.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 10
% Syntax : Number of formulae : 119 ( 36 unt; 0 def)
% Number of atoms : 958 ( 113 equ)
% Maximal formula atoms : 26 ( 8 avg)
% Number of connectives : 1460 ( 621 ~; 678 |; 139 &)
% ( 1 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-5 aty)
% Number of variables : 123 ( 1 sgn 23 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v3_vectsp_2,axiom,
! [A,B] :
( ( l1_vectsp_2(B,A)
& l1_struct_0(A) )
=> ( v3_vectsp_2(B,A)
=> B = g1_vectsp_2(A,u1_struct_0(B),u1_rlvect_1(B),u2_struct_0(B),u1_vectsp_2(A,B)) ) ),
file('theBenchmark.p',abstractness_v3_vectsp_2) ).
fof(d4_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)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> k2_rmod_2(A,B) = g1_vectsp_2(A,u1_struct_0(B),u1_rlvect_1(B),u2_struct_0(B),u1_vectsp_2(A,B)) ) ),
file('theBenchmark.p',d4_rmod_2) ).
fof(dt_k2_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) )
=> ( m1_rmod_2(k2_rmod_2(A,B),A,B)
& v3_vectsp_2(k2_rmod_2(A,B),A) ) ),
file('theBenchmark.p',dt_k2_rmod_2) ).
fof(dt_l1_rlvect_1,axiom,
! [A] :
( l1_rlvect_1(A)
=> l2_struct_0(A) ),
file('theBenchmark.p',dt_l1_rlvect_1) ).
fof(dt_l2_struct_0,axiom,
! [A] :
( l2_struct_0(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l2_struct_0) ).
fof(dt_l3_vectsp_1,axiom,
! [A] :
( l3_vectsp_1(A)
=> ( l2_vectsp_1(A)
& l1_rlvect_1(A) ) ),
file('theBenchmark.p',dt_l3_vectsp_1) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : r1_tarski(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t13_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_rmod_2(D,A,B)
& v3_vectsp_2(D,A) )
=> ( C = u1_struct_0(D)
=> ( k1_rmod_5(A,B,C) = D
| k1_rlvect_1(A) = k2_group_1(A) ) ) ) ) ) ),
file('theBenchmark.p',t13_rmod_5) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t14_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)))
=> ( C = u1_struct_0(B)
=> ( k1_rmod_5(A,B,C) = B
| k1_rlvect_1(A) = k2_group_1(A) ) ) ) ) ),
file('theBenchmark.p',t14_rmod_5) ).
fof(t14_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)))
=> ( C = u1_struct_0(B)
=> ( k1_rmod_5(A,B,C) = B
| k1_rlvect_1(A) = k2_group_1(A) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t14_rmod_5]) ).
fof(nnf_71,plain,
? [A] :
( ? [B] :
( ? [C] :
( k1_rmod_5(A,B,C) != B
& k2_group_1(A) != k1_rlvect_1(A)
& u1_struct_0(B) = C
& 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)],[t14_rmod_5_neg]) ).
fof(sk_t14_rmod_5_neg,plain,
( k1_rmod_5(sK0,sK1,sK2) != sK1
& k2_group_1(sK0) != k1_rlvect_1(sK0)
& u1_struct_0(sK1) = sK2
& m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
& l1_vectsp_2(sK1,sK0)
& v5_vectsp_2(sK1,sK0)
& v3_vectsp_2(sK1,sK0)
& v6_rlvect_1(sK1)
& v5_rlvect_1(sK1)
& v4_rlvect_1(sK1)
& v3_rlvect_1(sK1)
& ~ v3_struct_0(sK1)
& 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,sK1,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_71]) ).
cnf(c_72,negated_conjecture,
v4_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_73,plain,
( k1_rmod_5(A,B,C) = D
| k2_group_1(A) = k1_rlvect_1(A)
| u1_struct_0(D) != C
| ~ m1_rmod_2(D,A,B)
| ~ v3_vectsp_2(D,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)],[t13_rmod_5]) ).
cnf(c_105,plain,
( m1_rmod_2(k2_rmod_2(A,B),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_k2_rmod_2]) ).
cnf(c_109,plain,
( k2_rmod_2(A,B) = g1_vectsp_2(A,u1_struct_0(B),u1_rlvect_1(B),u2_struct_0(B),u1_vectsp_2(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)],[d4_rmod_2]) ).
cnf(c_130,plain,
( l1_struct_0(A)
| ~ l2_struct_0(A) ),
inference(clausify,[status(thm)],[dt_l2_struct_0]) ).
cnf(c_135,plain,
( g1_vectsp_2(A,u1_struct_0(B),u1_rlvect_1(B),u2_struct_0(B),u1_vectsp_2(A,B)) = B
| ~ v3_vectsp_2(B,A)
| ~ l1_vectsp_2(B,A)
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[abstractness_v3_vectsp_2]) ).
cnf(c_147,plain,
( l2_struct_0(A)
| ~ l1_rlvect_1(A) ),
inference(clausify,[status(thm)],[dt_l1_rlvect_1]) ).
cnf(c_170,plain,
( ~ l2_struct_0(B)
| g1_vectsp_2(B,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(B,A)) = A
| ~ v3_vectsp_2(A,B)
| ~ l1_vectsp_2(A,B) ),
inference(resolve,[status(thm)],[c_135,c_130]) ).
cnf(c_262,plain,
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_263,plain,
r1_tarski(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_264,plain,
m1_subset_1(A,k1_zfmisc_1(A)),
inference(resolve,[status(thm)],[c_263,c_262]) ).
cnf(c_322,plain,
( ~ l1_rlvect_1(B)
| g1_vectsp_2(B,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(B,A)) = A
| ~ v3_vectsp_2(A,B)
| ~ l1_vectsp_2(A,B) ),
inference(resolve,[status(thm)],[c_170,c_147]) ).
cnf(c_449,plain,
( l1_rlvect_1(A)
| ~ l3_vectsp_1(A) ),
inference(clausify,[status(thm)],[dt_l3_vectsp_1]) ).
cnf(c_474,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_475,negated_conjecture,
v3_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_476,negated_conjecture,
v4_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_477,negated_conjecture,
v5_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_478,negated_conjecture,
v6_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_479,negated_conjecture,
v7_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_480,negated_conjecture,
v6_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_481,negated_conjecture,
v7_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_482,negated_conjecture,
v8_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_483,negated_conjecture,
~ v10_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_484,negated_conjecture,
v2_vectsp_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_485,negated_conjecture,
l3_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_486,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_487,negated_conjecture,
v3_rlvect_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_488,negated_conjecture,
v4_rlvect_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_489,negated_conjecture,
v5_rlvect_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_490,negated_conjecture,
v6_rlvect_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_491,negated_conjecture,
v3_vectsp_2(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_492,negated_conjecture,
v5_vectsp_2(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_493,negated_conjecture,
l1_vectsp_2(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_495,negated_conjecture,
u1_struct_0(sK1) = sK2,
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_496,negated_conjecture,
sK2 = u1_struct_0(sK1),
inference(copy,[status(thm)],[c_495]) ).
cnf(c_497,negated_conjecture,
k2_group_1(sK0) != k1_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_498,negated_conjecture,
k1_rmod_5(sK0,sK1,sK2) != sK1,
inference(split_conjunct,[status(thm)],[sk_t14_rmod_5_neg]) ).
cnf(c_499,negated_conjecture,
k1_rmod_5(sK0,sK1,u1_struct_0(sK1)) != sK1,
inference(paramod,[status(thm)],[c_496,c_498]) ).
cnf(c_500,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_72,c_73]) ).
cnf(c_1183,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_474,c_500]) ).
cnf(c_1184,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_475,c_1183]) ).
cnf(c_1185,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_476,c_1184]) ).
cnf(c_1186,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_477,c_1185]) ).
cnf(c_1187,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_478,c_1186]) ).
cnf(c_1188,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_479,c_1187]) ).
cnf(c_1189,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_480,c_1188]) ).
cnf(c_1190,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_481,c_1189]) ).
cnf(c_1191,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_482,c_1190]) ).
cnf(c_1192,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_483,c_1191]) ).
cnf(c_1193,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_484,c_1192]) ).
cnf(c_1194,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| k2_group_1(sK0) = k1_rlvect_1(sK0)
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_485,c_1193]) ).
cnf(c_501,negated_conjecture,
( k1_rmod_5(sK0,A,B) = C
| u1_struct_0(C) != B
| ~ m1_rmod_2(C,sK0,A)
| ~ v3_vectsp_2(C,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_497,c_1194]) ).
cnf(c_564,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_72,c_105]) ).
cnf(c_1195,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_474,c_564]) ).
cnf(c_1196,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_475,c_1195]) ).
cnf(c_1197,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_476,c_1196]) ).
cnf(c_1198,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_477,c_1197]) ).
cnf(c_1199,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_478,c_1198]) ).
cnf(c_1200,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_480,c_1199]) ).
cnf(c_1201,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_481,c_1200]) ).
cnf(c_1202,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_482,c_1201]) ).
cnf(c_565,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,A),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_485,c_1202]) ).
cnf(c_572,negated_conjecture,
( k2_rmod_2(sK0,A) = g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(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_72,c_109]) ).
cnf(c_1203,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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(copy,[status(thm)],[c_572]) ).
cnf(c_1204,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_474,c_1203]) ).
cnf(c_1205,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_475,c_1204]) ).
cnf(c_1206,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_476,c_1205]) ).
cnf(c_1207,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_477,c_1206]) ).
cnf(c_1208,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_478,c_1207]) ).
cnf(c_1209,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_480,c_1208]) ).
cnf(c_1210,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_481,c_1209]) ).
cnf(c_1211,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_482,c_1210]) ).
cnf(c_573,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),u1_vectsp_2(sK0,A)) = k2_rmod_2(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_485,c_1211]) ).
cnf(c_917,plain,
l1_rlvect_1(sK0),
inference(resolve,[status(thm)],[c_485,c_449]) ).
cnf(c_1212,negated_conjecture,
( ~ l1_rlvect_1(sK0)
| g1_vectsp_2(sK0,u1_struct_0(sK1),u1_rlvect_1(sK1),u2_struct_0(sK1),u1_vectsp_2(sK0,sK1)) = sK1
| ~ l1_vectsp_2(sK1,sK0) ),
inference(resolve,[status(thm)],[c_491,c_322]) ).
cnf(c_1213,negated_conjecture,
( ~ l1_rlvect_1(sK0)
| g1_vectsp_2(sK0,u1_struct_0(sK1),u1_rlvect_1(sK1),u2_struct_0(sK1),u1_vectsp_2(sK0,sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_493,c_1212]) ).
cnf(c_927,negated_conjecture,
g1_vectsp_2(sK0,u1_struct_0(sK1),u1_rlvect_1(sK1),u2_struct_0(sK1),u1_vectsp_2(sK0,sK1)) = sK1,
inference(resolve,[status(thm)],[c_917,c_1213]) ).
cnf(c_1214,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,sK1),sK0,sK1)
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v3_rlvect_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_565,c_492]) ).
cnf(c_1215,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,sK1),sK0,sK1)
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v3_rlvect_1(sK1) ),
inference(resolve,[status(thm)],[c_486,c_1214]) ).
cnf(c_1216,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,sK1),sK0,sK1)
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1) ),
inference(resolve,[status(thm)],[c_487,c_1215]) ).
cnf(c_1217,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,sK1),sK0,sK1)
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1) ),
inference(resolve,[status(thm)],[c_488,c_1216]) ).
cnf(c_1218,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,sK1),sK0,sK1)
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1) ),
inference(resolve,[status(thm)],[c_489,c_1217]) ).
cnf(c_1219,negated_conjecture,
( m1_rmod_2(k2_rmod_2(sK0,sK1),sK0,sK1)
| ~ l1_vectsp_2(sK1,sK0) ),
inference(resolve,[status(thm)],[c_490,c_1218]) ).
cnf(c_958,negated_conjecture,
m1_rmod_2(k2_rmod_2(sK0,sK1),sK0,sK1),
inference(resolve,[status(thm)],[c_493,c_1219]) ).
cnf(c_1220,negated_conjecture,
( g1_vectsp_2(sK0,u1_struct_0(sK1),u1_rlvect_1(sK1),u2_struct_0(sK1),u1_vectsp_2(sK0,sK1)) = k2_rmod_2(sK0,sK1)
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v3_rlvect_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_573,c_492]) ).
cnf(c_1221,negated_conjecture,
( sK1 = k2_rmod_2(sK0,sK1)
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v3_rlvect_1(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_927,c_1220]) ).
cnf(c_1222,negated_conjecture,
( k2_rmod_2(sK0,sK1) = sK1
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v3_rlvect_1(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_1221]) ).
cnf(c_1223,negated_conjecture,
( k2_rmod_2(sK0,sK1) = sK1
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| ~ v3_rlvect_1(sK1) ),
inference(resolve,[status(thm)],[c_486,c_1222]) ).
cnf(c_1224,negated_conjecture,
( k2_rmod_2(sK0,sK1) = sK1
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1) ),
inference(resolve,[status(thm)],[c_487,c_1223]) ).
cnf(c_1225,negated_conjecture,
( k2_rmod_2(sK0,sK1) = sK1
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1) ),
inference(resolve,[status(thm)],[c_488,c_1224]) ).
cnf(c_1226,negated_conjecture,
( k2_rmod_2(sK0,sK1) = sK1
| ~ l1_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1) ),
inference(resolve,[status(thm)],[c_489,c_1225]) ).
cnf(c_1227,negated_conjecture,
( k2_rmod_2(sK0,sK1) = sK1
| ~ l1_vectsp_2(sK1,sK0) ),
inference(resolve,[status(thm)],[c_490,c_1226]) ).
cnf(c_978,negated_conjecture,
k2_rmod_2(sK0,sK1) = sK1,
inference(resolve,[status(thm)],[c_493,c_1227]) ).
cnf(c_980,negated_conjecture,
m1_rmod_2(sK1,sK0,sK1),
inference(paramod,[status(thm)],[c_978,c_958]) ).
cnf(c_1228,negated_conjecture,
( k1_rmod_5(sK0,sK1,A) = B
| u1_struct_0(B) != A
| ~ m1_rmod_2(B,sK0,sK1)
| ~ v3_vectsp_2(B,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_vectsp_2(sK1,sK0)
| ~ v5_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| ~ v4_rlvect_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_501,c_487]) ).
cnf(c_1229,negated_conjecture,
( k1_rmod_5(sK0,sK1,A) = B
| u1_struct_0(B) != A
| ~ m1_rmod_2(B,sK0,sK1)
| ~ v3_vectsp_2(B,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_vectsp_2(sK1,sK0)
| ~ v5_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| ~ v5_rlvect_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1228,c_488]) ).
cnf(c_1230,negated_conjecture,
( k1_rmod_5(sK0,sK1,A) = B
| u1_struct_0(B) != A
| ~ m1_rmod_2(B,sK0,sK1)
| ~ v3_vectsp_2(B,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_vectsp_2(sK1,sK0)
| ~ v5_vectsp_2(sK1,sK0)
| ~ v6_rlvect_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1229,c_489]) ).
cnf(c_1231,negated_conjecture,
( k1_rmod_5(sK0,sK1,A) = B
| u1_struct_0(B) != A
| ~ m1_rmod_2(B,sK0,sK1)
| ~ v3_vectsp_2(B,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_vectsp_2(sK1,sK0)
| ~ v5_vectsp_2(sK1,sK0)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1230,c_490]) ).
cnf(c_1232,negated_conjecture,
( k1_rmod_5(sK0,sK1,A) = B
| u1_struct_0(B) != A
| ~ m1_rmod_2(B,sK0,sK1)
| ~ v3_vectsp_2(B,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_vectsp_2(sK1,sK0)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1231,c_492]) ).
cnf(c_1233,negated_conjecture,
( k1_rmod_5(sK0,sK1,A) = B
| u1_struct_0(B) != A
| ~ m1_rmod_2(B,sK0,sK1)
| ~ v3_vectsp_2(B,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1232,c_493]) ).
cnf(c_1234,negated_conjecture,
( k1_rmod_5(sK0,sK1,u1_struct_0(sK1)) = A
| u1_struct_0(A) != u1_struct_0(sK1)
| ~ m1_rmod_2(A,sK0,sK1)
| ~ v3_vectsp_2(A,sK0)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1233,c_264]) ).
cnf(c_1235,negated_conjecture,
( k1_rmod_5(sK0,sK1,u1_struct_0(sK1)) = sK1
| u1_struct_0(sK1) != u1_struct_0(sK1)
| ~ m1_rmod_2(sK1,sK0,sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1234,c_491]) ).
cnf(c_1236,negated_conjecture,
( k1_rmod_5(sK0,sK1,u1_struct_0(sK1)) = sK1
| u1_struct_0(sK1) != u1_struct_0(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1235,c_980]) ).
cnf(c_1237,plain,
( k1_rmod_5(sK0,sK1,u1_struct_0(sK1)) = sK1
| v3_struct_0(sK1) ),
inference(xxres,[status(thm)],[c_1236]) ).
cnf(c_1238,negated_conjecture,
k1_rmod_5(sK0,sK1,u1_struct_0(sK1)) = sK1,
inference(resolve,[status(thm)],[c_486,c_1237]) ).
cnf(c_1182,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_499,c_1238]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG219+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n015.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 21:33:14 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 795045 was started by sandbox2 on n015,
% 0.11/0.37 % Sat Sep 26 21:33:14 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.40
% 0.11/0.40 % From the command line: assign(max_seconds, 300).
% 2.33/0.79
% 2.33/0.79 % SZS status Theorem for theBenchmark
% 2.33/0.79
% 2.33/0.79 % Proof 1 at 0.32 (+ 0.05) seconds.
% 2.33/0.79 % Length of proof is 60.
% 2.33/0.79 % Level of proof is 7.
% 2.33/0.79 % Maximum clause weight is 53.000.
% 2.33/0.79 % Given clauses 466.
% 2.33/0.79
% 2.33/0.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------