%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP641+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:55 PM UTC 2026
% Result : Theorem 0.45s 1.06s
% Output : CNFRefutation 0.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 23
% Syntax : Number of formulae : 96 ( 13 unt; 15 def)
% Number of atoms : 493 ( 0 equ)
% Maximal formula atoms : 18 ( 5 avg)
% Number of connectives : 665 ( 268 ~; 310 |; 51 &)
% ( 17 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 16 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 74 ( 72 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3812,axiom,
! [A] :
( ( l1_group_1(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k2_group_1(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f4399,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> r1_rlvect_1(B,k2_group_1(A)) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f5658,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) )
=> r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5659,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) )
=> r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B)) ) ),
inference(negated_conjecture,[status(cth)],[f5658]) ).
fof(f16371,plain,
! [A] :
( m1_subset_1(k2_group_1(A),u1_struct_0(A))
| ~ l1_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3812]) ).
fof(f16372,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| ~ l1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f16371]) ).
fof(f17649,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(f17650,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)],[f17649]) ).
fof(f17810,plain,
! [A] :
( ! [B] :
( r1_rlvect_1(B,k2_group_1(A))
| ~ 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)],[f4399]) ).
fof(f17811,plain,
! [X0,X1] :
( r1_rlvect_1(X1,k2_group_1(X0))
| ~ 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)],[f17810]) ).
fof(f17832,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(f17833,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)],[f17832]) ).
fof(f17836,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(f17837,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)],[f17836]) ).
fof(f18197,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(f18198,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)],[f18197]) ).
fof(f18199,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)],[f18197]) ).
fof(f18200,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)],[f18197]) ).
fof(f22081,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(f22082,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)],[f22081]) ).
fof(f22084,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)],[f22082]) ).
fof(f22085,plain,
? [A] :
( ? [B] :
( ~ r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B))
& 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)],[f5659]) ).
fof(f22086,plain,
( ~ r2_hidden(k2_group_1(sK1495_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_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]),skolemize(A,sK1495_skl),skolemize(B,sK1496_skl)],[f22085]) ).
fof(f22087,plain,
~ v3_struct_0(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22086]) ).
fof(f22088,plain,
v3_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22086]) ).
fof(f22089,plain,
v4_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22086]) ).
fof(f22090,plain,
l1_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22086]) ).
fof(f22091,plain,
v1_group_1(sK1496_skl),
inference(cnf_transformation,[status(thm)],[f22086]) ).
fof(f22092,plain,
m1_group_2(sK1496_skl,sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22086]) ).
fof(f22093,plain,
~ r2_hidden(k2_group_1(sK1495_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)),
inference(cnf_transformation,[status(thm)],[f22086]) ).
fof(f26302,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)],[f17650,f22092]) ).
fof(f26303,definition,
( sQ609_spl
<=> v3_struct_0(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition]) ).
fof(f26304,plain,
( ~ sQ609_spl
| v3_struct_0(sK1495_skl) ),
inference(component_clause,[status(thm)],[f26303]) ).
fof(f26306,definition,
( sQ610_spl
<=> v3_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ610_spl])],[split_symbol_definition]) ).
fof(f26308,plain,
( sQ610_spl
| ~ v3_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f26306]) ).
fof(f26309,definition,
( sQ611_spl
<=> v4_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ611_spl])],[split_symbol_definition]) ).
fof(f26311,plain,
( sQ611_spl
| ~ v4_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f26309]) ).
fof(f26312,definition,
( sQ612_spl
<=> l1_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition]) ).
fof(f26314,plain,
( sQ612_spl
| ~ l1_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f26312]) ).
fof(f26315,definition,
( sQ613_spl
<=> v4_group_1(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f26318,plain,
( sQ613_spl
| ~ sQ612_spl
| ~ sQ611_spl
| ~ sQ610_spl
| sQ609_spl ),
inference(split_clause,[status(thm)],[f26302,f26303,f26306,f26309,f26312,f26315]) ).
fof(f26319,plain,
( sQ612_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26314,f22090]) ).
fof(f26320,plain,
sQ612_spl,
inference(contradiction_clause,[status(thm)],[f26319]) ).
fof(f26321,plain,
( sQ611_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26311,f22089]) ).
fof(f26322,plain,
sQ611_spl,
inference(contradiction_clause,[status(thm)],[f26321]) ).
fof(f26323,plain,
( sQ610_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26308,f22088]) ).
fof(f26324,plain,
sQ610_spl,
inference(contradiction_clause,[status(thm)],[f26323]) ).
fof(f26325,plain,
( ~ sQ609_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26304,f22087]) ).
fof(f26326,plain,
~ sQ609_spl,
inference(contradiction_clause,[status(thm)],[f26325]) ).
fof(f26594,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)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f17837,f17650]) ).
fof(f26595,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)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f26594,f22092]) ).
fof(f26600,definition,
! [X0] :
( sQ614_spl
<=> ( m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1496_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition]) ).
fof(f26601,plain,
! [X0] :
( ~ sQ614_spl
| m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1496_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f26600]) ).
fof(f26603,definition,
( sQ615_spl
<=> v3_struct_0(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition]) ).
fof(f26606,definition,
( sQ616_spl
<=> v3_group_1(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition]) ).
fof(f26609,definition,
( sQ617_spl
<=> l1_group_1(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f26612,plain,
( ~ sQ612_spl
| ~ sQ611_spl
| ~ sQ610_spl
| sQ609_spl
| ~ sQ617_spl
| ~ sQ613_spl
| ~ sQ616_spl
| sQ615_spl
| sQ614_spl ),
inference(split_clause,[status(thm)],[f26595,f26600,f26603,f26606,f26315,f26609,f26303,f26306,f26309,f26312]) ).
fof(f26678,plain,
! [X0,X1] :
( ~ sQ614_spl
| ~ m1_group_2(X1,sK1496_skl)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(sK1496_skl)
| ~ v4_group_1(sK1496_skl)
| ~ v3_group_1(sK1496_skl)
| v3_struct_0(sK1496_skl)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f26601,f26594]) ).
fof(f26680,definition,
! [X0,X1] :
( sQ618_spl
<=> ( ~ m1_group_2(X1,sK1496_skl)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition]) ).
fof(f26681,plain,
! [X0,X1] :
( ~ sQ618_spl
| ~ m1_group_2(X1,sK1496_skl)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f26680]) ).
fof(f26683,plain,
( ~ sQ614_spl
| ~ sQ617_spl
| ~ sQ613_spl
| ~ sQ616_spl
| sQ615_spl
| sQ618_spl ),
inference(split_clause,[status(thm)],[f26678,f26680,f26603,f26606,f26315,f26609,f26600]) ).
fof(f26684,definition,
( sQ619_spl
<=> m1_group_2(sK1496_skl,sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ619_spl])],[split_symbol_definition]) ).
fof(f26688,plain,
! [X0,X1] :
( ~ sQ618_spl
| ~ m1_group_2(X1,sK1496_skl)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f26681]) ).
fof(f26694,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)],[f18198,f22092]) ).
fof(f26697,plain,
( ~ sQ615_spl
| ~ sQ612_spl
| ~ sQ610_spl
| sQ609_spl ),
inference(split_clause,[status(thm)],[f26694,f26303,f26306,f26312,f26603]) ).
fof(f26698,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)],[f18199,f22092]) ).
fof(f26700,plain,
( sQ616_spl
| ~ sQ612_spl
| ~ sQ610_spl
| sQ609_spl ),
inference(split_clause,[status(thm)],[f26698,f26303,f26306,f26312,f26606]) ).
fof(f26707,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)],[f18200,f22092]) ).
fof(f26709,plain,
( sQ617_spl
| ~ sQ612_spl
| ~ sQ610_spl
| sQ609_spl ),
inference(split_clause,[status(thm)],[f26707,f26303,f26306,f26312,f26609]) ).
fof(f26889,plain,
! [X0,X1] :
( ~ sQ618_spl
| ~ m1_group_2(X1,sK1496_skl)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f26688,f18198]) ).
fof(f26890,plain,
! [X0] :
( ~ sQ618_spl
| ~ l1_group_1(sK1496_skl)
| ~ v4_group_1(sK1496_skl)
| ~ v3_group_1(sK1496_skl)
| v3_struct_0(sK1496_skl)
| ~ m1_group_2(X0,sK1496_skl)
| ~ l1_group_1(sK1496_skl)
| ~ v4_group_1(sK1496_skl)
| ~ v3_group_1(sK1496_skl)
| v3_struct_0(sK1496_skl)
| m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0) ),
inference(resolution,[status(thm)],[f26889,f17833]) ).
fof(f26891,definition,
! [X0] :
( sQ620_spl
<=> ( ~ m1_group_2(X0,sK1496_skl)
| m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition]) ).
fof(f26892,plain,
! [X0] :
( ~ sQ620_spl
| ~ m1_group_2(X0,sK1496_skl)
| m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0) ),
inference(component_clause,[status(thm)],[f26891]) ).
fof(f26894,plain,
( ~ sQ618_spl
| ~ sQ617_spl
| ~ sQ613_spl
| ~ sQ616_spl
| sQ615_spl
| sQ620_spl ),
inference(split_clause,[status(thm)],[f26890,f26891,f26603,f26606,f26315,f26609,f26680]) ).
fof(f26895,plain,
( ~ sQ620_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)
| ~ v3_group_1(sK1496_skl) ),
inference(resolution,[status(thm)],[f26892,f17833]) ).
fof(f26896,plain,
( ~ sQ620_spl
| ~ sQ613_spl
| sQ615_spl
| sQ619_spl
| ~ sQ617_spl
| ~ sQ616_spl ),
inference(split_clause,[status(thm)],[f26895,f26606,f26609,f26684,f26603,f26315,f26891]) ).
fof(f27007,plain,
( ~ r1_rlvect_1(sK1496_skl,k2_group_1(sK1495_skl))
| ~ m1_subset_1(k2_group_1(sK1495_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)],[f22084,f22093]) ).
fof(f27052,definition,
( sQ621_spl
<=> v1_group_1(sK1496_skl) ),
introduced(definition,[new_symbols(definition,[sQ621_spl])],[split_symbol_definition]) ).
fof(f27054,plain,
( sQ621_spl
| ~ v1_group_1(sK1496_skl) ),
inference(component_clause,[status(thm)],[f27052]) ).
fof(f27055,definition,
( sQ622_spl
<=> m1_subset_1(k2_group_1(sK1495_skl),u1_struct_0(sK1495_skl)) ),
introduced(definition,[new_symbols(definition,[sQ622_spl])],[split_symbol_definition]) ).
fof(f27057,plain,
( sQ622_spl
| ~ m1_subset_1(k2_group_1(sK1495_skl),u1_struct_0(sK1495_skl)) ),
inference(component_clause,[status(thm)],[f27055]) ).
fof(f27058,definition,
( sQ623_spl
<=> r1_rlvect_1(sK1496_skl,k2_group_1(sK1495_skl)) ),
introduced(definition,[new_symbols(definition,[sQ623_spl])],[split_symbol_definition]) ).
fof(f27060,plain,
( sQ623_spl
| ~ r1_rlvect_1(sK1496_skl,k2_group_1(sK1495_skl)) ),
inference(component_clause,[status(thm)],[f27058]) ).
fof(f27061,plain,
( ~ sQ623_spl
| ~ sQ622_spl
| ~ sQ619_spl
| ~ sQ621_spl
| ~ sQ612_spl
| ~ sQ611_spl
| ~ sQ610_spl
| sQ609_spl ),
inference(split_clause,[status(thm)],[f27007,f26303,f26306,f26309,f26312,f27052,f26684,f27055,f27058]) ).
fof(f27062,plain,
( sQ621_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27054,f22091]) ).
fof(f27063,plain,
sQ621_spl,
inference(contradiction_clause,[status(thm)],[f27062]) ).
fof(f27113,plain,
( sQ623_spl
| ~ m1_group_2(sK1496_skl,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)],[f27060,f17811]) ).
fof(f27114,plain,
( sQ623_spl
| ~ sQ619_spl
| ~ sQ612_spl
| ~ sQ611_spl
| ~ sQ610_spl
| sQ609_spl ),
inference(split_clause,[status(thm)],[f27113,f26303,f26306,f26309,f26312,f26684,f27058]) ).
fof(f27115,plain,
( sQ622_spl
| ~ l1_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27057,f16372]) ).
fof(f27117,plain,
( sQ622_spl
| ~ sQ612_spl
| sQ609_spl ),
inference(split_clause,[status(thm)],[f27115,f26303,f26312,f27055]) ).
fof(f27118,plain,
$false,
inference(sat_refutation,[status(thm)],[f26318,f26320,f26322,f26324,f26326,f26612,f26683,f26697,f26700,f26709,f26894,f26896,f27061,f27063,f27114,f27117]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP641+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:26:44 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.32/0.60 % Drodi V4.1.1
% 0.45/1.06 % Refutation found
% 0.45/1.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.45/1.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.88/1.18 % Elapsed time: 0.814642 seconds
% 3.88/1.18 % CPU time: 4.033830 seconds
% 3.88/1.18 % Total memory used: 1.009 GB
% 3.88/1.18 % Net memory used: 997.221 MB
%------------------------------------------------------------------------------