%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG218+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 : 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:49 AM UTC 2026
% Result : Theorem 230.89s 31.31s
% Output : CNFRefutation 230.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 14
% Syntax : Number of formulae : 144 ( 47 unt; 0 def)
% Number of atoms : 836 ( 102 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 1192 ( 500 ~; 537 |; 131 &)
% ( 3 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-3 aty)
% Number of variables : 169 ( 0 sgn 46 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d1_tarski,axiom,
! [A,B] :
( B = k1_tarski(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> C = A ) ),
file('theBenchmark.p',d1_tarski) ).
fof(dt_k1_rlvect_1,axiom,
! [A] :
( l2_struct_0(A)
=> m1_subset_1(k1_rlvect_1(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k1_rlvect_1) ).
fof(dt_l1_rlvect_1,axiom,
! [A] :
( l1_rlvect_1(A)
=> l2_struct_0(A) ),
file('theBenchmark.p',dt_l1_rlvect_1) ).
fof(dt_l1_vectsp_2,axiom,
! [A] :
( l1_struct_0(A)
=> ! [B] :
( l1_vectsp_2(B,A)
=> l1_rlvect_1(B) ) ),
file('theBenchmark.p',dt_l1_vectsp_2) ).
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(existence_m1_subset_1,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('theBenchmark.p',existence_m1_subset_1) ).
fof(rc1_xboole_0,axiom,
? [A] : v1_xboole_0(A),
file('theBenchmark.p',rc1_xboole_0) ).
fof(redefinition_k7_rlvect_2,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l1_struct_0(A)
& ~ v3_struct_0(A) )
=> k7_rlvect_2(A,B) = k1_tarski(B) ),
file('theBenchmark.p',redefinition_k7_rlvect_2) ).
fof(t10_rmod_5,axiom,
! [A,B] :
( ( l3_vectsp_1(B)
& v2_vectsp_2(B)
& ~ v10_vectsp_1(B)
& v8_vectsp_1(B)
& v7_vectsp_1(B)
& v6_vectsp_1(B)
& v7_group_1(B)
& v4_group_1(B)
& 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,B)
& v5_vectsp_2(C,B)
& v6_rlvect_1(C)
& v5_rlvect_1(C)
& v4_rlvect_1(C)
& v3_rlvect_1(C)
& ~ v3_struct_0(C) )
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(C)))
=> ( r2_hidden(A,D)
=> r1_rlvect_1(k1_rmod_5(B,C,D),A) ) ) ) ),
file('theBenchmark.p',t10_rmod_5) ).
fof(t2_subset,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t46_rmod_2,axiom,
! [A,B] :
( ( l3_vectsp_1(B)
& v8_vectsp_1(B)
& v7_vectsp_1(B)
& v6_vectsp_1(B)
& v4_group_1(B)
& 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,B)
& v5_vectsp_2(C,B)
& v6_rlvect_1(C)
& v5_rlvect_1(C)
& v4_rlvect_1(C)
& v3_rlvect_1(C)
& ~ v3_struct_0(C) )
=> ( r1_rlvect_1(k1_rmod_2(B,C),A)
<=> A = k1_rlvect_1(C) ) ) ),
file('theBenchmark.p',t46_rmod_2) ).
fof(t6_boole,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('theBenchmark.p',t6_boole) ).
fof(t12_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)
& 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 != k7_rlvect_2(B,k1_rlvect_1(B))
& C != k1_xboole_0
& k1_rmod_5(A,B,C) = k1_rmod_2(A,B) ) ) ) ),
file('theBenchmark.p',t12_rmod_5) ).
fof(t12_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)
& 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 != k7_rlvect_2(B,k1_rlvect_1(B))
& C != k1_xboole_0
& k1_rmod_5(A,B,C) = k1_rmod_2(A,B) ) ) ) ),
inference(assume_negation,[status(cth)],[t12_rmod_5]) ).
fof(nnf_78,plain,
? [A] :
( ? [B] :
( ? [C] :
( k7_rlvect_2(B,k1_rlvect_1(B)) != C
& k1_xboole_0 != C
& k1_rmod_2(A,B) = k1_rmod_5(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) ),
inference(fof_nnf,[status(thm)],[t12_rmod_5_neg]) ).
fof(sk_t12_rmod_5_neg,plain,
( k7_rlvect_2(sK4,k1_rlvect_1(sK4)) != sK5
& k1_xboole_0 != sK5
& k1_rmod_2(sK0,sK4) = k1_rmod_5(sK0,sK4,sK5)
& m1_subset_1(sK5,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)
& 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,sK4,sK5]),skolemize(A,sK0),skolemize(B,sK4),skolemize(C,sK5)],[nnf_78]) ).
cnf(c_79,negated_conjecture,
v4_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_81,plain,
( k1_rlvect_1(B) = C
| ~ r1_rlvect_1(k1_rmod_2(A,B),C)
| ~ 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)],[t46_rmod_2]) ).
cnf(c_82,plain,
( r1_rlvect_1(k1_rmod_5(A,B,C),D)
| ~ r2_hidden(D,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) ),
inference(clausify,[status(thm)],[t10_rmod_5]) ).
cnf(c_125,plain,
( k1_tarski(B) = k7_rlvect_2(A,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k7_rlvect_2]) ).
cnf(c_142,plain,
( l1_struct_0(A)
| ~ l2_struct_0(A) ),
inference(clausify,[status(thm)],[dt_l2_struct_0]) ).
cnf(c_143,plain,
( l1_rlvect_1(B)
| ~ l1_vectsp_2(B,A)
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[dt_l1_vectsp_2]) ).
cnf(c_161,plain,
( l2_struct_0(A)
| ~ l1_rlvect_1(A) ),
inference(clausify,[status(thm)],[dt_l1_rlvect_1]) ).
cnf(c_162,plain,
( m1_subset_1(k1_rlvect_1(A),u1_struct_0(A))
| ~ l2_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_rlvect_1]) ).
cnf(c_184,plain,
( k1_tarski(B) = k7_rlvect_2(A,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| v3_struct_0(A)
| ~ l2_struct_0(A) ),
inference(resolve,[status(thm)],[c_142,c_125]) ).
cnf(c_185,plain,
( ~ l2_struct_0(B)
| l1_rlvect_1(A)
| ~ l1_vectsp_2(A,B) ),
inference(resolve,[status(thm)],[c_143,c_142]) ).
cnf(c_363,plain,
( ~ l1_rlvect_1(B)
| l1_rlvect_1(A)
| ~ l1_vectsp_2(A,B) ),
inference(resolve,[status(thm)],[c_185,c_161]) ).
cnf(c_368,plain,
( ~ l1_rlvect_1(A)
| k1_tarski(B) = k7_rlvect_2(A,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_184,c_161]) ).
cnf(c_369,plain,
( ~ l1_rlvect_1(A)
| k7_rlvect_2(A,B) = k1_tarski(B)
| ~ m1_subset_1(B,u1_struct_0(A))
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_368]) ).
cnf(c_436,plain,
( ~ l1_rlvect_1(A)
| m1_subset_1(k1_rlvect_1(A),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_162,c_161]) ).
fof(nnf_7,plain,
! [A,B] :
( ( ? [C] :
( ( C != A
| ~ r2_hidden(C,B) )
& ( C = A
| r2_hidden(C,B) ) )
| k1_tarski(A) = B )
& ( ! [X0] :
( ( X0 != A
| r2_hidden(X0,B) )
& ( X0 = A
| ~ r2_hidden(X0,B) ) )
| k1_tarski(A) != B ) ),
inference(fof_nnf,[status(thm)],[d1_tarski]) ).
fof(sk_d1_tarski_sk,plain,
! [A,B] :
( ( ( ( sK1(A,B) != A
| ~ r2_hidden(sK1(A,B),B) )
& ( sK1(A,B) = A
| r2_hidden(sK1(A,B),B) ) )
| k1_tarski(A) = B )
& ( ! [X0] :
( ( X0 != A
| r2_hidden(X0,B) )
& ( X0 = A
| ~ r2_hidden(X0,B) ) )
| k1_tarski(A) != B ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(C,sK1(A,B))],[nnf_7]) ).
fof(sk_d1_tarski,plain,
( ! [VAR_0,VAR_1] :
( sK1(VAR_0,VAR_1) != VAR_0
| ~ r2_hidden(sK1(VAR_0,VAR_1),VAR_1)
| k1_tarski(VAR_0) = VAR_1 )
& ! [VAR_0,VAR_1] :
( sK1(VAR_0,VAR_1) = VAR_0
| r2_hidden(sK1(VAR_0,VAR_1),VAR_1)
| k1_tarski(VAR_0) = VAR_1 )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 != VAR_0
| r2_hidden(VAR_2,VAR_1)
| k1_tarski(VAR_0) != VAR_1 )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = VAR_0
| ~ r2_hidden(VAR_2,VAR_1)
| k1_tarski(VAR_0) != VAR_1 ) ),
inference(cnf_transformation,[status(thm)],[sk_d1_tarski_sk]) ).
cnf(c_508,plain,
( sK1(A,B) = A
| r2_hidden(sK1(A,B),B)
| k1_tarski(A) = B ),
inference(split_conjunct,[status(thm)],[sk_d1_tarski]) ).
cnf(c_509,plain,
( sK1(A,B) != A
| ~ r2_hidden(sK1(A,B),B)
| k1_tarski(A) = B ),
inference(split_conjunct,[status(thm)],[sk_d1_tarski]) ).
cnf(c_513,plain,
( l1_rlvect_1(A)
| ~ l3_vectsp_1(A) ),
inference(clausify,[status(thm)],[dt_l3_vectsp_1]) ).
fof(nnf_44,plain,
! [A] :
? [B] : m1_subset_1(B,A),
inference(fof_nnf,[status(thm)],[existence_m1_subset_1]) ).
fof(sk_existence_m1_subset_1,plain,
! [A] : m1_subset_1(sK2(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(B,sK2(A))],[nnf_44]) ).
cnf(c_519,plain,
m1_subset_1(sK2(A),A),
inference(split_conjunct,[status(thm)],[sk_existence_m1_subset_1]) ).
fof(nnf_56,plain,
? [A] : v1_xboole_0(A),
inference(fof_nnf,[status(thm)],[rc1_xboole_0]) ).
fof(sk_rc1_xboole_0,plain,
v1_xboole_0(sK3),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(A,sK3)],[nnf_56]) ).
cnf(c_526,plain,
v1_xboole_0(sK3),
inference(split_conjunct,[status(thm)],[sk_rc1_xboole_0]) ).
cnf(c_534,plain,
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_539,plain,
( k1_xboole_0 = A
| ~ v1_xboole_0(A) ),
inference(clausify,[status(thm)],[t6_boole]) ).
cnf(c_542,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_543,negated_conjecture,
v3_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_544,negated_conjecture,
v4_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_545,negated_conjecture,
v5_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_546,negated_conjecture,
v6_rlvect_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_547,negated_conjecture,
v7_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_548,negated_conjecture,
v6_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_549,negated_conjecture,
v7_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_550,negated_conjecture,
v8_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_551,negated_conjecture,
~ v10_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_552,negated_conjecture,
v2_vectsp_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_553,negated_conjecture,
l3_vectsp_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_554,negated_conjecture,
~ v3_struct_0(sK4),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_555,negated_conjecture,
v3_rlvect_1(sK4),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_556,negated_conjecture,
v4_rlvect_1(sK4),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_557,negated_conjecture,
v5_rlvect_1(sK4),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_558,negated_conjecture,
v6_rlvect_1(sK4),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_559,negated_conjecture,
v5_vectsp_2(sK4,sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_560,negated_conjecture,
l1_vectsp_2(sK4,sK0),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_561,negated_conjecture,
m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4))),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_562,negated_conjecture,
k1_rmod_2(sK0,sK4) = k1_rmod_5(sK0,sK4,sK5),
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_563,negated_conjecture,
k1_rmod_5(sK0,sK4,sK5) = k1_rmod_2(sK0,sK4),
inference(copy,[status(thm)],[c_562]) ).
cnf(c_564,negated_conjecture,
k1_xboole_0 != sK5,
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_565,negated_conjecture,
k7_rlvect_2(sK4,k1_rlvect_1(sK4)) != sK5,
inference(split_conjunct,[status(thm)],[sk_t12_rmod_5_neg]) ).
cnf(c_568,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_79,c_81]) ).
cnf(c_7579,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_542,c_568]) ).
cnf(c_7580,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_543,c_7579]) ).
cnf(c_7581,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_544,c_7580]) ).
cnf(c_7582,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_545,c_7581]) ).
cnf(c_7583,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_546,c_7582]) ).
cnf(c_7584,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_548,c_7583]) ).
cnf(c_7585,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_549,c_7584]) ).
cnf(c_7586,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_550,c_7585]) ).
cnf(c_569,negated_conjecture,
( k1_rlvect_1(A) = B
| ~ r1_rlvect_1(k1_rmod_2(sK0,A),B)
| ~ 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_553,c_7586]) ).
cnf(c_570,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_79,c_82]) ).
cnf(c_7587,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_542,c_570]) ).
cnf(c_7588,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_543,c_7587]) ).
cnf(c_7589,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_544,c_7588]) ).
cnf(c_7590,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_545,c_7589]) ).
cnf(c_7591,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_546,c_7590]) ).
cnf(c_7592,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_547,c_7591]) ).
cnf(c_7593,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_548,c_7592]) ).
cnf(c_7594,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_549,c_7593]) ).
cnf(c_7595,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_550,c_7594]) ).
cnf(c_7596,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_551,c_7595]) ).
cnf(c_7597,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_552,c_7596]) ).
cnf(c_571,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,A,B),C)
| ~ r2_hidden(C,B)
| ~ 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_553,c_7597]) ).
cnf(c_964,plain,
( r2_hidden(sK2(A),A)
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_534,c_519]) ).
cnf(c_1013,plain,
k1_xboole_0 = sK3,
inference(resolve,[status(thm)],[c_539,c_526]) ).
cnf(c_1020,negated_conjecture,
sK3 != sK5,
inference(paramod,[status(thm)],[c_1013,c_564]) ).
cnf(c_1021,plain,
( sK3 = A
| ~ v1_xboole_0(A) ),
inference(paramod,[status(thm)],[c_1013,c_539]) ).
cnf(c_1024,plain,
l1_rlvect_1(sK0),
inference(resolve,[status(thm)],[c_553,c_513]) ).
cnf(c_7598,negated_conjecture,
( ~ l1_rlvect_1(sK0)
| l1_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_560,c_363]) ).
cnf(c_1028,negated_conjecture,
l1_rlvect_1(sK4),
inference(resolve,[status(thm)],[c_1024,c_7598]) ).
cnf(c_7599,negated_conjecture,
( k1_rlvect_1(sK4) = A
| ~ r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| v3_struct_0(sK4) ),
inference(resolve,[status(thm)],[c_569,c_555]) ).
cnf(c_7600,negated_conjecture,
( k1_rlvect_1(sK4) = A
| ~ r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ 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_554,c_7599]) ).
cnf(c_7601,negated_conjecture,
( k1_rlvect_1(sK4) = A
| ~ r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_556,c_7600]) ).
cnf(c_7602,negated_conjecture,
( k1_rlvect_1(sK4) = A
| ~ r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_557,c_7601]) ).
cnf(c_7603,negated_conjecture,
( k1_rlvect_1(sK4) = A
| ~ r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_558,c_7602]) ).
cnf(c_7604,negated_conjecture,
( k1_rlvect_1(sK4) = A
| ~ r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ l1_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_559,c_7603]) ).
cnf(c_1036,negated_conjecture,
( k1_rlvect_1(sK4) = A
| ~ r1_rlvect_1(k1_rmod_2(sK0,sK4),A) ),
inference(resolve,[status(thm)],[c_560,c_7604]) ).
cnf(c_7605,negated_conjecture,
( r1_rlvect_1(k1_rmod_5(sK0,sK4,sK5),A)
| ~ r2_hidden(A,sK5)
| ~ 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_571,c_561]) ).
cnf(c_7606,negated_conjecture,
( r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ r2_hidden(A,sK5)
| ~ 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(paramod,[status(thm)],[c_563,c_7605]) ).
cnf(c_7607,negated_conjecture,
( r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ r2_hidden(A,sK5)
| ~ 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_554,c_7606]) ).
cnf(c_7608,negated_conjecture,
( r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ r2_hidden(A,sK5)
| ~ 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_555,c_7607]) ).
cnf(c_7609,negated_conjecture,
( r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ r2_hidden(A,sK5)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_556,c_7608]) ).
cnf(c_7610,negated_conjecture,
( r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ r2_hidden(A,sK5)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4) ),
inference(resolve,[status(thm)],[c_557,c_7609]) ).
cnf(c_7611,negated_conjecture,
( r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ r2_hidden(A,sK5)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_558,c_7610]) ).
cnf(c_7612,negated_conjecture,
( r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ r2_hidden(A,sK5)
| ~ l1_vectsp_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_559,c_7611]) ).
cnf(c_1039,negated_conjecture,
( r1_rlvect_1(k1_rmod_2(sK0,sK4),A)
| ~ r2_hidden(A,sK5) ),
inference(resolve,[status(thm)],[c_560,c_7612]) ).
cnf(c_1228,plain,
m1_subset_1(k1_rlvect_1(sK4),u1_struct_0(sK4)),
inference(resolve,[status(thm)],[c_1028,c_436]) ).
cnf(c_7613,plain,
( ~ l1_rlvect_1(sK4)
| k7_rlvect_2(sK4,k1_rlvect_1(sK4)) = k1_tarski(k1_rlvect_1(sK4))
| v3_struct_0(sK4) ),
inference(resolve,[status(thm)],[c_1228,c_369]) ).
cnf(c_7614,negated_conjecture,
( ~ l1_rlvect_1(sK4)
| k7_rlvect_2(sK4,k1_rlvect_1(sK4)) = k1_tarski(k1_rlvect_1(sK4)) ),
inference(resolve,[status(thm)],[c_554,c_7613]) ).
cnf(c_1885,negated_conjecture,
k7_rlvect_2(sK4,k1_rlvect_1(sK4)) = k1_tarski(k1_rlvect_1(sK4)),
inference(resolve,[status(thm)],[c_1028,c_7614]) ).
cnf(c_1887,negated_conjecture,
k1_tarski(k1_rlvect_1(sK4)) != sK5,
inference(paramod,[status(thm)],[c_1885,c_565]) ).
cnf(c_2164,plain,
( v1_xboole_0(sK5)
| r1_rlvect_1(k1_rmod_2(sK0,sK4),sK2(sK5)) ),
inference(resolve,[status(thm)],[c_1039,c_964]) ).
cnf(c_2165,plain,
( sK1(A,sK5) = A
| k1_tarski(A) = sK5
| r1_rlvect_1(k1_rmod_2(sK0,sK4),sK1(A,sK5)) ),
inference(resolve,[status(thm)],[c_1039,c_508]) ).
cnf(c_7615,negated_conjecture,
( k1_rlvect_1(sK4) = sK2(sK5)
| ~ 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)
| v1_xboole_0(sK5) ),
inference(resolve,[status(thm)],[c_2164,c_569]) ).
cnf(c_7616,negated_conjecture,
( k1_rlvect_1(sK4) = sK2(sK5)
| ~ 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)
| v1_xboole_0(sK5) ),
inference(resolve,[status(thm)],[c_554,c_7615]) ).
cnf(c_7617,negated_conjecture,
( k1_rlvect_1(sK4) = sK2(sK5)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| v1_xboole_0(sK5) ),
inference(resolve,[status(thm)],[c_555,c_7616]) ).
cnf(c_7618,negated_conjecture,
( k1_rlvect_1(sK4) = sK2(sK5)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| v1_xboole_0(sK5) ),
inference(resolve,[status(thm)],[c_556,c_7617]) ).
cnf(c_7619,negated_conjecture,
( k1_rlvect_1(sK4) = sK2(sK5)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| ~ v6_rlvect_1(sK4)
| v1_xboole_0(sK5) ),
inference(resolve,[status(thm)],[c_557,c_7618]) ).
cnf(c_7620,negated_conjecture,
( k1_rlvect_1(sK4) = sK2(sK5)
| ~ l1_vectsp_2(sK4,sK0)
| ~ v5_vectsp_2(sK4,sK0)
| v1_xboole_0(sK5) ),
inference(resolve,[status(thm)],[c_558,c_7619]) ).
cnf(c_7621,negated_conjecture,
( k1_rlvect_1(sK4) = sK2(sK5)
| ~ l1_vectsp_2(sK4,sK0)
| v1_xboole_0(sK5) ),
inference(resolve,[status(thm)],[c_559,c_7620]) ).
cnf(c_2262,negated_conjecture,
( k1_rlvect_1(sK4) = sK2(sK5)
| v1_xboole_0(sK5) ),
inference(resolve,[status(thm)],[c_560,c_7621]) ).
cnf(c_7622,plain,
( sK3 = sK5
| k1_rlvect_1(sK4) = sK2(sK5) ),
inference(resolve,[status(thm)],[c_2262,c_1021]) ).
cnf(c_2269,negated_conjecture,
k1_rlvect_1(sK4) = sK2(sK5),
inference(resolve,[status(thm)],[c_1020,c_7622]) ).
cnf(c_2277,negated_conjecture,
k1_tarski(sK2(sK5)) != sK5,
inference(paramod,[status(thm)],[c_2269,c_1887]) ).
cnf(c_2282,negated_conjecture,
( sK2(sK5) = A
| ~ r1_rlvect_1(k1_rmod_2(sK0,sK4),A) ),
inference(paramod,[status(thm)],[c_2269,c_1036]) ).
cnf(c_7623,plain,
( sK2(sK5) = sK1(A,sK5)
| sK1(A,sK5) = A
| k1_tarski(A) = sK5 ),
inference(resolve,[status(thm)],[c_2165,c_2282]) ).
cnf(c_7495,plain,
( sK1(A,sK5) = sK2(sK5)
| sK1(A,sK5) = A
| k1_tarski(A) = sK5 ),
inference(copy,[status(thm)],[c_7623]) ).
cnf(c_7624,plain,
( sK1(sK2(sK5),sK5) = sK2(sK5)
| k1_tarski(sK2(sK5)) = sK5 ),
inference(factor,[status(thm)],[c_7495]) ).
cnf(c_7496,negated_conjecture,
sK1(sK2(sK5),sK5) = sK2(sK5),
inference(resolve,[status(thm)],[c_2277,c_7624]) ).
cnf(c_7625,plain,
( ~ r2_hidden(sK1(sK2(sK5),sK5),sK5)
| k1_tarski(sK2(sK5)) = sK5 ),
inference(resolve,[status(thm)],[c_7496,c_509]) ).
cnf(c_7626,plain,
( ~ r2_hidden(sK2(sK5),sK5)
| k1_tarski(sK2(sK5)) = sK5 ),
inference(paramod,[status(thm)],[c_7496,c_7625]) ).
cnf(c_7497,negated_conjecture,
~ r2_hidden(sK2(sK5),sK5),
inference(resolve,[status(thm)],[c_2277,c_7626]) ).
cnf(c_7504,plain,
v1_xboole_0(sK5),
inference(resolve,[status(thm)],[c_7497,c_964]) ).
cnf(c_7627,plain,
sK3 = sK5,
inference(resolve,[status(thm)],[c_7504,c_1021]) ).
cnf(c_7578,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1020,c_7627]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG218+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.09/0.76 % Computer : n004.cluster.edu
% 0.09/0.76 % Model : x86_64 x86_64
% 0.09/0.76 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.76 % Memory : 8046.5625MB
% 0.09/0.76 % OS : Linux 6.8.0-71-generic
% 0.09/0.76 % CPULimit : 300
% 0.09/0.76 % WCLimit : 300
% 0.09/0.76 % DateTime : Sat Sep 26 21:29:39 UTC 2026
% 0.09/0.77 % CPUTime :
% 0.09/0.77 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.77 % Process 2642111 was started by sandbox on n004,
% 0.09/0.77 % Sat Sep 26 21:29:39 2026
% 0.09/0.77 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.80
% 0.09/0.80 % From the command line: assign(max_seconds, 300).
% 230.89/31.31
% 230.89/31.31 % given #500 (I,wt=48): 871 -v1_funct_1(A) | -v1_funct_2(A,k2_zfmisc_1(u1_struct_0(c6),u1_struct_0(c6)),u1_struct_0(c6)) | -m1_relset_1(A,k2_zfmisc_1(u1_struct_0(c6),u1_struct_0(c6)),u1_struct_0(c6)) | -m1_subset_1(B,u1_struct_0(c6)) | v3_vectsp_2(g1_vectsp_2(c6,u1_struct_0(c6),A,B,A),c6). [factor(705,b,f),merge(e),merge(f)].
% 230.89/31.31
% 230.89/31.31 % given #1000 (T,wt=19): 1322 v1_funct_1(u1_rlvect_1(f16(c1))). [resolve(885,a,514,a)].
% 230.89/31.31
% 230.89/31.31 % given #1500 (F,wt=25): 3569 -v3_struct_0(f16(f15(f3(c12)))). [resolve(3556,a,372,b)].
% 230.89/31.31
% 230.89/31.31 % given #2000 (T,wt=22): 2815 -l1_vectsp_2(A,f15(f16(c11))) | l1_rlvect_1(A). [resolve(2801,a,363,c)].
% 230.89/31.31
% 230.89/31.31 % given #2500 (F,wt=27): 5535 -v1_xboole_0(u1_struct_0(k1_rmod_5(c12,c13,f14(c13)))). [resolve(5532,a,424,c),unit_del(a,5510)].
% 230.89/31.31
% 230.89/31.31 % given #3000 (W,wt=24): 6255 f2(c14,A) = f6(c14) | c14 = A | -r2_hidden(A,f2(A,c14)). [resolve(3950,b,502,b)].
% 230.89/31.31
% 230.89/31.31 % SZS status Theorem for theBenchmark
% 230.89/31.31
% 230.89/31.31 % Proof 1 at 4.57 (+ 1.65) seconds.
% 230.89/31.31 % Length of proof is 85.
% 230.89/31.31 % Level of proof is 13.
% 230.89/31.31 % Maximum clause weight is 45.000.
% 230.89/31.31 % Given clauses 3350.
% 230.89/31.31
% 230.89/31.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------