%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP644+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:34:57 PM UTC 2026
% Result : Theorem 16.09s 3.23s
% Output : CNFRefutation 11.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 23
% Syntax : Number of formulae : 96 ( 16 unt; 15 def)
% Number of atoms : 461 ( 0 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 605 ( 240 ~; 265 |; 58 &)
% ( 17 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 16 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 73 ( 70 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3813,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k3_group_1(A,B),u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4339,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> v4_group_1(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4404,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_group_2(C,A)
=> ( r1_rlvect_1(C,B)
=> r1_rlvect_1(C,k3_group_1(A,B)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4407,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> m1_group_2(A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4409,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] :
( ( l1_group_1(C)
& v4_group_1(C)
& v3_group_1(C)
& ~ v3_struct_0(C) )
=> ( ( m1_group_2(B,C)
& m1_group_2(A,B) )
=> m1_group_2(A,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4540,axiom,
! [A] :
( ( l1_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> ( l1_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5657,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
<=> r1_rlvect_1(B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5661,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
=> r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5662,negated_conjecture,
~ ! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
=> r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f5661]) ).
fof(f16376,plain,
! [A,B] :
( m1_subset_1(k3_group_1(A,B),u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3813]) ).
fof(f16377,plain,
! [X0,X1] :
( m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f16376]) ).
fof(f17652,plain,
! [A] :
( ! [B] :
( v4_group_1(B)
| ~ m1_group_2(B,A) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4339]) ).
fof(f17653,plain,
! [X0,X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f17652]) ).
fof(f17823,plain,
! [A] :
( ! [B] :
( ! [C] :
( r1_rlvect_1(C,k3_group_1(A,B))
| ~ r1_rlvect_1(C,B)
| ~ m1_group_2(C,A) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4404]) ).
fof(f17824,plain,
! [X0,X1,X2] :
( r1_rlvect_1(X2,k3_group_1(X0,X1))
| ~ r1_rlvect_1(X2,X1)
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f17823]) ).
fof(f17835,plain,
! [A] :
( m1_group_2(A,A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4407]) ).
fof(f17836,plain,
! [X0] :
( m1_group_2(X0,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f17835]) ).
fof(f17839,plain,
! [A] :
( ! [B] :
( ! [C] :
( m1_group_2(A,C)
| ~ m1_group_2(B,C)
| ~ m1_group_2(A,B)
| ~ l1_group_1(C)
| ~ v4_group_1(C)
| ~ v3_group_1(C)
| v3_struct_0(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)],[f4409]) ).
fof(f17840,plain,
! [X0,X1,X2] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X1,X2)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(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)],[f17839]) ).
fof(f18200,plain,
! [A] :
( ! [B] :
( ( l1_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
| ~ m1_group_2(B,A) )
| ~ l1_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4540]) ).
fof(f18201,plain,
! [X0,X1] :
( ~ v3_struct_0(X1)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f18200]) ).
fof(f18202,plain,
! [X0,X1] :
( v3_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f18200]) ).
fof(f18203,plain,
! [X0,X1] :
( l1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f18200]) ).
fof(f22084,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
<=> r1_rlvect_1(B,C) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_group_2(B,A)
| ~ v1_group_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5657]) ).
fof(f22085,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ r1_rlvect_1(B,C)
| r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) )
& ( r1_rlvect_1(B,C)
| ~ r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) ) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_group_2(B,A)
| ~ v1_group_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f22084]) ).
fof(f22086,plain,
! [X0,X1,X2] :
( r1_rlvect_1(X1,X2)
| ~ r2_hidden(X2,k1_funct_1(k1_latsubgr(X0),X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f22085]) ).
fof(f22087,plain,
! [X0,X1,X2] :
( ~ r1_rlvect_1(X1,X2)
| r2_hidden(X2,k1_funct_1(k1_latsubgr(X0),X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f22085]) ).
fof(f22094,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B))
& r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
& m1_subset_1(C,u1_struct_0(A)) )
& m1_group_2(B,A)
& v1_group_1(B) )
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5662]) ).
fof(f22095,plain,
( ~ r2_hidden(k3_group_1(sK1495_skl,sK1497_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))
& r2_hidden(sK1497_skl,k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))
& m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl))
& m1_group_2(sK1496_skl,sK1495_skl)
& v1_group_1(sK1496_skl)
& l1_group_1(sK1495_skl)
& v4_group_1(sK1495_skl)
& v3_group_1(sK1495_skl)
& ~ v3_struct_0(sK1495_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1495_skl,sK1496_skl,sK1497_skl]),skolemize(A,sK1495_skl),skolemize(B,sK1496_skl),skolemize(C,sK1497_skl)],[f22094]) ).
fof(f22096,plain,
~ v3_struct_0(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f22097,plain,
v3_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f22098,plain,
v4_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f22099,plain,
l1_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f22100,plain,
v1_group_1(sK1496_skl),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f22101,plain,
m1_group_2(sK1496_skl,sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f22102,plain,
m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl)),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f22103,plain,
r2_hidden(sK1497_skl,k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f22104,plain,
~ r2_hidden(k3_group_1(sK1495_skl,sK1497_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)),
inference(cnf_transformation,[status(thm)],[f22095]) ).
fof(f27149,plain,
( ~ v3_struct_0(sK1496_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18201,f22101]) ).
fof(f27151,definition,
( sQ612_spl
<=> v3_struct_0(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition]) ).
fof(f27152,plain,
( ~ sQ612_spl
| v3_struct_0(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27151]) ).
fof(f27154,definition,
( sQ613_spl
<=> v3_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f27156,plain,
( sQ613_spl
| ~ v3_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27154]) ).
fof(f27157,definition,
( sQ614_spl
<=> l1_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition]) ).
fof(f27159,plain,
( sQ614_spl
| ~ l1_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27157]) ).
fof(f27160,definition,
( sQ615_spl
<=> v3_struct_0(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition]) ).
fof(f27163,plain,
( ~ sQ615_spl
| ~ sQ614_spl
| ~ sQ613_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f27149,f27151,f27154,f27157,f27160]) ).
fof(f27164,plain,
( sQ614_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27159,f22099]) ).
fof(f27165,plain,
sQ614_spl,
inference(contradiction_clause,[status(thm)],[f27164]) ).
fof(f27166,plain,
( sQ613_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27156,f22097]) ).
fof(f27167,plain,
sQ613_spl,
inference(contradiction_clause,[status(thm)],[f27166]) ).
fof(f27168,plain,
( ~ sQ612_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27152,f22096]) ).
fof(f27169,plain,
~ sQ612_spl,
inference(contradiction_clause,[status(thm)],[f27168]) ).
fof(f27170,plain,
( v3_group_1(sK1496_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18202,f22101]) ).
fof(f27172,definition,
( sQ616_spl
<=> v3_group_1(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition]) ).
fof(f27175,plain,
( sQ616_spl
| ~ sQ614_spl
| ~ sQ613_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f27170,f27151,f27154,f27157,f27172]) ).
fof(f27176,plain,
( l1_group_1(sK1496_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18203,f22101]) ).
fof(f27178,definition,
( sQ617_spl
<=> l1_group_1(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f27181,plain,
( sQ617_spl
| ~ sQ614_spl
| ~ sQ613_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f27176,f27151,f27154,f27157,f27178]) ).
fof(f28484,plain,
( v4_group_1(sK1496_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f17653,f22101]) ).
fof(f28486,definition,
( sQ626_spl
<=> v4_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ626_spl])],[split_symbol_definition]) ).
fof(f28488,plain,
( sQ626_spl
| ~ v4_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f28486]) ).
fof(f28489,definition,
( sQ627_spl
<=> v4_group_1(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition]) ).
fof(f28492,plain,
( sQ627_spl
| ~ sQ614_spl
| ~ sQ626_spl
| ~ sQ613_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f28484,f27151,f27154,f28486,f27157,f28489]) ).
fof(f28493,plain,
( sQ626_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28488,f22098]) ).
fof(f28494,plain,
sQ626_spl,
inference(contradiction_clause,[status(thm)],[f28493]) ).
fof(f28885,plain,
! [X0,X1,X2] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X1,X2)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(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) ),
inference(forward_subsumption_resolution,[status(thm)],[f17840,f18201]) ).
fof(f28886,plain,
! [X0] :
( m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1496_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(sK1496_skl)
| ~ v4_group_1(sK1496_skl)
| ~ v3_group_1(sK1496_skl)
| v3_struct_0(sK1496_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(resolution,[status(thm)],[f28885,f22101]) ).
fof(f28888,definition,
! [X0] :
( sQ628_spl
<=> ( m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1496_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition]) ).
fof(f28889,plain,
! [X0] :
( ~ sQ628_spl
| m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1496_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(component_clause,[status(thm)],[f28888]) ).
fof(f28891,plain,
( ~ sQ614_spl
| ~ sQ626_spl
| ~ sQ613_spl
| sQ612_spl
| ~ sQ617_spl
| ~ sQ627_spl
| ~ sQ616_spl
| sQ615_spl
| sQ628_spl ),
inference(split_clause,[status(thm)],[f28886,f28888,f27160,f27172,f28489,f27178,f27151,f27154,f28486,f27157]) ).
fof(f29014,plain,
( ~ sQ628_spl
| ~ l1_group_1(sK1496_skl)
| ~ v4_group_1(sK1496_skl)
| ~ v3_group_1(sK1496_skl)
| v3_struct_0(sK1496_skl)
| m1_group_2(sK1496_skl,sK1495_skl)
| ~ l1_group_1(sK1496_skl)
| ~ v4_group_1(sK1496_skl)
| ~ v3_group_1(sK1496_skl) ),
inference(resolution,[status(thm)],[f28889,f17836]) ).
fof(f29015,definition,
( sQ629_spl
<=> m1_group_2(sK1496_skl,sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ629_spl])],[split_symbol_definition]) ).
fof(f29018,plain,
( ~ sQ628_spl
| sQ615_spl
| sQ629_spl
| ~ sQ617_spl
| ~ sQ627_spl
| ~ sQ616_spl ),
inference(split_clause,[status(thm)],[f29014,f27172,f28489,f27178,f29015,f27160,f28888]) ).
fof(f30180,plain,
( r1_rlvect_1(sK1496_skl,sK1497_skl)
| ~ m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl))
| ~ m1_group_2(sK1496_skl,sK1495_skl)
| ~ v1_group_1(sK1496_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f22086,f22103]) ).
fof(f30181,definition,
( sQ642_spl
<=> v1_group_1(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ642_spl])],[split_symbol_definition]) ).
fof(f30183,plain,
( sQ642_spl
| ~ v1_group_1(sK1496_skl) ),
inference(component_clause,[status(thm)],[f30181]) ).
fof(f30184,definition,
( sQ643_spl
<=> m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl)) ),
introduced(definition,[new_symbols(definition,[sQ643_spl])],[split_symbol_definition]) ).
fof(f30186,plain,
( sQ643_spl
| ~ m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl)) ),
inference(component_clause,[status(thm)],[f30184]) ).
fof(f30187,definition,
( sQ644_spl
<=> r1_rlvect_1(sK1496_skl,sK1497_skl) ),
introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition]) ).
fof(f30190,plain,
( sQ644_spl
| ~ sQ643_spl
| ~ sQ629_spl
| ~ sQ642_spl
| ~ sQ614_spl
| ~ sQ626_spl
| ~ sQ613_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f30180,f27151,f27154,f28486,f27157,f30181,f29015,f30184,f30187]) ).
fof(f30191,plain,
( sQ643_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30186,f22102]) ).
fof(f30192,plain,
sQ643_spl,
inference(contradiction_clause,[status(thm)],[f30191]) ).
fof(f30193,plain,
( sQ642_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30183,f22100]) ).
fof(f30194,plain,
sQ642_spl,
inference(contradiction_clause,[status(thm)],[f30193]) ).
fof(f30667,plain,
( ~ r1_rlvect_1(sK1496_skl,k3_group_1(sK1495_skl,sK1497_skl))
| ~ m1_subset_1(k3_group_1(sK1495_skl,sK1497_skl),u1_struct_0(sK1495_skl))
| ~ m1_group_2(sK1496_skl,sK1495_skl)
| ~ v1_group_1(sK1496_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f22087,f22104]) ).
fof(f30702,definition,
( sQ646_spl
<=> m1_subset_1(k3_group_1(sK1495_skl,sK1497_skl),u1_struct_0(sK1495_skl)) ),
introduced(definition,[new_symbols(definition,[sQ646_spl])],[split_symbol_definition]) ).
fof(f30704,plain,
( sQ646_spl
| ~ m1_subset_1(k3_group_1(sK1495_skl,sK1497_skl),u1_struct_0(sK1495_skl)) ),
inference(component_clause,[status(thm)],[f30702]) ).
fof(f30705,definition,
( sQ647_spl
<=> r1_rlvect_1(sK1496_skl,k3_group_1(sK1495_skl,sK1497_skl)) ),
introduced(definition,[new_symbols(definition,[sQ647_spl])],[split_symbol_definition]) ).
fof(f30707,plain,
( sQ647_spl
| ~ r1_rlvect_1(sK1496_skl,k3_group_1(sK1495_skl,sK1497_skl)) ),
inference(component_clause,[status(thm)],[f30705]) ).
fof(f30708,plain,
( ~ sQ647_spl
| ~ sQ646_spl
| ~ sQ629_spl
| ~ sQ642_spl
| ~ sQ614_spl
| ~ sQ626_spl
| ~ sQ613_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f30667,f27151,f27154,f28486,f27157,f30181,f29015,f30702,f30705]) ).
fof(f30935,plain,
( sQ647_spl
| ~ r1_rlvect_1(sK1496_skl,sK1497_skl)
| ~ m1_group_2(sK1496_skl,sK1495_skl)
| ~ m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f30707,f17824]) ).
fof(f30936,plain,
( sQ647_spl
| ~ sQ644_spl
| ~ sQ629_spl
| ~ sQ643_spl
| ~ sQ614_spl
| ~ sQ626_spl
| ~ sQ613_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f30935,f27151,f27154,f28486,f27157,f30184,f29015,f30187,f30705]) ).
fof(f31191,plain,
( sQ646_spl
| ~ m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f30704,f16377]) ).
fof(f31192,plain,
( sQ646_spl
| ~ sQ643_spl
| ~ sQ614_spl
| ~ sQ626_spl
| ~ sQ613_spl
| sQ612_spl ),
inference(split_clause,[status(thm)],[f31191,f27151,f27154,f28486,f27157,f30184,f30702]) ).
fof(f31193,plain,
$false,
inference(sat_refutation,[status(thm)],[f27163,f27165,f27167,f27169,f27175,f27181,f28492,f28494,f28891,f29018,f30190,f30192,f30194,f30708,f30936,f31192]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP644+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.56 % Computer : n002.cluster.edu
% 0.10/0.56 % Model : x86_64 x86_64
% 0.10/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.56 % Memory : 8046.5625MB
% 0.10/0.56 % OS : Linux 6.8.0-71-generic
% 0.10/0.56 % CPULimit : 300
% 0.10/0.56 % WCLimit : 300
% 0.10/0.56 % DateTime : Sun Sep 20 20:28:34 UTC 2026
% 0.10/0.56 % CPUTime :
% 0.71/1.15 % Drodi V4.1.1
% 16.09/3.23 % Refutation found
% 16.09/3.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.09/3.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.51/3.35 % Elapsed time: 2.771829 seconds
% 11.51/3.35 % CPU time: 17.198234 seconds
% 11.51/3.35 % Total memory used: 1.078 GB
% 11.51/3.35 % Net memory used: 1.052 GB
%------------------------------------------------------------------------------