%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP653+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 : Thu Sep 24 12:35:00 PM UTC 2026
% Result : Theorem 0.17s 0.52s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 30
% Syntax : Number of formulae : 144 ( 28 unt; 23 def)
% Number of atoms : 724 ( 0 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 956 ( 376 ~; 433 |; 99 &)
% ( 25 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 39 ( 38 usr; 24 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 92 ( 89 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,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(negated_conjecture,[status(cth)],[f1]) ).
fof(f10,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A,B] :
( ( l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [C] :
( m4_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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,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(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f69,plain,
( ~ m1_lattice4(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))
& v2_funct_1(sK2_skl)
& m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
& v1_group_6(sK2_skl,sK0_skl,sK1_skl)
& v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
& v1_funct_1(sK2_skl)
& l1_group_1(sK1_skl)
& v4_group_1(sK1_skl)
& v3_group_1(sK1_skl)
& ~ v3_struct_0(sK1_skl)
& l1_group_1(sK0_skl)
& v4_group_1(sK0_skl)
& v3_group_1(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f68]) ).
fof(f70,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
v3_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f72,plain,
v4_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f73,plain,
l1_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f74,plain,
~ v3_struct_0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f75,plain,
v3_group_1(sK1_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f76,plain,
v4_group_1(sK1_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f77,plain,
l1_group_1(sK1_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f78,plain,
v1_funct_1(sK2_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f79,plain,
v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f80,plain,
v1_group_6(sK2_skl,sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f81,plain,
m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f82,plain,
v2_funct_1(sK2_skl),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f83,plain,
~ m1_lattice4(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f107,plain,
! [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)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f108,plain,
! [X0] :
( ~ v3_struct_0(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f110,plain,
! [X0] :
( v10_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f111,plain,
! [X0] :
( l3_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f131,plain,
! [A,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) )
| ~ 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(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f133,plain,
! [X0,X1,X2] :
( v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m3_vectsp_8(X2,X0,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f135,plain,
! [A,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) )
| ~ m4_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(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f136,plain,
! [X0,X1,X2] :
( v1_funct_1(X2)
| ~ m4_vectsp_8(X2,X0,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f138,plain,
! [X0,X1,X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m4_vectsp_8(X2,X0,X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f233,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( m1_lattice4(C,A,B)
<=> ( m3_vectsp_8(C,A,B)
& m4_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) )
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f234,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ m3_vectsp_8(C,A,B)
| ~ m4_vectsp_8(C,A,B)
| m1_lattice4(C,A,B) )
& ( ( 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(NNF_transformation,[status(thm)],[f233]) ).
fof(f237,plain,
! [X0,X1,X2] :
( ~ m3_vectsp_8(X2,X0,X1)
| ~ m4_vectsp_8(X2,X0,X1)
| m1_lattice4(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f242,plain,
! [A] :
( ! [B] :
( ! [C] :
( 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(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f243,plain,
! [X0,X1,X2] :
( m3_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
| ~ v2_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f244,plain,
! [A] :
( ! [B] :
( ! [C] :
( 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(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f245,plain,
! [X0,X1,X2] :
( m4_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f266,plain,
! [X0,X1,X2] :
( ~ m3_vectsp_8(X2,X0,X1)
| ~ m4_vectsp_8(X2,X0,X1)
| m1_lattice4(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f237,f136]) ).
fof(f273,definition,
( sQ0_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( ~ sQ0_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f273]) ).
fof(f276,definition,
( sQ1_spl
<=> v4_group_1(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( sQ1_spl
| ~ v4_group_1(sK1_skl) ),
inference(component_clause,[status(thm)],[f276]) ).
fof(f279,definition,
( sQ2_spl
<=> l1_group_1(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f281,plain,
( sQ2_spl
| ~ l1_group_1(sK1_skl) ),
inference(component_clause,[status(thm)],[f279]) ).
fof(f286,definition,
( sQ4_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f287,plain,
( ~ sQ4_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f286]) ).
fof(f289,definition,
( sQ5_spl
<=> v4_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f291,plain,
( sQ5_spl
| ~ v4_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f289]) ).
fof(f292,definition,
( sQ6_spl
<=> l1_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f294,plain,
( sQ6_spl
| ~ l1_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f292]) ).
fof(f299,definition,
( sQ8_spl
<=> v3_group_1(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f301,plain,
( sQ8_spl
| ~ v3_group_1(sK1_skl) ),
inference(component_clause,[status(thm)],[f299]) ).
fof(f303,definition,
( sQ9_spl
<=> v3_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f305,plain,
( sQ9_spl
| ~ v3_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f303]) ).
fof(f307,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f294,f73]) ).
fof(f308,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f307]) ).
fof(f309,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f287,f70]) ).
fof(f310,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f309]) ).
fof(f311,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ m3_vectsp_8(X2,X0,k11_group_4(X1))
| ~ m4_vectsp_8(X2,X0,k11_group_4(X1))
| m1_lattice4(X2,X0,k11_group_4(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(k11_group_4(X1)))
| ~ l3_lattices(k11_group_4(X1))
| v3_struct_0(k11_group_4(X1))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f266,f110]) ).
fof(f312,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ m3_vectsp_8(X2,X0,k11_group_4(X1))
| ~ m4_vectsp_8(X2,X0,k11_group_4(X1))
| m1_lattice4(X2,X0,k11_group_4(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(k11_group_4(X1)))
| ~ l3_lattices(k11_group_4(X1))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f311,f108]) ).
fof(f313,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ m3_vectsp_8(X1,X0,k11_group_4(X2))
| ~ m4_vectsp_8(X1,X0,k11_group_4(X2))
| m1_lattice4(X1,X0,k11_group_4(X2))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(k11_group_4(X2)))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(k11_group_4(X2)))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f312,f111]) ).
fof(f314,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ m3_vectsp_8(X1,X0,k11_group_4(X2))
| ~ m4_vectsp_8(X1,X0,k11_group_4(X2))
| m1_lattice4(X1,X0,k11_group_4(X2))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(k11_group_4(X2)))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(k11_group_4(X2)))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f313]) ).
fof(f315,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ m3_vectsp_8(X1,k11_group_4(X0),k11_group_4(X2))
| ~ m4_vectsp_8(X1,k11_group_4(X0),k11_group_4(X2))
| m1_lattice4(X1,k11_group_4(X0),k11_group_4(X2))
| ~ m2_relset_1(X1,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X2)))
| ~ v1_funct_2(X1,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X2)))
| ~ l3_lattices(k11_group_4(X0))
| v3_struct_0(k11_group_4(X0)) ),
inference(resolution,[status(thm)],[f314,f110]) ).
fof(f316,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ m3_vectsp_8(X1,k11_group_4(X0),k11_group_4(X2))
| ~ m4_vectsp_8(X1,k11_group_4(X0),k11_group_4(X2))
| m1_lattice4(X1,k11_group_4(X0),k11_group_4(X2))
| ~ m2_relset_1(X1,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X2)))
| ~ v1_funct_2(X1,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X2)))
| ~ l3_lattices(k11_group_4(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f315,f108]) ).
fof(f317,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ m3_vectsp_8(X0,k11_group_4(X1),k11_group_4(X2))
| ~ m4_vectsp_8(X0,k11_group_4(X1),k11_group_4(X2))
| m1_lattice4(X0,k11_group_4(X1),k11_group_4(X2))
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(X1)),u1_struct_0(k11_group_4(X2)))
| ~ v1_funct_2(X0,u1_struct_0(k11_group_4(X1)),u1_struct_0(k11_group_4(X2))) ),
inference(resolution,[status(thm)],[f316,f111]) ).
fof(f318,plain,
! [X0,X1,X2] :
( ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ m3_vectsp_8(X0,k11_group_4(X1),k11_group_4(X2))
| ~ m4_vectsp_8(X0,k11_group_4(X1),k11_group_4(X2))
| m1_lattice4(X0,k11_group_4(X1),k11_group_4(X2))
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(X1)),u1_struct_0(k11_group_4(X2)))
| ~ v1_funct_2(X0,u1_struct_0(k11_group_4(X1)),u1_struct_0(k11_group_4(X2))) ),
inference(duplicate_literals_removal,[status(thm)],[f317]) ).
fof(f319,plain,
( ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l1_group_1(sK1_skl)
| ~ v4_group_1(sK1_skl)
| ~ v3_group_1(sK1_skl)
| v3_struct_0(sK1_skl)
| ~ m3_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))
| ~ m4_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))
| ~ m2_relset_1(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl)))
| ~ v1_funct_2(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl))) ),
inference(resolution,[status(thm)],[f318,f83]) ).
fof(f320,definition,
( sQ10_spl
<=> v1_funct_2(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f322,plain,
( sQ10_spl
| ~ v1_funct_2(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl))) ),
inference(component_clause,[status(thm)],[f320]) ).
fof(f323,definition,
( sQ11_spl
<=> m2_relset_1(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f325,plain,
( sQ11_spl
| ~ m2_relset_1(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl))) ),
inference(component_clause,[status(thm)],[f323]) ).
fof(f326,definition,
( sQ12_spl
<=> m4_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f328,plain,
( sQ12_spl
| ~ m4_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl)) ),
inference(component_clause,[status(thm)],[f326]) ).
fof(f329,definition,
( sQ13_spl
<=> m3_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( sQ13_spl
| ~ m3_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl)) ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f332,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ9_spl
| sQ4_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ8_spl
| sQ0_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f319,f320,f323,f326,f329,f273,f299,f276,f279,f286,f303,f289,f292]) ).
fof(f333,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f281,f77]) ).
fof(f334,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f333]) ).
fof(f335,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f291,f72]) ).
fof(f336,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f335]) ).
fof(f337,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f274,f74]) ).
fof(f338,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f337]) ).
fof(f339,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f278,f76]) ).
fof(f340,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f339]) ).
fof(f341,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f301,f75]) ).
fof(f342,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f341]) ).
fof(f343,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f305,f71]) ).
fof(f344,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f343]) ).
fof(f345,plain,
( sQ13_spl
| ~ v2_funct_1(sK2_skl)
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_group_6(sK2_skl,sK0_skl,sK1_skl)
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_group_1(sK1_skl)
| ~ v4_group_1(sK1_skl)
| ~ v3_group_1(sK1_skl)
| v3_struct_0(sK1_skl)
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f331,f243]) ).
fof(f347,definition,
( sQ14_spl
<=> v1_funct_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f349,plain,
( sQ14_spl
| ~ v1_funct_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f350,definition,
( sQ15_spl
<=> v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f352,plain,
( sQ15_spl
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f350]) ).
fof(f353,definition,
( sQ16_spl
<=> v1_group_6(sK2_skl,sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f355,plain,
( sQ16_spl
| ~ v1_group_6(sK2_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f356,definition,
( sQ17_spl
<=> m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f358,plain,
( sQ17_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,definition,
( sQ18_spl
<=> v2_funct_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f361,plain,
( sQ18_spl
| ~ v2_funct_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f359]) ).
fof(f362,plain,
( sQ13_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ8_spl
| sQ0_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ9_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f345,f286,f303,f289,f292,f273,f299,f276,f279,f347,f350,f353,f356,f359,f329]) ).
fof(f363,definition,
( sQ19_spl
<=> v3_struct_0(k11_group_4(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f364,plain,
( ~ sQ19_spl
| v3_struct_0(k11_group_4(sK0_skl)) ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f366,definition,
( sQ20_spl
<=> v10_lattices(k11_group_4(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f368,plain,
( sQ20_spl
| ~ v10_lattices(k11_group_4(sK0_skl)) ),
inference(component_clause,[status(thm)],[f366]) ).
fof(f369,definition,
( sQ21_spl
<=> l3_lattices(k11_group_4(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f371,plain,
( sQ21_spl
| ~ l3_lattices(k11_group_4(sK0_skl)) ),
inference(component_clause,[status(thm)],[f369]) ).
fof(f372,definition,
( sQ22_spl
<=> v3_struct_0(k11_group_4(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f373,plain,
( ~ sQ22_spl
| v3_struct_0(k11_group_4(sK1_skl)) ),
inference(component_clause,[status(thm)],[f372]) ).
fof(f375,definition,
( sQ23_spl
<=> v10_lattices(k11_group_4(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( sQ23_spl
| ~ v10_lattices(k11_group_4(sK1_skl)) ),
inference(component_clause,[status(thm)],[f375]) ).
fof(f378,definition,
( sQ24_spl
<=> l3_lattices(k11_group_4(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f380,plain,
( sQ24_spl
| ~ l3_lattices(k11_group_4(sK1_skl)) ),
inference(component_clause,[status(thm)],[f378]) ).
fof(f385,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f361,f82]) ).
fof(f386,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f385]) ).
fof(f387,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f358,f81]) ).
fof(f388,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f387]) ).
fof(f389,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f355,f80]) ).
fof(f390,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f389]) ).
fof(f391,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f352,f79]) ).
fof(f392,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f391]) ).
fof(f393,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f349,f78]) ).
fof(f394,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f393]) ).
fof(f396,plain,
( sQ11_spl
| ~ m4_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))
| ~ l3_lattices(k11_group_4(sK1_skl))
| ~ v10_lattices(k11_group_4(sK1_skl))
| v3_struct_0(k11_group_4(sK1_skl))
| ~ l3_lattices(k11_group_4(sK0_skl))
| ~ v10_lattices(k11_group_4(sK0_skl))
| v3_struct_0(k11_group_4(sK0_skl)) ),
inference(resolution,[status(thm)],[f325,f138]) ).
fof(f403,plain,
( sQ11_spl
| ~ sQ12_spl
| ~ sQ24_spl
| ~ sQ23_spl
| sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f396,f363,f366,f369,f372,f375,f378,f326,f323]) ).
fof(f408,plain,
( sQ10_spl
| ~ m3_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))
| ~ l3_lattices(k11_group_4(sK1_skl))
| ~ v10_lattices(k11_group_4(sK1_skl))
| v3_struct_0(k11_group_4(sK1_skl))
| ~ l3_lattices(k11_group_4(sK0_skl))
| ~ v10_lattices(k11_group_4(sK0_skl))
| v3_struct_0(k11_group_4(sK0_skl)) ),
inference(resolution,[status(thm)],[f322,f133]) ).
fof(f412,plain,
( sQ10_spl
| ~ sQ13_spl
| ~ sQ24_spl
| ~ sQ23_spl
| sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f408,f363,f366,f369,f372,f375,f378,f329,f320]) ).
fof(f414,plain,
( sQ24_spl
| ~ l1_group_1(sK1_skl)
| ~ v4_group_1(sK1_skl)
| ~ v3_group_1(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f380,f111]) ).
fof(f415,plain,
( sQ24_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ8_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f414,f273,f299,f276,f279,f378]) ).
fof(f416,plain,
( sQ12_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_group_6(sK2_skl,sK0_skl,sK1_skl)
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_group_1(sK1_skl)
| ~ v4_group_1(sK1_skl)
| ~ v3_group_1(sK1_skl)
| v3_struct_0(sK1_skl)
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f328,f245]) ).
fof(f418,plain,
( sQ12_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ8_spl
| sQ0_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ9_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f416,f286,f303,f289,f292,f273,f299,f276,f279,f347,f350,f353,f356,f326]) ).
fof(f428,plain,
( sQ23_spl
| ~ l1_group_1(sK1_skl)
| ~ v4_group_1(sK1_skl)
| ~ v3_group_1(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f377,f110]) ).
fof(f429,plain,
( sQ23_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ8_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f428,f273,f299,f276,f279,f375]) ).
fof(f440,plain,
( ~ sQ22_spl
| ~ l1_group_1(sK1_skl)
| ~ v4_group_1(sK1_skl)
| ~ v3_group_1(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f108,f373]) ).
fof(f441,plain,
( ~ sQ22_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ8_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f440,f273,f299,f276,f279,f372]) ).
fof(f444,plain,
( sQ21_spl
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f371,f111]) ).
fof(f445,plain,
( sQ21_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ9_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f444,f286,f303,f289,f292,f369]) ).
fof(f446,plain,
( ~ sQ19_spl
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f364,f108]) ).
fof(f447,plain,
( ~ sQ19_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ9_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f446,f286,f303,f289,f292,f363]) ).
fof(f448,plain,
( sQ20_spl
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f368,f110]) ).
fof(f449,plain,
( sQ20_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ9_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f448,f286,f303,f289,f292,f366]) ).
fof(f450,plain,
$false,
inference(sat_refutation,[status(thm)],[f308,f310,f332,f334,f336,f338,f340,f342,f344,f362,f386,f388,f390,f392,f394,f403,f412,f415,f418,f429,f441,f445,f447,f449]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP653+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n017.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 20 20:23:11 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 0.17/0.52 % Refutation found
% 0.17/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.27/0.54 % Elapsed time: 0.085959 seconds
% 0.27/0.54 % CPU time: 0.331435 seconds
% 0.27/0.54 % Total memory used: 67.748 MB
% 0.27/0.54 % Net memory used: 67.614 MB
%------------------------------------------------------------------------------