%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP645+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 0.08s 0.41s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 25
% Syntax : Number of formulae : 118 ( 25 unt; 17 def)
% Number of atoms : 448 ( 42 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 554 ( 224 ~; 234 |; 63 &)
% ( 19 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 18 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-3 aty)
% Number of variables : 100 ( 94 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(k1_latsubgr(A),k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
file('/export/starexec/sandbox/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] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(k1_latsubgr(A),k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f11,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_1(B) )
=> ( B = k1_latsubgr(A)
<=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(B,C) = u1_struct_0(C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_1(k1_latsubgr(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B,C] :
( ( m1_group_2(C,A)
& m1_group_2(B,A)
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( m1_group_2(k9_group_2(A,B,C),A)
& v1_group_1(k9_group_2(A,B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B] :
? [C] :
( v1_funct_2(C,A,B)
& v1_funct_1(C)
& v1_relat_1(C)
& m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,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_group_2(C,A)
& v1_group_1(C) )
=> u1_struct_0(k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,plain,
? [A] :
( ? [B] :
( ? [C] :
( k1_funct_1(k1_latsubgr(A),k9_group_2(A,B,C)) != k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C))
& m1_group_2(C,A)
& v1_group_1(C) )
& 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)],[f2]) ).
fof(f65,plain,
( k1_funct_1(k1_latsubgr(sK0_skl),k9_group_2(sK0_skl,sK1_skl,sK2_skl)) != k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl),k1_funct_1(k1_latsubgr(sK0_skl),sK2_skl))
& m1_group_2(sK2_skl,sK0_skl)
& v1_group_1(sK2_skl)
& m1_group_2(sK1_skl,sK0_skl)
& v1_group_1(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)],[f64]) ).
fof(f66,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
v3_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f68,plain,
v4_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f69,plain,
l1_group_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f70,plain,
v1_group_1(sK1_skl),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f71,plain,
m1_group_2(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f72,plain,
v1_group_1(sK2_skl),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f73,plain,
m1_group_2(sK2_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f74,plain,
k1_funct_1(k1_latsubgr(sK0_skl),k9_group_2(sK0_skl,sK1_skl,sK2_skl)) != k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl),k1_funct_1(k1_latsubgr(sK0_skl),sK2_skl)),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f98,plain,
! [A] :
( ! [B] :
( ( B = k1_latsubgr(A)
<=> ! [C] :
( k1_funct_1(B,C) = u1_struct_0(C)
| ~ m1_group_2(C,A)
| ~ v1_group_1(C) ) )
| ~ m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f99,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( k1_funct_1(B,C) != u1_struct_0(C)
& m1_group_2(C,A)
& v1_group_1(C) )
| B = k1_latsubgr(A) )
& ( ! [C] :
( k1_funct_1(B,C) = u1_struct_0(C)
| ~ m1_group_2(C,A)
| ~ v1_group_1(C) )
| B != k1_latsubgr(A) ) )
| ~ m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
! [A] :
( ! [B] :
( ( ( ( k1_funct_1(B,sK3_skl(B,A)) != u1_struct_0(sK3_skl(B,A))
& m1_group_2(sK3_skl(B,A),A)
& v1_group_1(sK3_skl(B,A)) )
| B = k1_latsubgr(A) )
& ( ! [C] :
( k1_funct_1(B,C) = u1_struct_0(C)
| ~ m1_group_2(C,A)
| ~ v1_group_1(C) )
| B != k1_latsubgr(A) ) )
| ~ m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( k1_funct_1(X1,X2) = u1_struct_0(X2)
| ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| X1 != k1_latsubgr(X0)
| ~ m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f108,plain,
! [A] :
( ( m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_1(k1_latsubgr(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f109,plain,
! [X0] :
( v1_funct_1(k1_latsubgr(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f110,plain,
! [X0] :
( v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(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)],[f108]) ).
fof(f111,plain,
! [X0] :
( m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(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)],[f108]) ).
fof(f115,plain,
! [A,B,C] :
( ( m1_group_2(k9_group_2(A,B,C),A)
& v1_group_1(k9_group_2(A,B,C)) )
| ~ m1_group_2(C,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)],[f21]) ).
fof(f116,plain,
! [X0,X1,X2] :
( v1_group_1(k9_group_2(X0,X1,X2))
| ~ m1_group_2(X2,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)],[f115]) ).
fof(f117,plain,
! [X0,X1,X2] :
( m1_group_2(k9_group_2(X0,X1,X2),X0)
| ~ m1_group_2(X2,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)],[f115]) ).
fof(f139,plain,
! [A] : m1_subset_1(sK8_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f34]) ).
fof(f140,plain,
! [X0] : m1_subset_1(sK8_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f147,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f156,plain,
! [A,B] :
( v1_funct_2(sK10_skl(B,A),A,B)
& v1_funct_1(sK10_skl(B,A))
& v1_relat_1(sK10_skl(B,A))
& m1_relset_1(sK10_skl(B,A),A,B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(C,sK10_skl(B,A))],[f43]) ).
fof(f159,plain,
! [X0,X1] : v1_funct_1(sK10_skl(X0,X1)),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f193,plain,
! [A] :
( ! [B] :
( ! [C] :
( u1_struct_0(k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C))
| ~ m1_group_2(C,A)
| ~ v1_group_1(C) )
| ~ 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)],[f55]) ).
fof(f194,plain,
! [X0,X1,X2] :
( u1_struct_0(k9_group_2(X0,X1,X2)) = k3_xboole_0(k1_funct_1(k1_latsubgr(X0),X1),k1_funct_1(k1_latsubgr(X0),X2))
| ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ~ 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)],[f193]) ).
fof(f216,plain,
! [X0,X1] :
( k1_funct_1(k1_latsubgr(X0),X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(k1_latsubgr(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f101]) ).
fof(f242,definition,
( sQ4_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f243,plain,
( ~ sQ4_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f245,definition,
( sQ5_spl
<=> v3_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f247,plain,
( sQ5_spl
| ~ v3_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,definition,
( sQ6_spl
<=> l1_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( sQ6_spl
| ~ l1_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f248]) ).
fof(f252,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f250,f69]) ).
fof(f253,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f252]) ).
fof(f254,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f247,f67]) ).
fof(f255,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f254]) ).
fof(f256,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f243,f66]) ).
fof(f257,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f256]) ).
fof(f261,plain,
! [X0,X1] :
( v1_group_1(k9_group_2(sK0_skl,X0,X1))
| ~ m1_group_2(X1,sK0_skl)
| ~ m1_group_2(X0,sK0_skl)
| ~ l1_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f116,f68]) ).
fof(f262,definition,
! [X0,X1] :
( sQ7_spl
<=> ( v1_group_1(k9_group_2(sK0_skl,X0,X1))
| ~ m1_group_2(X1,sK0_skl)
| ~ m1_group_2(X0,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f263,plain,
! [X0,X1] :
( ~ sQ7_spl
| v1_group_1(k9_group_2(sK0_skl,X0,X1))
| ~ m1_group_2(X1,sK0_skl)
| ~ m1_group_2(X0,sK0_skl) ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f265,plain,
( sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f261,f242,f245,f248,f262]) ).
fof(f266,plain,
! [X0] :
( ~ sQ7_spl
| v1_group_1(k9_group_2(sK0_skl,X0,sK2_skl))
| ~ m1_group_2(X0,sK0_skl) ),
inference(resolution,[status(thm)],[f263,f73]) ).
fof(f269,plain,
( ~ sQ7_spl
| v1_group_1(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) ),
inference(resolution,[status(thm)],[f266,f71]) ).
fof(f270,plain,
! [X0,X1] :
( k1_funct_1(k1_latsubgr(X0),X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f109]) ).
fof(f271,plain,
! [X0,X1] :
( m1_group_2(k9_group_2(sK0_skl,X0,X1),sK0_skl)
| ~ m1_group_2(X1,sK0_skl)
| ~ m1_group_2(X0,sK0_skl)
| ~ l1_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f117,f68]) ).
fof(f272,definition,
! [X0,X1] :
( sQ8_spl
<=> ( m1_group_2(k9_group_2(sK0_skl,X0,X1),sK0_skl)
| ~ m1_group_2(X1,sK0_skl)
| ~ m1_group_2(X0,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f273,plain,
! [X0,X1] :
( ~ sQ8_spl
| m1_group_2(k9_group_2(sK0_skl,X0,X1),sK0_skl)
| ~ m1_group_2(X1,sK0_skl)
| ~ m1_group_2(X0,sK0_skl) ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f275,plain,
( sQ8_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f271,f242,f245,f248,f272]) ).
fof(f335,plain,
! [X0] :
( ~ sQ8_spl
| m1_group_2(k9_group_2(sK0_skl,X0,sK2_skl),sK0_skl)
| ~ m1_group_2(X0,sK0_skl) ),
inference(resolution,[status(thm)],[f273,f73]) ).
fof(f338,plain,
( ~ sQ8_spl
| m1_group_2(k9_group_2(sK0_skl,sK1_skl,sK2_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f335,f71]) ).
fof(f339,plain,
! [X0,X1] :
( u1_struct_0(k9_group_2(sK0_skl,X0,X1)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),X0),k1_funct_1(k1_latsubgr(sK0_skl),X1))
| ~ m1_group_2(X1,sK0_skl)
| ~ v1_group_1(X1)
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0)
| ~ l1_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f194,f68]) ).
fof(f340,definition,
! [X0,X1] :
( sQ17_spl
<=> ( u1_struct_0(k9_group_2(sK0_skl,X0,X1)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),X0),k1_funct_1(k1_latsubgr(sK0_skl),X1))
| ~ m1_group_2(X1,sK0_skl)
| ~ v1_group_1(X1)
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f341,plain,
! [X0,X1] :
( ~ sQ17_spl
| u1_struct_0(k9_group_2(sK0_skl,X0,X1)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),X0),k1_funct_1(k1_latsubgr(sK0_skl),X1))
| ~ m1_group_2(X1,sK0_skl)
| ~ v1_group_1(X1)
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0) ),
inference(component_clause,[status(thm)],[f340]) ).
fof(f343,plain,
( sQ17_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f339,f242,f245,f248,f340]) ).
fof(f389,plain,
! [X0] :
( ~ sQ17_spl
| u1_struct_0(k9_group_2(sK0_skl,X0,sK2_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),X0),k1_funct_1(k1_latsubgr(sK0_skl),sK2_skl))
| ~ v1_group_1(sK2_skl)
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0) ),
inference(resolution,[status(thm)],[f341,f73]) ).
fof(f394,definition,
( sQ20_spl
<=> v1_group_1(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f396,plain,
( sQ20_spl
| ~ v1_group_1(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f394]) ).
fof(f412,definition,
! [X0] :
( sQ25_spl
<=> ( u1_struct_0(k9_group_2(sK0_skl,X0,sK2_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),X0),k1_funct_1(k1_latsubgr(sK0_skl),sK2_skl))
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f413,plain,
! [X0] :
( ~ sQ25_spl
| u1_struct_0(k9_group_2(sK0_skl,X0,sK2_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),X0),k1_funct_1(k1_latsubgr(sK0_skl),sK2_skl))
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0) ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,definition,
( sQ26_spl
<=> v1_group_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( sQ26_spl
| ~ v1_group_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f418,plain,
( ~ sQ17_spl
| ~ sQ26_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f389,f412,f415,f340]) ).
fof(f422,definition,
( sQ28_spl
<=> v1_group_1(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f424,plain,
( sQ28_spl
| ~ v1_group_1(sK1_skl) ),
inference(component_clause,[status(thm)],[f422]) ).
fof(f497,definition,
( sQ45_spl
<=> v1_funct_1(sK10_skl(k1_zfmisc_1(u1_struct_0(sK0_skl)),k1_group_3(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f499,plain,
( sQ45_spl
| ~ v1_funct_1(sK10_skl(k1_zfmisc_1(u1_struct_0(sK0_skl)),k1_group_3(sK0_skl))) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f515,plain,
( ~ sQ25_spl
| u1_struct_0(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl),k1_funct_1(k1_latsubgr(sK0_skl),sK2_skl))
| ~ v1_group_1(sK1_skl) ),
inference(resolution,[status(thm)],[f413,f71]) ).
fof(f536,definition,
( sQ54_spl
<=> u1_struct_0(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl),k1_funct_1(k1_latsubgr(sK0_skl),sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f537,plain,
( ~ sQ54_spl
| u1_struct_0(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl),k1_funct_1(k1_latsubgr(sK0_skl),sK2_skl)) ),
inference(component_clause,[status(thm)],[f536]) ).
fof(f539,plain,
( ~ sQ25_spl
| sQ54_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f515,f422,f536,f412]) ).
fof(f540,plain,
( sQ20_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f396,f269]) ).
fof(f541,plain,
( sQ20_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f540]) ).
fof(f548,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f417,f72]) ).
fof(f549,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f548]) ).
fof(f550,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f424,f70]) ).
fof(f551,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f550]) ).
fof(f626,plain,
( ~ sQ54_spl
| k1_funct_1(k1_latsubgr(sK0_skl),k9_group_2(sK0_skl,sK1_skl,sK2_skl)) != u1_struct_0(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) ),
inference(backward_demodulation,[status(thm)],[f537,f74]) ).
fof(f680,definition,
! [X0] :
( sQ70_spl
<=> ~ m1_subset_1(X0,sK8_skl(k1_zfmisc_1(k1_xboole_0))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f681,plain,
! [X0] :
( ~ sQ70_spl
| ~ m1_subset_1(X0,sK8_skl(k1_zfmisc_1(k1_xboole_0))) ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f687,plain,
! [X0,X1] :
( k1_funct_1(k1_latsubgr(X0),X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f270,f110]) ).
fof(f715,definition,
( sQ78_spl
<=> v4_group_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f717,plain,
( sQ78_spl
| ~ v4_group_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f715]) ).
fof(f719,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f68]) ).
fof(f720,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f719]) ).
fof(f752,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f499,f159]) ).
fof(f753,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f752]) ).
fof(f768,definition,
( sQ85_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( ~ sQ85_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f768]) ).
fof(f776,plain,
( ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f769,f147]) ).
fof(f777,plain,
~ sQ85_spl,
inference(contradiction_clause,[status(thm)],[f776]) ).
fof(f794,plain,
! [X0,X1] :
( k1_funct_1(k1_latsubgr(X0),X1) = u1_struct_0(X1)
| ~ 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(forward_subsumption_resolution,[status(thm)],[f687,f111]) ).
fof(f795,plain,
! [X0] :
( k1_funct_1(k1_latsubgr(sK0_skl),X0) = u1_struct_0(X0)
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0)
| ~ l1_group_1(sK0_skl)
| ~ v3_group_1(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f794,f68]) ).
fof(f796,definition,
! [X0] :
( sQ88_spl
<=> ( k1_funct_1(k1_latsubgr(sK0_skl),X0) = u1_struct_0(X0)
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f797,plain,
! [X0] :
( ~ sQ88_spl
| k1_funct_1(k1_latsubgr(sK0_skl),X0) = u1_struct_0(X0)
| ~ m1_group_2(X0,sK0_skl)
| ~ v1_group_1(X0) ),
inference(component_clause,[status(thm)],[f796]) ).
fof(f799,plain,
( sQ88_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f795,f242,f245,f248,f796]) ).
fof(f800,plain,
( ~ sQ70_spl
| $false ),
inference(resolution,[status(thm)],[f681,f140]) ).
fof(f802,plain,
~ sQ70_spl,
inference(contradiction_clause,[status(thm)],[f800]) ).
fof(f993,plain,
( ~ sQ8_spl
| ~ sQ88_spl
| k1_funct_1(k1_latsubgr(sK0_skl),k9_group_2(sK0_skl,sK1_skl,sK2_skl)) = u1_struct_0(k9_group_2(sK0_skl,sK1_skl,sK2_skl))
| ~ v1_group_1(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) ),
inference(resolution,[status(thm)],[f797,f338]) ).
fof(f1018,definition,
( sQ120_spl
<=> k1_funct_1(k1_latsubgr(sK0_skl),k9_group_2(sK0_skl,sK1_skl,sK2_skl)) = u1_struct_0(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1019,plain,
( ~ sQ120_spl
| k1_funct_1(k1_latsubgr(sK0_skl),k9_group_2(sK0_skl,sK1_skl,sK2_skl)) = u1_struct_0(k9_group_2(sK0_skl,sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f1018]) ).
fof(f1021,plain,
( ~ sQ8_spl
| ~ sQ88_spl
| sQ120_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f993,f394,f1018,f796,f272]) ).
fof(f1038,plain,
( ~ sQ120_spl
| ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1019,f626]) ).
fof(f1039,plain,
( ~ sQ120_spl
| ~ sQ54_spl ),
inference(contradiction_clause,[status(thm)],[f1038]) ).
fof(f1040,plain,
$false,
inference(sat_refutation,[status(thm)],[f253,f255,f257,f265,f275,f343,f418,f539,f541,f549,f551,f720,f753,f777,f799,f802,f1021,f1039]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP645+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 20:26:33 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.41 % Refutation found
% 0.08/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.08/0.44 % Elapsed time: 0.069568 seconds
% 0.08/0.44 % CPU time: 0.245580 seconds
% 0.08/0.44 % Total memory used: 108.284 MB
% 0.08/0.44 % Net memory used: 108.091 MB
%------------------------------------------------------------------------------