%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : ALG220+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 09:46:00 AM UTC 2025
% Result : Theorem 279.96s 35.47s
% Output : CNFRefutation 279.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 5
% Syntax : Number of formulae : 416 ( 380 unt; 0 def)
% Number of atoms : 1169 ( 12 equ)
% Maximal formula atoms : 29 ( 2 avg)
% Number of connectives : 1340 ( 587 ~; 606 |; 125 &)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 55 ( 0 sgn 21 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t16_rmod_5,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v7_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& ~ v10_vectsp_1(A)
& v2_vectsp_2(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v3_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( k1_rmod_5(A,B,C) = B
& r1_tarski(C,D) )
=> k1_rmod_5(A,B,D) = B ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_rmod_5) ).
fof(t16_rmod_5_negated,plain,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v7_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& ~ v10_vectsp_1(A)
& v2_vectsp_2(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v3_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( k1_rmod_5(A,B,C) = B
& r1_tarski(C,D) )
=> k1_rmod_5(A,B,D) = B ) ) ) ) ),
inference(negate_conjecture,[status(cth)],[t16_rmod_5]) ).
cnf(0,plain,
~ v3_struct_0(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l0,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(t33_rmod_2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v3_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( ( ~ v3_struct_0(C)
& v3_rlvect_1(C)
& v4_rlvect_1(C)
& v5_rlvect_1(C)
& v6_rlvect_1(C)
& v3_vectsp_2(C,A)
& v5_vectsp_2(C,A)
& l1_vectsp_2(C,A) )
=> ( ( m1_rmod_2(C,A,B)
& m1_rmod_2(B,A,C) )
=> C = B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_rmod_2) ).
cnf(129,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v3_vectsp_2(X1,X0)
| ~ v3_vectsp_2(X2,X0)
| ~ l1_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X2,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X2,X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(X1,X0,X2)
| ~ m1_rmod_2(X2,X0,X1)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v3_struct_0(X2)
| X2 = X1 ),
inference(cnf,[status(esa)],[t33_rmod_2]) ).
cnf(l1,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v6_rlvect_1(k1_rmod_5(sK1,sK2,sK4))
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v3_vectsp_2(sK2,sK1)
| ~ v3_vectsp_2(k1_rmod_5(sK1,sK2,sK4),sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(k1_rmod_5(sK1,sK2,sK4),sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(k1_rmod_5(sK1,sK2,sK4),sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v3_rlvect_1(k1_rmod_5(sK1,sK2,sK4))
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v4_rlvect_1(k1_rmod_5(sK1,sK2,sK4))
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v5_rlvect_1(k1_rmod_5(sK1,sK2,sK4))
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_2(sK2,sK1,k1_rmod_5(sK1,sK2,sK4))
| ~ m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v3_struct_0(k1_rmod_5(sK1,sK2,sK4))
| k1_rmod_5(sK1,sK2,sK4) = sK2 ),
inference(instantiation,[status(thm)],[129]) ).
cnf(16,plain,
v5_rlvect_1(sK2),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l6135,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(17,plain,
v6_rlvect_1(sK2),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l9,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(1,plain,
v3_rlvect_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l27,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(20,plain,
l1_vectsp_2(sK2,sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l127,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
fof(t15_rmod_5,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v7_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& ~ v10_vectsp_1(A)
& v2_vectsp_2(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( r1_tarski(C,D)
=> m1_rmod_2(k1_rmod_5(A,B,C),A,k1_rmod_5(A,B,D)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_rmod_5) ).
cnf(126,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0)
| ~ r1_tarski(X2,X3)
| v3_struct_0(X0)
| v3_struct_0(X1)
| m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,k1_rmod_5(X0,X1,X3))
| v10_vectsp_1(X0) ),
inference(cnf,[status(esa)],[t15_rmod_5]) ).
cnf(l6218,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| ~ r1_tarski(sK3,sK4)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK3),sK1,k1_rmod_5(sK1,sK2,sK4))
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[126]) ).
cnf(14,plain,
v3_rlvect_1(sK2),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l47,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(23,plain,
k1_rmod_5(sK1,sK2,sK3) = sK2,
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l6141,plain,
k1_rmod_5(sK1,sK2,sK3) = sK2,
inference(instantiation,[status(thm)],[23]) ).
cnf(9,plain,
v8_vectsp_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l7758,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(12,plain,
l3_vectsp_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l7070,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(24,plain,
r1_tarski(sK3,sK4),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l8640,plain,
r1_tarski(sK3,sK4),
inference(instantiation,[status(thm)],[24]) ).
cnf(l7582,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(22,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l7474,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
fof(dt_k1_rmod_5,plain,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v7_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& ~ v10_vectsp_1(A)
& v2_vectsp_2(A)
& l3_vectsp_1(A)
& ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A)
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
=> ( v3_vectsp_2(k1_rmod_5(A,B,C),A)
& m1_rmod_2(k1_rmod_5(A,B,C),A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_rmod_5) ).
cnf(35,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0)
| v3_vectsp_2(k1_rmod_5(X0,X1,X2),X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v10_vectsp_1(X0) ),
inference(cnf,[status(esa)],[dt_k1_rmod_5]) ).
cnf(l8,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_vectsp_2(k1_rmod_5(sK1,sK2,sK3),sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(6,plain,
v7_group_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l268,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(2,plain,
v4_rlvect_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l1264,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(11,plain,
v2_vectsp_2(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l8398,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(13,plain,
~ v3_struct_0(sK2),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l7072,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(19,plain,
v5_vectsp_2(sK2,sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l7478,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(15,plain,
v4_rlvect_1(sK2),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l44,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(36,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,X1)
| v10_vectsp_1(X0) ),
inference(cnf,[status(esa)],[dt_k1_rmod_5]) ).
cnf(l6136,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l7532,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l9123,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(5,plain,
v4_group_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l6267,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l10,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(8,plain,
v7_vectsp_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l7099,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l7087,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(4,plain,
v6_rlvect_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l6237,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l7755,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9164,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(10,plain,
~ v10_vectsp_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l10165,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l8668,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1189,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1258,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1065,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(7,plain,
v6_vectsp_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l2173,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l7573,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(3,plain,
v5_rlvect_1(sK1),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l1263,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
fof(dt_m1_rmod_2,plain,
! [A,B] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A)
& ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_rmod_2(C,A,B)
=> ( ~ v3_struct_0(C)
& v3_rlvect_1(C)
& v4_rlvect_1(C)
& v5_rlvect_1(C)
& v6_rlvect_1(C)
& v5_vectsp_2(C,A)
& l1_vectsp_2(C,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_rmod_2) ).
cnf(48,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(X2,X0,X1)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v4_rlvect_1(X2) ),
inference(cnf,[status(esa)],[dt_m1_rmod_2]) ).
cnf(l124,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v4_rlvect_1(k1_rmod_5(sK1,sK2,sK4)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l171,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(21,plain,
m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l7475,plain,
m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[21]) ).
cnf(l205,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l162,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l9134,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3035,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2937,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l10167,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8670,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l201,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6930,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l10168,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l126,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l10179,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(51,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(X2,X0,X1)
| ~ l3_vectsp_1(X0)
| v5_vectsp_2(X2,X0)
| v3_struct_0(X0)
| v3_struct_0(X1) ),
inference(cnf,[status(esa)],[dt_m1_rmod_2]) ).
cnf(l62,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| ~ l3_vectsp_1(sK1)
| v5_vectsp_2(k1_rmod_5(sK1,sK2,sK4),sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l617,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9113,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2936,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l246,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1094,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1265,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2909,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l23,plain,
k1_rmod_5(sK1,sK2,sK3) = sK2,
inference(instantiation,[status(thm)],[23]) ).
cnf(l7526,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1014,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l555,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(49,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(X2,X0,X1)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v5_rlvect_1(X2) ),
inference(cnf,[status(esa)],[dt_m1_rmod_2]) ).
cnf(l4407,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v5_rlvect_1(k1_rmod_5(sK1,sK2,sK4)) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l1055,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l7327,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l4149,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4458,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l136,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1102,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l9156,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l681,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l7741,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l153,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9116,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7527,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9138,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(47,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(X2,X0,X1)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v3_rlvect_1(X2) ),
inference(cnf,[status(esa)],[dt_m1_rmod_2]) ).
cnf(l30,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v3_rlvect_1(k1_rmod_5(sK1,sK2,sK4)) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l4408,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4586,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1266,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4434,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l4049,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l9124,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1260,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5581,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4422,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1018,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1097,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7574,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1041,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1046,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2938,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4438,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l131,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l957,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4655,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l2174,plain,
m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[21]) ).
cnf(l306,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l721,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1031,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l9112,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4135,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3499,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l160,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l5691,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4432,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l655,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4060,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l150,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1029,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l10648,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l4054,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l239,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4453,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8774,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l7529,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1270,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3276,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l220,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l5687,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5689,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l228,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4142,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l362,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1206,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l226,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5686,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7473,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5692,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l7151,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l615,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1257,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l242,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1015,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l4439,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l128,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l961,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4465,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6068,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l2,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1109,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(50,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(X2,X0,X1)
| ~ l3_vectsp_1(X0)
| v6_rlvect_1(X2)
| v3_struct_0(X0)
| v3_struct_0(X1) ),
inference(cnf,[status(esa)],[dt_m1_rmod_2]) ).
cnf(l48,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| ~ l3_vectsp_1(sK1)
| v6_rlvect_1(k1_rmod_5(sK1,sK2,sK4))
| v3_struct_0(sK1)
| v3_struct_0(sK2) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l4466,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4140,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4480,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l7073,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1034,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4418,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4476,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l173,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l72,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l6064,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4410,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l7118,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l8557,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l10231,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4055,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l5580,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1093,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4485,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5688,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l4143,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l7114,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4472,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4063,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l9161,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4634,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l10228,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l4243,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l190,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l6769,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l5690,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7129,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l238,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10230,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l4423,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l7479,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7346,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l2294,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l7093,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l772,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l7080,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7123,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5579,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4061,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7284,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l754,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8547,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l623,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8555,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3498,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l9166,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8550,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2932,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(52,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(X2,X0,X1)
| ~ l3_vectsp_1(X0)
| l1_vectsp_2(X2,X0)
| v3_struct_0(X0)
| v3_struct_0(X1) ),
inference(cnf,[status(esa)],[dt_m1_rmod_2]) ).
cnf(l70,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| ~ l3_vectsp_1(sK1)
| l1_vectsp_2(k1_rmod_5(sK1,sK2,sK4),sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l326,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4413,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2935,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4455,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4137,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l241,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7422,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l83,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l4420,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11614,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2696,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l854,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4062,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2684,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8556,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l2698,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l5210,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7152,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8553,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4663,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l115,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l2686,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l8559,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2719,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l4440,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l92,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l11529,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l4475,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l371,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1105,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7090,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l274,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4409,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2671,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l281,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l8566,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7157,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2674,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6082,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2695,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4052,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l269,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8544,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l2685,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l2672,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l245,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l9120,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l243,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l240,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1990,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l10654,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l7233,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l77,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7125,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4748,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l11615,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l10246,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1945,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l7091,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(46,plain,
( ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v3_struct_0(X2)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_2(X2,X0,X1)
| ~ l3_vectsp_1(X0)
| v3_struct_0(X0)
| v3_struct_0(X1) ),
inference(cnf,[status(esa)],[dt_m1_rmod_2]) ).
cnf(l8221,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ v3_struct_0(k1_rmod_5(sK1,sK2,sK4))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l8248,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4419,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l10248,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8267,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_2(k1_rmod_5(sK1,sK2,sK4),sK1,sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l10243,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8223,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l273,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l7115,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l10227,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l11120,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4751,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l266,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l8549,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8181,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4479,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8256,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2748,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2673,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8320,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l11128,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l10244,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8289,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l8433,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l250,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1101,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8268,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7131,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2694,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l11618,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l8621,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8280,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l10242,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l8611,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l325,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8619,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8615,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8614,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l6065,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4412,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7106,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l11117,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l8222,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8616,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l10247,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l631,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l8426,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l11516,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4406,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l10255,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8554,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8238,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8618,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(25,plain,
k1_rmod_5(sK1,sK2,sK4) != sK2,
inference(cnf,[status(esa)],[t16_rmod_5_negated]) ).
cnf(l7067,plain,
k1_rmod_5(sK1,sK2,sK4) != sK2,
inference(instantiation,[status(thm)],[25]) ).
cnf(l4136,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10241,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8224,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7074,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8239,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l8266,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l318,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8262,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l11515,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2741,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8620,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l10254,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l11619,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l8265,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8226,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8285,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8667,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l642,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l11507,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l4618,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8545,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l11131,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4621,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l2830,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l11447,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l8612,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1092,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4452,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l11113,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8271,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l8543,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8617,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8249,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l64,plain,
( ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v7_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v5_vectsp_2(sK2,sK1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ v8_vectsp_1(sK1)
| ~ v2_vectsp_2(sK1)
| ~ l3_vectsp_1(sK1)
| v3_vectsp_2(k1_rmod_5(sK1,sK2,sK4),sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v10_vectsp_1(sK1) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l731,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l865,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8235,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1352,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l10259,plain,
~ v10_vectsp_1(sK1),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1166,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l2127,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l122,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1023,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[20]) ).
cnf(l734,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l90,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1779,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8321,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l87,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1275,plain,
v2_vectsp_2(sK1),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1281,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[22]) ).
cnf(l84,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l76,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8610,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1357,plain,
v7_group_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l295,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[12]) ).
cnf(l10266,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1283,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l82,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l74,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l6135,l9,l27,l127,l6218,l47,l6141,l7758,l7070,l8640,l7582,l7474,l8,l268,l1264,l8398,l7072,l7478,l44,l6136,l7532,l9123,l6267,l10,l7099,l7087,l6237,l7755,l9164,l10165,l8668,l1189,l1258,l1065,l2173,l7573,l1263,l124,l171,l7475,l205,l162,l9134,l3035,l2937,l10167,l8670,l201,l6930,l10168,l126,l10179,l62,l617,l9113,l2936,l246,l1094,l1265,l2909,l23,l7526,l1014,l555,l4407,l1055,l7327,l4149,l4458,l136,l1102,l9156,l681,l7741,l153,l9116,l7527,l9138,l30,l4408,l4586,l1266,l4434,l4049,l9124,l1260,l5581,l4422,l1018,l1097,l7574,l1041,l1046,l2938,l4438,l131,l957,l4655,l2174,l306,l721,l1031,l9112,l4135,l3499,l160,l5691,l4432,l655,l4060,l150,l1029,l10648,l4054,l239,l4453,l8774,l7529,l1270,l3276,l220,l5687,l5689,l228,l4142,l362,l1206,l226,l5686,l7473,l5692,l7151,l615,l1257,l242,l1015,l4439,l128,l961,l4465,l6068,l2,l1109,l48,l4466,l4140,l4480,l7073,l1034,l4418,l4476,l173,l72,l6064,l4410,l3,l7118,l8557,l10231,l4055,l5580,l1093,l4485,l5688,l4143,l7114,l4472,l4063,l9161,l4634,l10228,l4243,l190,l6769,l5690,l7129,l238,l10230,l4423,l7479,l7346,l2294,l7093,l772,l7080,l7123,l5579,l4061,l7284,l754,l8547,l623,l8555,l3498,l9166,l8550,l2932,l70,l326,l4413,l2935,l4455,l4137,l241,l7422,l83,l4420,l11614,l2696,l854,l4062,l2684,l8556,l2698,l5210,l7152,l8553,l4663,l115,l2686,l8559,l2719,l4440,l92,l11529,l4475,l371,l1105,l7090,l274,l4409,l2671,l281,l8566,l7157,l2674,l6082,l2695,l4052,l269,l8544,l2685,l7,l2672,l245,l9120,l243,l240,l1990,l10654,l7233,l77,l7125,l4748,l11615,l10246,l1945,l7091,l8221,l8248,l4419,l10248,l8267,l10243,l8223,l273,l7115,l10227,l11120,l4751,l266,l8549,l8181,l4479,l8256,l2748,l2673,l8320,l11128,l10244,l8289,l8433,l250,l1101,l8268,l7131,l2694,l11618,l8621,l8280,l10242,l8611,l325,l8619,l8615,l8614,l6065,l4412,l7106,l11117,l8222,l8616,l10247,l631,l8426,l11516,l4406,l10255,l8554,l8238,l8618,l7067,l4136,l10241,l8224,l7074,l8239,l8266,l318,l8262,l11515,l2741,l8620,l10254,l11619,l8265,l8226,l8285,l8667,l642,l11507,l4618,l8545,l11131,l4621,l2830,l11447,l8612,l1092,l4452,l11113,l8271,l8543,l8617,l8249,l64,l731,l865,l8235,l1352,l10259,l1166,l2127,l122,l1023,l734,l90,l1779,l8321,l87,l1275,l1281,l84,l76,l8610,l1357,l295,l10266,l1283,l82,l74]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.09 % Problem : ALG220+1 : TPTP v9.0.0. Released v3.4.0.
% 0.03/0.09 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.28 % Computer : n032.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Sun Jul 20 02:52:04 EDT 2025
% 0.08/0.28 % CPUTime :
% 0.08/0.29 % launching worker at depth: 3
% 0.08/0.29 % launching worker at depth: 4
% 0.08/0.29 % launching worker at depth: 2
% 0.08/0.29 % launching worker at depth: 1
% 0.08/0.29 % launching worker at depth: 5
% 0.08/0.29 % launching worker at depth: 6
% 0.08/0.29 % launching worker at depth: 7
% 0.08/0.29 % launching worker at depth: 8
% 0.08/0.30 % launching worker at depth: 9
% 0.13/0.35 % launching worker at depth: 10
% 6.39/1.14 % launching worker at depth: 11
% 279.96/35.47 % SZS status Theorem for theBenchmark
% 279.96/35.47 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------