%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP628+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 : n010.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:51 PM UTC 2026
% Result : Theorem 0.15s 5.47s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 21
% Syntax : Number of formulae : 100 ( 18 unt; 14 def)
% Number of atoms : 444 ( 34 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 572 ( 228 ~; 249 |; 57 &)
% ( 14 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 15 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 70 ( 67 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(k5_autgroup(A)))
=> ( B = C
=> k2_funct_1(B) = k3_group_1(k5_autgroup(A),C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(k5_autgroup(A)))
=> ( B = C
=> k2_funct_1(B) = k3_group_1(k5_autgroup(A),C) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f22,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ( l1_group_1(k3_autgroup(A))
& v4_group_1(k3_autgroup(A))
& v3_group_1(k3_autgroup(A))
& v1_group_1(k3_autgroup(A))
& ~ v3_struct_0(k3_autgroup(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ( m1_group_2(k5_autgroup(A),k3_autgroup(A))
& v1_group_3(k5_autgroup(A),k3_autgroup(A))
& v1_group_1(k5_autgroup(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(k3_autgroup(A)))
=> ( B = C
=> k2_funct_1(B) = k3_group_1(k3_autgroup(A),C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))
=> m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A] :
( ( l1_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(B))
=> m1_subset_1(C,u1_struct_0(A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,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)
=> ! [D] :
( m1_subset_1(D,u1_struct_0(C))
=> ( D = B
=> k3_group_1(C,D) = k3_group_1(A,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,plain,
? [A] :
( ? [B] :
( ? [C] :
( k2_funct_1(B) != k3_group_1(k5_autgroup(A),C)
& B = C
& m1_subset_1(C,u1_struct_0(k5_autgroup(A))) )
& m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A)) )
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f80,plain,
( k2_funct_1(sK1_skl) != k3_group_1(k5_autgroup(sK0_skl),sK2_skl)
& sK1_skl = sK2_skl
& m1_subset_1(sK2_skl,u1_struct_0(k5_autgroup(sK0_skl)))
& m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))
& l1_group_1(sK0_skl)
& v4_group_1(sK0_skl)
& v3_group_1(sK0_skl)
& v1_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)],[f79]) ).
fof(f81,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
v1_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f83,plain,
v3_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f84,plain,
v4_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f85,plain,
l1_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f86,plain,
m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f87,plain,
m1_subset_1(sK2_skl,u1_struct_0(k5_autgroup(sK0_skl))),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f88,plain,
sK1_skl = sK2_skl,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f89,plain,
k2_funct_1(sK1_skl) != k3_group_1(k5_autgroup(sK0_skl),sK2_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f138,plain,
! [A] :
( ( l1_group_1(k3_autgroup(A))
& v4_group_1(k3_autgroup(A))
& v3_group_1(k3_autgroup(A))
& v1_group_1(k3_autgroup(A))
& ~ v3_struct_0(k3_autgroup(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| ~ v1_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f139,plain,
! [X0] :
( ~ v3_struct_0(k3_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f141,plain,
! [X0] :
( v3_group_1(k3_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f142,plain,
! [X0] :
( v4_group_1(k3_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f143,plain,
! [X0] :
( l1_group_1(k3_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f148,plain,
! [A] :
( ( m1_group_2(k5_autgroup(A),k3_autgroup(A))
& v1_group_3(k5_autgroup(A),k3_autgroup(A))
& v1_group_1(k5_autgroup(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| ~ v1_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f151,plain,
! [X0] :
( m1_group_2(k5_autgroup(X0),k3_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f280,plain,
! [A] :
( ! [B] :
( ! [C] :
( k2_funct_1(B) = k3_group_1(k3_autgroup(A),C)
| B != C
| ~ m1_subset_1(C,u1_struct_0(k3_autgroup(A))) )
| ~ m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| ~ v1_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f281,plain,
! [X0,X1,X2] :
( k2_funct_1(X1) = k3_group_1(k3_autgroup(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k3_autgroup(X0)))
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f282,plain,
! [A] :
( ! [B] :
( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))
| ~ m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| ~ v1_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f283,plain,
! [X0,X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f295,plain,
! [A] :
( ! [B] :
( ! [C] :
( m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(C,u1_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)],[f73]) ).
fof(f296,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_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)],[f295]) ).
fof(f297,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( k3_group_1(C,D) = k3_group_1(A,B)
| D != B
| ~ m1_subset_1(D,u1_struct_0(C)) )
| ~ 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)],[f74]) ).
fof(f298,plain,
! [X0,X1,X2,X3] :
( k3_group_1(X2,X3) = k3_group_1(X0,X1)
| X3 != X1
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ 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)],[f297]) ).
fof(f310,plain,
! [X0,X1] :
( k2_funct_1(X1) = k3_group_1(k3_autgroup(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(X0)))
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f281]) ).
fof(f311,plain,
! [X0,X1,X2] :
( k3_group_1(X2,X1) = k3_group_1(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ 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(destructive_equality_resolution,[status(thm)],[f298]) ).
fof(f312,plain,
m1_subset_1(sK1_skl,u1_struct_0(k5_autgroup(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f88,f87]) ).
fof(f313,plain,
k2_funct_1(sK1_skl) != k3_group_1(k5_autgroup(sK0_skl),sK1_skl),
inference(forward_demodulation,[status(thm)],[f88,f89]) ).
fof(f343,definition,
( sQ6_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f344,plain,
( ~ sQ6_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f343]) ).
fof(f346,definition,
( sQ7_spl
<=> v1_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( sQ7_spl
| ~ v1_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f346]) ).
fof(f349,definition,
( sQ8_spl
<=> v3_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( sQ8_spl
| ~ v3_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f349]) ).
fof(f352,definition,
( sQ9_spl
<=> v4_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f354,plain,
( sQ9_spl
| ~ v4_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f355,definition,
( sQ10_spl
<=> l1_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f357,plain,
( sQ10_spl
| ~ l1_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f359,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f357,f85]) ).
fof(f360,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f359]) ).
fof(f361,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f354,f84]) ).
fof(f362,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f361]) ).
fof(f363,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f351,f83]) ).
fof(f364,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f363]) ).
fof(f365,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f348,f82]) ).
fof(f366,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f365]) ).
fof(f367,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f344,f81]) ).
fof(f368,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f367]) ).
fof(f382,plain,
! [X0,X1] :
( k2_funct_1(X1) = k3_group_1(k3_autgroup(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(X0)))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f283,f310]) ).
fof(f386,plain,
! [X0,X1] :
( k2_funct_1(X1) = k3_group_1(k3_autgroup(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(X0)))
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f382]) ).
fof(f448,plain,
( k2_funct_1(sK1_skl) = k3_group_1(k3_autgroup(sK0_skl),sK1_skl)
| ~ m1_subset_1(sK1_skl,u1_struct_0(k3_autgroup(sK0_skl)))
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| ~ v1_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f386,f86]) ).
fof(f450,definition,
( sQ22_spl
<=> m1_subset_1(sK1_skl,u1_struct_0(k3_autgroup(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f453,definition,
( sQ23_spl
<=> k2_funct_1(sK1_skl) = k3_group_1(k3_autgroup(sK0_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( ~ sQ23_spl
| k2_funct_1(sK1_skl) = k3_group_1(k3_autgroup(sK0_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f456,plain,
( sQ23_spl
| ~ sQ22_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f448,f343,f346,f349,f352,f355,f450,f453]) ).
fof(f1210,plain,
! [X0,X1,X2] :
( k3_group_1(X1,X2) = k3_group_1(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f311,f296]) ).
fof(f1214,plain,
! [X0] :
( m1_subset_1(sK1_skl,u1_struct_0(X0))
| ~ m1_group_2(k5_autgroup(sK0_skl),X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f296,f312]) ).
fof(f1216,plain,
( ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| ~ v1_group_1(sK0_skl)
| v3_struct_0(sK0_skl)
| m1_subset_1(sK1_skl,u1_struct_0(k3_autgroup(sK0_skl)))
| ~ l1_group_1(k3_autgroup(sK0_skl))
| ~ v3_group_1(k3_autgroup(sK0_skl))
| v3_struct_0(k3_autgroup(sK0_skl)) ),
inference(resolution,[status(thm)],[f1214,f151]) ).
fof(f1217,definition,
( sQ94_spl
<=> v3_struct_0(k3_autgroup(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1218,plain,
( ~ sQ94_spl
| v3_struct_0(k3_autgroup(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1217]) ).
fof(f1220,definition,
( sQ95_spl
<=> v3_group_1(k3_autgroup(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1222,plain,
( sQ95_spl
| ~ v3_group_1(k3_autgroup(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1220]) ).
fof(f1223,definition,
( sQ96_spl
<=> l1_group_1(k3_autgroup(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1225,plain,
( sQ96_spl
| ~ l1_group_1(k3_autgroup(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1223]) ).
fof(f1226,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl
| sQ22_spl
| ~ sQ96_spl
| ~ sQ95_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f1216,f1217,f1220,f1223,f450,f343,f346,f349,f352,f355]) ).
fof(f1229,plain,
( sQ96_spl
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| ~ v1_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1225,f143]) ).
fof(f1230,plain,
( sQ96_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1229,f343,f346,f349,f352,f355,f1223]) ).
fof(f1238,plain,
( sQ95_spl
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| ~ v1_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1222,f141]) ).
fof(f1239,plain,
( sQ95_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1238,f343,f346,f349,f352,f355,f1220]) ).
fof(f1240,plain,
( ~ sQ94_spl
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| ~ v1_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1218,f139]) ).
fof(f1241,plain,
( ~ sQ94_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1240,f343,f346,f349,f352,f355,f1217]) ).
fof(f1275,plain,
! [X0] :
( ~ sQ23_spl
| k3_group_1(X0,sK1_skl) = k2_funct_1(sK1_skl)
| ~ m1_subset_1(sK1_skl,u1_struct_0(X0))
| ~ m1_group_2(X0,k3_autgroup(sK0_skl))
| ~ l1_group_1(k3_autgroup(sK0_skl))
| ~ v4_group_1(k3_autgroup(sK0_skl))
| ~ v3_group_1(k3_autgroup(sK0_skl))
| v3_struct_0(k3_autgroup(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f454,f1210]) ).
fof(f1288,definition,
( sQ100_spl
<=> v4_group_1(k3_autgroup(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1290,plain,
( sQ100_spl
| ~ v4_group_1(k3_autgroup(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1288]) ).
fof(f1292,definition,
! [X0] :
( sQ101_spl
<=> ( k3_group_1(X0,sK1_skl) = k2_funct_1(sK1_skl)
| ~ m1_subset_1(sK1_skl,u1_struct_0(X0))
| ~ m1_group_2(X0,k3_autgroup(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1293,plain,
! [X0] :
( ~ sQ101_spl
| k3_group_1(X0,sK1_skl) = k2_funct_1(sK1_skl)
| ~ m1_subset_1(sK1_skl,u1_struct_0(X0))
| ~ m1_group_2(X0,k3_autgroup(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1292]) ).
fof(f1295,plain,
( ~ sQ23_spl
| sQ101_spl
| ~ sQ96_spl
| ~ sQ100_spl
| ~ sQ95_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f1275,f1217,f1220,f1288,f1223,f1292,f453]) ).
fof(f1315,plain,
( sQ100_spl
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| ~ v1_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1290,f142]) ).
fof(f1316,plain,
( sQ100_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1315,f343,f346,f349,f352,f355,f1288]) ).
fof(f1508,plain,
( ~ sQ101_spl
| ~ m1_subset_1(sK1_skl,u1_struct_0(k5_autgroup(sK0_skl)))
| ~ m1_group_2(k5_autgroup(sK0_skl),k3_autgroup(sK0_skl)) ),
inference(resolution,[status(thm)],[f1293,f313]) ).
fof(f1510,definition,
( sQ126_spl
<=> m1_group_2(k5_autgroup(sK0_skl),k3_autgroup(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1512,plain,
( sQ126_spl
| ~ m1_group_2(k5_autgroup(sK0_skl),k3_autgroup(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1510]) ).
fof(f1513,definition,
( sQ127_spl
<=> m1_subset_1(sK1_skl,u1_struct_0(k5_autgroup(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1515,plain,
( sQ127_spl
| ~ m1_subset_1(sK1_skl,u1_struct_0(k5_autgroup(sK0_skl))) ),
inference(component_clause,[status(thm)],[f1513]) ).
fof(f1516,plain,
( ~ sQ101_spl
| ~ sQ127_spl
| ~ sQ126_spl ),
inference(split_clause,[status(thm)],[f1508,f1510,f1513,f1292]) ).
fof(f1518,plain,
( sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1515,f312]) ).
fof(f1519,plain,
sQ127_spl,
inference(contradiction_clause,[status(thm)],[f1518]) ).
fof(f1520,plain,
( sQ126_spl
| ~ l1_group_1(sK0_skl)
| ~ v4_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| ~ v1_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1512,f151]) ).
fof(f1521,plain,
( sQ126_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1520,f343,f346,f349,f352,f355,f1510]) ).
fof(f1522,plain,
$false,
inference(sat_refutation,[status(thm)],[f360,f362,f364,f366,f368,f456,f1226,f1230,f1239,f1241,f1295,f1316,f1516,f1519,f1521]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP628+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n010.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Sun Sep 20 20:21:17 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.40 % Drodi V4.1.1
% 0.15/5.47 % Refutation found
% 0.15/5.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/5.50 % Elapsed time: 0.113390 seconds
% 0.15/5.50 % CPU time: 0.606097 seconds
% 0.15/5.50 % Total memory used: 119.595 MB
% 0.15/5.50 % Net memory used: 119.148 MB
%------------------------------------------------------------------------------