%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP653+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 : n007.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 07:30:40 AM UTC 2026
% Result : Theorem 0.15s 0.50s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 6
% Syntax : Number of formulae : 150 ( 26 unt; 0 def)
% Number of atoms : 1203 ( 0 equ)
% Maximal formula atoms : 23 ( 8 avg)
% Number of connectives : 1880 ( 827 ~; 949 |; 82 &)
% ( 1 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 43 ( 0 sgn 19 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k11_group_4,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k11_group_4(A))
& v10_lattices(k11_group_4(A))
& v3_lattices(k11_group_4(A))
& ~ v3_struct_0(k11_group_4(A)) ) ),
file('theBenchmark.p',dt_k11_group_4) ).
fof(dt_m3_vectsp_8,axiom,
! [A,B] :
( ( l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [C] :
( m3_vectsp_8(C,A,B)
=> ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) ) ) ),
file('theBenchmark.p',dt_m3_vectsp_8) ).
fof(t11_vectsp_8,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( m1_lattice4(C,A,B)
<=> ( m3_vectsp_8(C,A,B)
& m4_vectsp_8(C,A,B) ) ) ) ) ),
file('theBenchmark.p',t11_vectsp_8) ).
fof(t36_latsubgr,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_group_1(B)
& v4_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_group_6(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( v2_funct_1(C)
=> m3_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) ) ),
file('theBenchmark.p',t36_latsubgr) ).
fof(t37_latsubgr,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_group_1(B)
& v4_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_group_6(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> m4_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) ),
file('theBenchmark.p',t37_latsubgr) ).
fof(t38_latsubgr,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_group_1(B)
& v4_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_group_6(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( v2_funct_1(C)
=> m1_lattice4(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) ) ),
file('theBenchmark.p',t38_latsubgr) ).
fof(t38_latsubgr_neg,negated_conjecture,
~ ! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_group_1(B)
& v4_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_group_6(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( v2_funct_1(C)
=> m1_lattice4(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) ) ),
inference(assume_negation,[status(cth)],[t38_latsubgr]) ).
fof(nnf_65,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ m1_lattice4(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B))
& v2_funct_1(C)
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_group_6(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
& l1_group_1(B)
& v4_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t38_latsubgr_neg]) ).
fof(sk_t38_latsubgr_neg,plain,
( ~ m1_lattice4(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
& v2_funct_1(sK0)
& m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
& v1_group_6(sK0,sK1,sK2)
& v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
& v1_funct_1(sK0)
& l1_group_1(sK2)
& v4_group_1(sK2)
& v3_group_1(sK2)
& ~ v3_struct_0(sK2)
& l1_group_1(sK1)
& v4_group_1(sK1)
& v3_group_1(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK0]),skolemize(A,sK1),skolemize(B,sK2),skolemize(C,sK0)],[nnf_65]) ).
cnf(c_66,negated_conjecture,
v1_group_6(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_67,plain,
( m4_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B))
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_group_6(C,A,B)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_group_1(B)
| ~ v4_group_1(B)
| ~ v3_group_1(B)
| v3_struct_0(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t37_latsubgr]) ).
cnf(c_68,plain,
( m3_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B))
| ~ v2_funct_1(C)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_group_6(C,A,B)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_group_1(B)
| ~ v4_group_1(B)
| ~ v3_group_1(B)
| v3_struct_0(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t36_latsubgr]) ).
cnf(c_100,plain,
( ~ m3_vectsp_8(C,A,B)
| ~ m4_vectsp_8(C,A,B)
| m1_lattice4(C,A,B)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t11_vectsp_8]) ).
cnf(c_101,negated_conjecture,
( m3_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_66,c_68]) ).
cnf(c_104,plain,
( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ m3_vectsp_8(C,A,B)
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m3_vectsp_8]) ).
cnf(c_105,plain,
( v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ m3_vectsp_8(C,A,B)
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m3_vectsp_8]) ).
cnf(c_106,plain,
( v1_funct_1(C)
| ~ m3_vectsp_8(C,A,B)
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m3_vectsp_8]) ).
cnf(c_111,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_106,c_101]) ).
cnf(c_114,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_105,c_101]) ).
cnf(c_117,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_104,c_101]) ).
cnf(c_122,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1)
| ~ m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| m1_lattice4(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_100,c_101]) ).
cnf(c_140,plain,
( ~ v3_struct_0(k11_group_4(A))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k11_group_4]) ).
cnf(c_141,plain,
( v10_lattices(k11_group_4(A))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k11_group_4]) ).
cnf(c_142,plain,
( l3_lattices(k11_group_4(A))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k11_group_4]) ).
cnf(c_191,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_192,negated_conjecture,
v3_group_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_193,negated_conjecture,
v4_group_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_194,negated_conjecture,
l1_group_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_195,negated_conjecture,
~ v3_struct_0(sK2),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_196,negated_conjecture,
v3_group_1(sK2),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_197,negated_conjecture,
v4_group_1(sK2),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_198,negated_conjecture,
l1_group_1(sK2),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_199,negated_conjecture,
v1_funct_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_200,negated_conjecture,
v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2)),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_201,negated_conjecture,
m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2)),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_202,negated_conjecture,
v2_funct_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_203,negated_conjecture,
~ m1_lattice4(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2)),
inference(split_conjunct,[status(thm)],[sk_t38_latsubgr_neg]) ).
cnf(c_204,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_66,c_67]) ).
cnf(c_359,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(resolve,[status(thm)],[c_191,c_204]) ).
cnf(c_360,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1) ),
inference(resolve,[status(thm)],[c_192,c_359]) ).
cnf(c_361,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1) ),
inference(resolve,[status(thm)],[c_193,c_360]) ).
cnf(c_362,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_194,c_361]) ).
cnf(c_363,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2) ),
inference(resolve,[status(thm)],[c_195,c_362]) ).
cnf(c_364,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2) ),
inference(resolve,[status(thm)],[c_196,c_363]) ).
cnf(c_365,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2) ),
inference(resolve,[status(thm)],[c_197,c_364]) ).
cnf(c_366,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0) ),
inference(resolve,[status(thm)],[c_198,c_365]) ).
cnf(c_367,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_199,c_366]) ).
cnf(c_368,negated_conjecture,
( m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_200,c_367]) ).
cnf(c_205,negated_conjecture,
m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2)),
inference(resolve,[status(thm)],[c_201,c_368]) ).
cnf(c_369,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1)
| ~ m4_vectsp_8(k3_latsubgr(sK1,sK2,sK0),k11_group_4(sK1),k11_group_4(sK2))
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_203,c_122]) ).
cnf(c_370,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_205,c_369]) ).
cnf(c_371,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_191,c_370]) ).
cnf(c_372,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_192,c_371]) ).
cnf(c_373,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_193,c_372]) ).
cnf(c_374,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_194,c_373]) ).
cnf(c_375,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_195,c_374]) ).
cnf(c_376,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_196,c_375]) ).
cnf(c_377,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_197,c_376]) ).
cnf(c_378,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_198,c_377]) ).
cnf(c_379,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_199,c_378]) ).
cnf(c_380,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_200,c_379]) ).
cnf(c_381,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_201,c_380]) ).
cnf(c_251,negated_conjecture,
( ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_202,c_381]) ).
cnf(c_382,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_191,c_117]) ).
cnf(c_383,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_192,c_382]) ).
cnf(c_384,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_193,c_383]) ).
cnf(c_385,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_194,c_384]) ).
cnf(c_386,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_195,c_385]) ).
cnf(c_387,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_196,c_386]) ).
cnf(c_388,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_197,c_387]) ).
cnf(c_389,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_198,c_388]) ).
cnf(c_390,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_199,c_389]) ).
cnf(c_391,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_200,c_390]) ).
cnf(c_392,negated_conjecture,
( ~ v2_funct_1(sK0)
| m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_201,c_391]) ).
cnf(c_252,negated_conjecture,
( m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_202,c_392]) ).
cnf(c_393,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_191,c_114]) ).
cnf(c_394,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_192,c_393]) ).
cnf(c_395,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_193,c_394]) ).
cnf(c_396,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_194,c_395]) ).
cnf(c_397,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_195,c_396]) ).
cnf(c_398,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_196,c_397]) ).
cnf(c_399,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_197,c_398]) ).
cnf(c_400,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_198,c_399]) ).
cnf(c_401,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_199,c_400]) ).
cnf(c_402,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_200,c_401]) ).
cnf(c_403,negated_conjecture,
( ~ v2_funct_1(sK0)
| v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_201,c_402]) ).
cnf(c_253,negated_conjecture,
( v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_202,c_403]) ).
cnf(c_404,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ v3_group_1(sK1)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_191,c_111]) ).
cnf(c_405,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| ~ v4_group_1(sK1)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_192,c_404]) ).
cnf(c_406,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| ~ l1_group_1(sK1)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_193,c_405]) ).
cnf(c_407,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_194,c_406]) ).
cnf(c_408,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ v3_group_1(sK2)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_195,c_407]) ).
cnf(c_409,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| ~ v4_group_1(sK2)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_196,c_408]) ).
cnf(c_410,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| ~ l1_group_1(sK2)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_197,c_409]) ).
cnf(c_411,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(sK0)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_198,c_410]) ).
cnf(c_412,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_199,c_411]) ).
cnf(c_413,negated_conjecture,
( ~ v2_funct_1(sK0)
| ~ m2_relset_1(sK0,u1_struct_0(sK1),u1_struct_0(sK2))
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_200,c_412]) ).
cnf(c_414,negated_conjecture,
( ~ v2_funct_1(sK0)
| v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_201,c_413]) ).
cnf(c_254,negated_conjecture,
( v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1))
| v3_struct_0(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_202,c_414]) ).
cnf(c_415,negated_conjecture,
( l3_lattices(k11_group_4(sK1))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_193,c_142]) ).
cnf(c_416,negated_conjecture,
( l3_lattices(k11_group_4(sK1))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(resolve,[status(thm)],[c_191,c_415]) ).
cnf(c_417,negated_conjecture,
( l3_lattices(k11_group_4(sK1))
| ~ l1_group_1(sK1) ),
inference(resolve,[status(thm)],[c_192,c_416]) ).
cnf(c_339,negated_conjecture,
l3_lattices(k11_group_4(sK1)),
inference(resolve,[status(thm)],[c_194,c_417]) ).
cnf(c_418,negated_conjecture,
( v10_lattices(k11_group_4(sK1))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_193,c_141]) ).
cnf(c_419,negated_conjecture,
( v10_lattices(k11_group_4(sK1))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(resolve,[status(thm)],[c_191,c_418]) ).
cnf(c_420,negated_conjecture,
( v10_lattices(k11_group_4(sK1))
| ~ l1_group_1(sK1) ),
inference(resolve,[status(thm)],[c_192,c_419]) ).
cnf(c_340,negated_conjecture,
v10_lattices(k11_group_4(sK1)),
inference(resolve,[status(thm)],[c_194,c_420]) ).
cnf(c_421,negated_conjecture,
( ~ v3_struct_0(k11_group_4(sK1))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_193,c_140]) ).
cnf(c_422,negated_conjecture,
( ~ v3_struct_0(k11_group_4(sK1))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(resolve,[status(thm)],[c_191,c_421]) ).
cnf(c_423,negated_conjecture,
( ~ v3_struct_0(k11_group_4(sK1))
| ~ l1_group_1(sK1) ),
inference(resolve,[status(thm)],[c_192,c_422]) ).
cnf(c_341,negated_conjecture,
~ v3_struct_0(k11_group_4(sK1)),
inference(resolve,[status(thm)],[c_194,c_423]) ).
cnf(c_424,negated_conjecture,
( v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_341,c_254]) ).
cnf(c_425,negated_conjecture,
( v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_340,c_424]) ).
cnf(c_343,negated_conjecture,
( v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_339,c_425]) ).
cnf(c_426,negated_conjecture,
( v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_341,c_253]) ).
cnf(c_427,negated_conjecture,
( v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_340,c_426]) ).
cnf(c_344,negated_conjecture,
( v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_339,c_427]) ).
cnf(c_428,negated_conjecture,
( m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_341,c_252]) ).
cnf(c_429,negated_conjecture,
( m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_340,c_428]) ).
cnf(c_345,negated_conjecture,
( m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_339,c_429]) ).
cnf(c_430,negated_conjecture,
( ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1))
| ~ v10_lattices(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_341,c_251]) ).
cnf(c_431,negated_conjecture,
( ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2))
| ~ l3_lattices(k11_group_4(sK1)) ),
inference(resolve,[status(thm)],[c_340,c_430]) ).
cnf(c_346,negated_conjecture,
( ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2))
| v3_struct_0(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_339,c_431]) ).
cnf(c_432,negated_conjecture,
( l3_lattices(k11_group_4(sK2))
| ~ l1_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_197,c_142]) ).
cnf(c_433,negated_conjecture,
( l3_lattices(k11_group_4(sK2))
| ~ l1_group_1(sK2)
| ~ v3_group_1(sK2) ),
inference(resolve,[status(thm)],[c_195,c_432]) ).
cnf(c_434,negated_conjecture,
( l3_lattices(k11_group_4(sK2))
| ~ l1_group_1(sK2) ),
inference(resolve,[status(thm)],[c_196,c_433]) ).
cnf(c_350,negated_conjecture,
l3_lattices(k11_group_4(sK2)),
inference(resolve,[status(thm)],[c_198,c_434]) ).
cnf(c_435,negated_conjecture,
( v10_lattices(k11_group_4(sK2))
| ~ l1_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_197,c_141]) ).
cnf(c_436,negated_conjecture,
( v10_lattices(k11_group_4(sK2))
| ~ l1_group_1(sK2)
| ~ v3_group_1(sK2) ),
inference(resolve,[status(thm)],[c_195,c_435]) ).
cnf(c_437,negated_conjecture,
( v10_lattices(k11_group_4(sK2))
| ~ l1_group_1(sK2) ),
inference(resolve,[status(thm)],[c_196,c_436]) ).
cnf(c_351,negated_conjecture,
v10_lattices(k11_group_4(sK2)),
inference(resolve,[status(thm)],[c_198,c_437]) ).
cnf(c_438,negated_conjecture,
( ~ v3_struct_0(k11_group_4(sK2))
| ~ l1_group_1(sK2)
| ~ v3_group_1(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_197,c_140]) ).
cnf(c_439,negated_conjecture,
( ~ v3_struct_0(k11_group_4(sK2))
| ~ l1_group_1(sK2)
| ~ v3_group_1(sK2) ),
inference(resolve,[status(thm)],[c_195,c_438]) ).
cnf(c_440,negated_conjecture,
( ~ v3_struct_0(k11_group_4(sK2))
| ~ l1_group_1(sK2) ),
inference(resolve,[status(thm)],[c_196,c_439]) ).
cnf(c_352,negated_conjecture,
~ v3_struct_0(k11_group_4(sK2)),
inference(resolve,[status(thm)],[c_198,c_440]) ).
cnf(c_441,negated_conjecture,
( ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_352,c_346]) ).
cnf(c_442,negated_conjecture,
( ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_351,c_441]) ).
cnf(c_354,negated_conjecture,
( ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_1(k3_latsubgr(sK1,sK2,sK0)) ),
inference(resolve,[status(thm)],[c_350,c_442]) ).
cnf(c_443,negated_conjecture,
( m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_352,c_345]) ).
cnf(c_444,negated_conjecture,
( m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_351,c_443]) ).
cnf(c_355,negated_conjecture,
m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2))),
inference(resolve,[status(thm)],[c_350,c_444]) ).
cnf(c_445,negated_conjecture,
( v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_352,c_344]) ).
cnf(c_446,negated_conjecture,
( v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ l3_lattices(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_351,c_445]) ).
cnf(c_356,negated_conjecture,
v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2))),
inference(resolve,[status(thm)],[c_350,c_446]) ).
cnf(c_447,negated_conjecture,
( v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2))
| ~ v10_lattices(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_352,c_343]) ).
cnf(c_448,negated_conjecture,
( v1_funct_1(k3_latsubgr(sK1,sK2,sK0))
| ~ l3_lattices(k11_group_4(sK2)) ),
inference(resolve,[status(thm)],[c_351,c_447]) ).
cnf(c_357,negated_conjecture,
v1_funct_1(k3_latsubgr(sK1,sK2,sK0)),
inference(resolve,[status(thm)],[c_350,c_448]) ).
cnf(c_449,negated_conjecture,
( ~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2)))
| ~ v1_funct_2(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2))) ),
inference(resolve,[status(thm)],[c_357,c_354]) ).
cnf(c_450,negated_conjecture,
~ m2_relset_1(k3_latsubgr(sK1,sK2,sK0),u1_struct_0(k11_group_4(sK1)),u1_struct_0(k11_group_4(sK2))),
inference(resolve,[status(thm)],[c_356,c_449]) ).
cnf(c_358,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_355,c_450]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP653+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 15:25:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1347018 was started by sandbox2 on n007,
% 0.10/0.37 % Fri Sep 25 15:25:54 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.40
% 0.15/0.40 % From the command line: assign(max_seconds, 300).
% 0.15/0.50
% 0.15/0.50 % SZS status Theorem for theBenchmark
% 0.15/0.50
% 0.15/0.50 % Proof 1 at 0.07 (+ 0.01) seconds.
% 0.15/0.50 % Length of proof is 55.
% 0.15/0.50 % Level of proof is 7.
% 0.15/0.50 % Maximum clause weight is 110.000.
% 0.15/0.50 % Given clauses 80.
% 0.15/0.50
% 0.15/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------