%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG214+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 : n004.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:47 AM UTC 2026
% Result : Theorem 2.20s 0.73s
% Output : CNFRefutation 2.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 3
% Syntax : Number of formulae : 138 ( 28 unt; 0 def)
% Number of atoms : 1465 ( 100 equ)
% Maximal formula atoms : 82 ( 10 avg)
% Number of connectives : 2409 (1082 ~;1192 |; 113 &)
% ( 1 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 10 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 201 ( 0 sgn 38 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d1_rmod_5,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) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ( v1_rmod_5(C,A,B)
<=> ! [D] :
( m2_rmod_4(D,A,B,C)
=> ( k5_rmod_4(A,B,D) = k1_rlvect_1(B)
=> k2_rmod_4(A,B,D) = k1_xboole_0 ) ) ) ) ) ),
file('theBenchmark.p',d1_rmod_5) ).
fof(t25_rmod_4,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) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ! [E] :
( m2_rmod_4(E,A,B,C)
=> ( r1_tarski(C,D)
=> m2_rmod_4(E,A,B,D) ) ) ) ) ) ),
file('theBenchmark.p',t25_rmod_4) ).
fof(t2_rmod_5,conjecture,
! [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) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( v1_rmod_5(D,A,B)
& r1_tarski(C,D) )
=> v1_rmod_5(C,A,B) ) ) ) ) ),
file('theBenchmark.p',t2_rmod_5) ).
fof(t2_rmod_5_neg,negated_conjecture,
~ ! [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) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( v1_rmod_5(D,A,B)
& r1_tarski(C,D) )
=> v1_rmod_5(C,A,B) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t2_rmod_5]) ).
fof(nnf_74,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ~ v1_rmod_5(C,A,B)
& v1_rmod_5(D,A,B)
& 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)
& 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(fof_nnf,[status(thm)],[t2_rmod_5_neg]) ).
fof(sk_t2_rmod_5_neg,plain,
( ~ v1_rmod_5(sK2,sK0,sK4)
& v1_rmod_5(sK3,sK0,sK4)
& r1_tarski(sK2,sK3)
& m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
& m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4)))
& l1_vectsp_2(sK4,sK0)
& v5_vectsp_2(sK4,sK0)
& v6_rlvect_1(sK4)
& v5_rlvect_1(sK4)
& v4_rlvect_1(sK4)
& v3_rlvect_1(sK4)
& ~ v3_struct_0(sK4)
& l3_vectsp_1(sK0)
& v8_vectsp_1(sK0)
& v7_vectsp_1(sK0)
& v6_vectsp_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,sK4,sK2,sK3]),skolemize(A,sK0),skolemize(B,sK4),skolemize(C,sK2),skolemize(D,sK3)],[nnf_74]) ).
cnf(c_75,negated_conjecture,
v4_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_76,plain,
( m2_rmod_4(E,A,B,D)
| ~ r1_tarski(C,D)
| ~ m2_rmod_4(E,A,B,C)
| ~ 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)
| ~ 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)],[t25_rmod_4]) ).
fof(nnf_3,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D] :
( k2_rmod_4(A,B,D) != k1_xboole_0
& k1_rlvect_1(B) = k5_rmod_4(A,B,D)
& m2_rmod_4(D,A,B,C) )
| v1_rmod_5(C,A,B) )
& ( ! [X0] :
( k2_rmod_4(A,B,X0) = k1_xboole_0
| k1_rlvect_1(B) != k5_rmod_4(A,B,X0)
| ~ m2_rmod_4(X0,A,B,C) )
| ~ v1_rmod_5(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)
| ~ 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(fof_nnf,[status(thm)],[d1_rmod_5]) ).
fof(sk_d1_rmod_5_sk,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ( k2_rmod_4(A,B,sK1(A,B,C)) != k1_xboole_0
& k1_rlvect_1(B) = k5_rmod_4(A,B,sK1(A,B,C))
& m2_rmod_4(sK1(A,B,C),A,B,C) )
| v1_rmod_5(C,A,B) )
& ( ! [X0] :
( k2_rmod_4(A,B,X0) = k1_xboole_0
| k1_rlvect_1(B) != k5_rmod_4(A,B,X0)
| ~ m2_rmod_4(X0,A,B,C) )
| ~ v1_rmod_5(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)
| ~ 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(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(D,sK1(A,B,C))],[nnf_3]) ).
fof(sk_d1_rmod_5,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( k2_rmod_4(VAR_0,VAR_1,sK1(VAR_0,VAR_1,VAR_2)) != k1_xboole_0
| v1_rmod_5(VAR_2,VAR_0,VAR_1)
| ~ m1_subset_1(VAR_2,k1_zfmisc_1(u1_struct_0(VAR_1)))
| ~ l1_vectsp_2(VAR_1,VAR_0)
| ~ v5_vectsp_2(VAR_1,VAR_0)
| ~ v6_rlvect_1(VAR_1)
| ~ v5_rlvect_1(VAR_1)
| ~ v4_rlvect_1(VAR_1)
| ~ v3_rlvect_1(VAR_1)
| v3_struct_0(VAR_1)
| ~ l3_vectsp_1(VAR_0)
| ~ v8_vectsp_1(VAR_0)
| ~ v7_vectsp_1(VAR_0)
| ~ v6_vectsp_1(VAR_0)
| ~ v4_group_1(VAR_0)
| ~ v6_rlvect_1(VAR_0)
| ~ v5_rlvect_1(VAR_0)
| ~ v4_rlvect_1(VAR_0)
| ~ v3_rlvect_1(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( k1_rlvect_1(VAR_1) = k5_rmod_4(VAR_0,VAR_1,sK1(VAR_0,VAR_1,VAR_2))
| v1_rmod_5(VAR_2,VAR_0,VAR_1)
| ~ m1_subset_1(VAR_2,k1_zfmisc_1(u1_struct_0(VAR_1)))
| ~ l1_vectsp_2(VAR_1,VAR_0)
| ~ v5_vectsp_2(VAR_1,VAR_0)
| ~ v6_rlvect_1(VAR_1)
| ~ v5_rlvect_1(VAR_1)
| ~ v4_rlvect_1(VAR_1)
| ~ v3_rlvect_1(VAR_1)
| v3_struct_0(VAR_1)
| ~ l3_vectsp_1(VAR_0)
| ~ v8_vectsp_1(VAR_0)
| ~ v7_vectsp_1(VAR_0)
| ~ v6_vectsp_1(VAR_0)
| ~ v4_group_1(VAR_0)
| ~ v6_rlvect_1(VAR_0)
| ~ v5_rlvect_1(VAR_0)
| ~ v4_rlvect_1(VAR_0)
| ~ v3_rlvect_1(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( m2_rmod_4(sK1(VAR_0,VAR_1,VAR_2),VAR_0,VAR_1,VAR_2)
| v1_rmod_5(VAR_2,VAR_0,VAR_1)
| ~ m1_subset_1(VAR_2,k1_zfmisc_1(u1_struct_0(VAR_1)))
| ~ l1_vectsp_2(VAR_1,VAR_0)
| ~ v5_vectsp_2(VAR_1,VAR_0)
| ~ v6_rlvect_1(VAR_1)
| ~ v5_rlvect_1(VAR_1)
| ~ v4_rlvect_1(VAR_1)
| ~ v3_rlvect_1(VAR_1)
| v3_struct_0(VAR_1)
| ~ l3_vectsp_1(VAR_0)
| ~ v8_vectsp_1(VAR_0)
| ~ v7_vectsp_1(VAR_0)
| ~ v6_vectsp_1(VAR_0)
| ~ v4_group_1(VAR_0)
| ~ v6_rlvect_1(VAR_0)
| ~ v5_rlvect_1(VAR_0)
| ~ v4_rlvect_1(VAR_0)
| ~ v3_rlvect_1(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( k2_rmod_4(VAR_0,VAR_1,VAR_3) = k1_xboole_0
| k1_rlvect_1(VAR_1) != k5_rmod_4(VAR_0,VAR_1,VAR_3)
| ~ m2_rmod_4(VAR_3,VAR_0,VAR_1,VAR_2)
| ~ v1_rmod_5(VAR_2,VAR_0,VAR_1)
| ~ m1_subset_1(VAR_2,k1_zfmisc_1(u1_struct_0(VAR_1)))
| ~ l1_vectsp_2(VAR_1,VAR_0)
| ~ v5_vectsp_2(VAR_1,VAR_0)
| ~ v6_rlvect_1(VAR_1)
| ~ v5_rlvect_1(VAR_1)
| ~ v4_rlvect_1(VAR_1)
| ~ v3_rlvect_1(VAR_1)
| v3_struct_0(VAR_1)
| ~ l3_vectsp_1(VAR_0)
| ~ v8_vectsp_1(VAR_0)
| ~ v7_vectsp_1(VAR_0)
| ~ v6_vectsp_1(VAR_0)
| ~ v4_group_1(VAR_0)
| ~ v6_rlvect_1(VAR_0)
| ~ v5_rlvect_1(VAR_0)
| ~ v4_rlvect_1(VAR_0)
| ~ v3_rlvect_1(VAR_0)
| v3_struct_0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d1_rmod_5_sk]) ).
cnf(c_89,plain,
( k2_rmod_4(A,B,sK1(A,B,C)) != k1_xboole_0
| v1_rmod_5(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)
| ~ 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(split_conjunct,[status(thm)],[sk_d1_rmod_5]) ).
cnf(c_90,plain,
( k1_rlvect_1(B) = k5_rmod_4(A,B,sK1(A,B,C))
| v1_rmod_5(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)
| ~ 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(split_conjunct,[status(thm)],[sk_d1_rmod_5]) ).
cnf(c_91,plain,
( m2_rmod_4(sK1(A,B,C),A,B,C)
| v1_rmod_5(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)
| ~ 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(split_conjunct,[status(thm)],[sk_d1_rmod_5]) ).
cnf(c_92,plain,
( k2_rmod_4(A,B,D) = k1_xboole_0
| k1_rlvect_1(B) != k5_rmod_4(A,B,D)
| ~ m2_rmod_4(D,A,B,C)
| ~ v1_rmod_5(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)
| ~ 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(split_conjunct,[status(thm)],[sk_d1_rmod_5]) ).
cnf(c_93,negated_conjecture,
r1_tarski(sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_94,negated_conjecture,
( m2_rmod_4(D,sK0,A,C)
| ~ r1_tarski(B,C)
| ~ m2_rmod_4(D,sK0,A,B)
| ~ 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)
| ~ 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_75,c_76]) ).
cnf(c_300,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k1_rlvect_1(A) != k5_rmod_4(sK0,A,C)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ 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_75,c_92]) ).
cnf(c_301,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ 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_300]) ).
cnf(c_302,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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)
| ~ 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_75,c_91]) ).
cnf(c_303,negated_conjecture,
( k1_rlvect_1(A) = k5_rmod_4(sK0,A,sK1(sK0,A,B))
| v1_rmod_5(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)
| ~ 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_75,c_90]) ).
cnf(c_304,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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)
| ~ 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_303]) ).
cnf(c_305,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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)
| ~ 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_75,c_89]) ).
cnf(c_318,negated_conjecture,
~ v1_rmod_5(sK2,sK0,sK4),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_319,negated_conjecture,
v1_rmod_5(sK3,sK0,sK4),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_320,negated_conjecture,
m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4))),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_321,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4))),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_322,negated_conjecture,
l1_vectsp_2(sK4,sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_323,negated_conjecture,
v5_vectsp_2(sK4,sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_324,negated_conjecture,
v6_rlvect_1(sK4),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_325,negated_conjecture,
v5_rlvect_1(sK4),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_326,negated_conjecture,
v4_rlvect_1(sK4),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_327,negated_conjecture,
v3_rlvect_1(sK4),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_328,negated_conjecture,
~ v3_struct_0(sK4),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_329,negated_conjecture,
l3_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_330,negated_conjecture,
v8_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_331,negated_conjecture,
v7_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_332,negated_conjecture,
v6_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_333,negated_conjecture,
v6_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_334,negated_conjecture,
v5_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_335,negated_conjecture,
v4_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_336,negated_conjecture,
v3_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_337,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t2_rmod_5_neg]) ).
cnf(c_364,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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)
| ~ 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_93,c_94]) ).
cnf(c_2515,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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)
| ~ 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_337,c_364]) ).
cnf(c_2516,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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)
| ~ 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_336,c_2515]) ).
cnf(c_2517,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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)
| ~ 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_335,c_2516]) ).
cnf(c_2518,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_334,c_2517]) ).
cnf(c_2519,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_333,c_2518]) ).
cnf(c_2520,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_332,c_2519]) ).
cnf(c_2521,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_331,c_2520]) ).
cnf(c_2522,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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_330,c_2521]) ).
cnf(c_365,negated_conjecture,
( m2_rmod_4(B,sK0,A,sK3)
| ~ m2_rmod_4(B,sK0,A,sK2)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK2,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_329,c_2522]) ).
cnf(c_2523,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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)
| ~ 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_337,c_305]) ).
cnf(c_2524,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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)
| ~ 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_336,c_2523]) ).
cnf(c_2525,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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)
| ~ 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_335,c_2524]) ).
cnf(c_2526,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_334,c_2525]) ).
cnf(c_2527,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_333,c_2526]) ).
cnf(c_2528,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_332,c_2527]) ).
cnf(c_2529,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_331,c_2528]) ).
cnf(c_2530,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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_330,c_2529]) ).
cnf(c_428,negated_conjecture,
( k2_rmod_4(sK0,A,sK1(sK0,A,B)) != k1_xboole_0
| v1_rmod_5(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_329,c_2530]) ).
cnf(c_2531,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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)
| ~ 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_337,c_304]) ).
cnf(c_2532,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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)
| ~ 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_336,c_2531]) ).
cnf(c_2533,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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)
| ~ 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_335,c_2532]) ).
cnf(c_2534,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_334,c_2533]) ).
cnf(c_2535,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_333,c_2534]) ).
cnf(c_2536,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_332,c_2535]) ).
cnf(c_2537,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_331,c_2536]) ).
cnf(c_2538,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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_330,c_2537]) ).
cnf(c_429,negated_conjecture,
( k5_rmod_4(sK0,A,sK1(sK0,A,B)) = k1_rlvect_1(A)
| v1_rmod_5(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_329,c_2538]) ).
cnf(c_2539,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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)
| ~ 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_337,c_302]) ).
cnf(c_2540,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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)
| ~ 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_336,c_2539]) ).
cnf(c_2541,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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)
| ~ 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_335,c_2540]) ).
cnf(c_2542,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_334,c_2541]) ).
cnf(c_2543,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_333,c_2542]) ).
cnf(c_2544,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_332,c_2543]) ).
cnf(c_2545,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_331,c_2544]) ).
cnf(c_2546,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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_330,c_2545]) ).
cnf(c_430,negated_conjecture,
( m2_rmod_4(sK1(sK0,A,B),sK0,A,B)
| v1_rmod_5(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_329,c_2546]) ).
cnf(c_2547,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ 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_337,c_301]) ).
cnf(c_2548,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ 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_336,c_2547]) ).
cnf(c_2549,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ 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_335,c_2548]) ).
cnf(c_2550,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0)
| ~ v6_rlvect_1(sK0) ),
inference(resolve,[status(thm)],[c_334,c_2549]) ).
cnf(c_2551,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0)
| ~ v6_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_333,c_2550]) ).
cnf(c_2552,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ v8_vectsp_1(sK0)
| ~ v7_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_332,c_2551]) ).
cnf(c_2553,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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)
| ~ v8_vectsp_1(sK0) ),
inference(resolve,[status(thm)],[c_331,c_2552]) ).
cnf(c_2554,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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_330,c_2553]) ).
cnf(c_431,negated_conjecture,
( k2_rmod_4(sK0,A,C) = k1_xboole_0
| k5_rmod_4(sK0,A,C) != k1_rlvect_1(A)
| ~ m2_rmod_4(C,sK0,A,B)
| ~ v1_rmod_5(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_329,c_2554]) ).
cnf(c_2555,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) != k1_xboole_0
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4)
| v3_struct_0(sK4) ),
inference(resolve,[status(thm)],[c_428,c_323]) ).
cnf(c_2556,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) != k1_xboole_0
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_328,c_2555]) ).
cnf(c_2557,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) != k1_xboole_0
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_327,c_2556]) ).
cnf(c_2558,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) != k1_xboole_0
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_326,c_2557]) ).
cnf(c_2559,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) != k1_xboole_0
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_325,c_2558]) ).
cnf(c_2560,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) != k1_xboole_0
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_324,c_2559]) ).
cnf(c_585,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) != k1_xboole_0
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(resolve,[status(thm)],[c_322,c_2560]) ).
cnf(c_2561,negated_conjecture,
( k5_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) = k1_rlvect_1(sK4)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4)
| v3_struct_0(sK4) ),
inference(resolve,[status(thm)],[c_429,c_323]) ).
cnf(c_2562,negated_conjecture,
( k5_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) = k1_rlvect_1(sK4)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_328,c_2561]) ).
cnf(c_2563,negated_conjecture,
( k5_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) = k1_rlvect_1(sK4)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_327,c_2562]) ).
cnf(c_2564,negated_conjecture,
( k5_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) = k1_rlvect_1(sK4)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_326,c_2563]) ).
cnf(c_2565,negated_conjecture,
( k5_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) = k1_rlvect_1(sK4)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_325,c_2564]) ).
cnf(c_2566,negated_conjecture,
( k5_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) = k1_rlvect_1(sK4)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_324,c_2565]) ).
cnf(c_586,negated_conjecture,
( k5_rmod_4(sK0,sK4,sK1(sK0,sK4,A)) = k1_rlvect_1(sK4)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(resolve,[status(thm)],[c_322,c_2566]) ).
cnf(c_2567,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,A),sK0,sK4,A)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4)
| v3_struct_0(sK4) ),
inference(resolve,[status(thm)],[c_430,c_323]) ).
cnf(c_2568,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,A),sK0,sK4,A)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_328,c_2567]) ).
cnf(c_2569,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,A),sK0,sK4,A)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_327,c_2568]) ).
cnf(c_2570,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,A),sK0,sK4,A)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_326,c_2569]) ).
cnf(c_2571,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,A),sK0,sK4,A)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_325,c_2570]) ).
cnf(c_2572,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,A),sK0,sK4,A)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_324,c_2571]) ).
cnf(c_587,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,A),sK0,sK4,A)
| v1_rmod_5(A,sK0,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(resolve,[status(thm)],[c_322,c_2572]) ).
cnf(c_2573,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_xboole_0
| v1_rmod_5(sK2,sK0,sK4) ),
inference(resolve,[status(thm)],[c_585,c_321]) ).
cnf(c_2363,negated_conjecture,
k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_xboole_0,
inference(resolve,[status(thm)],[c_318,c_2573]) ).
cnf(c_2574,negated_conjecture,
( k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_rlvect_1(sK4)
| v1_rmod_5(sK2,sK0,sK4) ),
inference(resolve,[status(thm)],[c_586,c_321]) ).
cnf(c_2434,negated_conjecture,
k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_rlvect_1(sK4),
inference(resolve,[status(thm)],[c_318,c_2574]) ).
cnf(c_2575,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK2)
| v1_rmod_5(sK2,sK0,sK4) ),
inference(resolve,[status(thm)],[c_587,c_321]) ).
cnf(c_2449,negated_conjecture,
m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK2),
inference(resolve,[status(thm)],[c_318,c_2575]) ).
cnf(c_2576,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4)
| v3_struct_0(sK4) ),
inference(resolve,[status(thm)],[c_2449,c_365]) ).
cnf(c_2577,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_328,c_2576]) ).
cnf(c_2578,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_327,c_2577]) ).
cnf(c_2579,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_326,c_2578]) ).
cnf(c_2580,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_325,c_2579]) ).
cnf(c_2581,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_324,c_2580]) ).
cnf(c_2582,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_323,c_2581]) ).
cnf(c_2583,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(resolve,[status(thm)],[c_322,c_2582]) ).
cnf(c_2584,negated_conjecture,
( m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(resolve,[status(thm)],[c_321,c_2583]) ).
cnf(c_2481,negated_conjecture,
m2_rmod_4(sK1(sK0,sK4,sK2),sK0,sK4,sK3),
inference(resolve,[status(thm)],[c_320,c_2584]) ).
cnf(c_2585,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4)
| v3_struct_0(sK4) ),
inference(resolve,[status(thm)],[c_2481,c_431]) ).
cnf(c_2586,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v3_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_328,c_2585]) ).
cnf(c_2587,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_327,c_2586]) ).
cnf(c_2588,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_326,c_2587]) ).
cnf(c_2589,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_325,c_2588]) ).
cnf(c_2590,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_324,c_2589]) ).
cnf(c_2591,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_323,c_2590]) ).
cnf(c_2592,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(resolve,[status(thm)],[c_322,c_2591]) ).
cnf(c_2593,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4)
| ~ v1_rmod_5(sK3,sK0,sK4) ),
inference(resolve,[status(thm)],[c_320,c_2592]) ).
cnf(c_2594,negated_conjecture,
( k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0
| k5_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) != k1_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_319,c_2593]) ).
cnf(c_2595,negated_conjecture,
k2_rmod_4(sK0,sK4,sK1(sK0,sK4,sK2)) = k1_xboole_0,
inference(resolve,[status(thm)],[c_2434,c_2594]) ).
cnf(c_2514,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2363,c_2595]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG214+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 21:26:36 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 2638603 was started by sandbox2 on n004,
% 0.12/0.36 % Sat Sep 26 21:26:36 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.38
% 0.12/0.38 % From the command line: assign(max_seconds, 300).
% 2.20/0.73
% 2.20/0.73 % given #500 (T,wt=19): 2027 l1_rlvect_1(f2(f15(c11))). [resolve(647,a,256,b),unit_del(a,456)].
% 2.20/0.73
% 2.20/0.73 % SZS status Theorem for theBenchmark
% 2.20/0.73
% 2.20/0.73 % Proof 1 at 0.25 (+ 0.07) seconds.
% 2.20/0.73 % Length of proof is 51.
% 2.20/0.73 % Level of proof is 7.
% 2.20/0.73 % Maximum clause weight is 76.000.
% 2.20/0.73 % Given clauses 552.
% 2.20/0.73
% 2.20/0.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------