%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP642+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:56 PM UTC 2026
% Result : Theorem 28.83s 14.45s
% Output : CNFRefutation 29.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 58 ( 21 unt; 6 def)
% Number of atoms : 148 ( 21 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 144 ( 54 ~; 47 |; 29 &)
% ( 8 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 7 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 34 ( 29 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
? [A] : v1_xboole_0(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( v1_xboole_0(A)
<=> A = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36509,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) )
=> r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36510,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) )
=> k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36511,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) )
=> k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) ),
inference(negated_conjecture,[status(cth)],[f36510]) ).
fof(f36591,plain,
v1_xboole_0(sK20_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f25]) ).
fof(f36592,plain,
v1_xboole_0(sK20_skl),
inference(cnf_transformation,[status(thm)],[f36591]) ).
fof(f36601,plain,
! [A] :
( ( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(NNF_transformation,[status(thm)],[f29]) ).
fof(f36602,plain,
( ! [A] :
( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(miniscoping,[status(thm)],[f36601]) ).
fof(f36603,plain,
( ! [A] :
( r2_hidden(sK22_skl(A),A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f36602]) ).
fof(f36604,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| X0 != k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f36603]) ).
fof(f36633,plain,
! [A] :
( ( A != k1_xboole_0
| v1_xboole_0(A) )
& ( A = k1_xboole_0
| ~ v1_xboole_0(A) ) ),
inference(NNF_transformation,[status(thm)],[f33]) ).
fof(f36634,plain,
( ! [A] :
( A != k1_xboole_0
| v1_xboole_0(A) )
& ! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ) ),
inference(miniscoping,[status(thm)],[f36633]) ).
fof(f36635,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f36634]) ).
fof(f162772,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)],[f36509]) ).
fof(f162773,plain,
! [X0,X1] :
( r2_hidden(k2_group_1(X0),k1_funct_1(k1_latsubgr(X0),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(cnf_transformation,[status(thm)],[f162772]) ).
fof(f162774,plain,
? [A] :
( ? [B] :
( k1_funct_1(k1_latsubgr(A),B) = k1_xboole_0
& 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)],[f36511]) ).
fof(f162775,plain,
( k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl) = k1_xboole_0
& m1_group_2(sK12738_skl,sK12737_skl)
& v1_group_1(sK12738_skl)
& l1_group_1(sK12737_skl)
& v4_group_1(sK12737_skl)
& v3_group_1(sK12737_skl)
& ~ v3_struct_0(sK12737_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12737_skl,sK12738_skl]),skolemize(A,sK12737_skl),skolemize(B,sK12738_skl)],[f162774]) ).
fof(f162776,plain,
~ v3_struct_0(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162775]) ).
fof(f162777,plain,
v3_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162775]) ).
fof(f162778,plain,
v4_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162775]) ).
fof(f162779,plain,
l1_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162775]) ).
fof(f162780,plain,
v1_group_1(sK12738_skl),
inference(cnf_transformation,[status(thm)],[f162775]) ).
fof(f162781,plain,
m1_group_2(sK12738_skl,sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162775]) ).
fof(f162782,plain,
k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl) = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f162775]) ).
fof(f193348,plain,
! [X0] : ~ r2_hidden(X0,k1_xboole_0),
inference(destructive_equality_resolution,[status(thm)],[f36604]) ).
fof(f202857,definition,
( sQ3074_spl
<=> v3_struct_0(sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3074_spl])],[split_symbol_definition]) ).
fof(f202858,plain,
( ~ sQ3074_spl
| v3_struct_0(sK12737_skl) ),
inference(component_clause,[status(thm)],[f202857]) ).
fof(f202860,definition,
( sQ3075_spl
<=> v3_group_1(sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3075_spl])],[split_symbol_definition]) ).
fof(f202862,plain,
( sQ3075_spl
| ~ v3_group_1(sK12737_skl) ),
inference(component_clause,[status(thm)],[f202860]) ).
fof(f202863,definition,
( sQ3076_spl
<=> v4_group_1(sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3076_spl])],[split_symbol_definition]) ).
fof(f202865,plain,
( sQ3076_spl
| ~ v4_group_1(sK12737_skl) ),
inference(component_clause,[status(thm)],[f202863]) ).
fof(f202866,definition,
( sQ3077_spl
<=> l1_group_1(sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3077_spl])],[split_symbol_definition]) ).
fof(f202868,plain,
( sQ3077_spl
| ~ l1_group_1(sK12737_skl) ),
inference(component_clause,[status(thm)],[f202866]) ).
fof(f202873,plain,
( sQ3077_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f202868,f162779]) ).
fof(f202874,plain,
sQ3077_spl,
inference(contradiction_clause,[status(thm)],[f202873]) ).
fof(f202875,plain,
( sQ3076_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f202865,f162778]) ).
fof(f202876,plain,
sQ3076_spl,
inference(contradiction_clause,[status(thm)],[f202875]) ).
fof(f202877,plain,
( sQ3075_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f202862,f162777]) ).
fof(f202878,plain,
sQ3075_spl,
inference(contradiction_clause,[status(thm)],[f202877]) ).
fof(f202879,plain,
( ~ sQ3074_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f202858,f162776]) ).
fof(f202880,plain,
~ sQ3074_spl,
inference(contradiction_clause,[status(thm)],[f202879]) ).
fof(f202978,definition,
( sQ3089_spl
<=> v1_group_1(sK12738_skl) ),
introduced(definition,[new_symbols(definition,[sQ3089_spl])],[split_symbol_definition]) ).
fof(f202980,plain,
( sQ3089_spl
| ~ v1_group_1(sK12738_skl) ),
inference(component_clause,[status(thm)],[f202978]) ).
fof(f202988,plain,
( sQ3089_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f202980,f162780]) ).
fof(f202989,plain,
sQ3089_spl,
inference(contradiction_clause,[status(thm)],[f202988]) ).
fof(f203149,plain,
sK20_skl = k1_xboole_0,
inference(resolution,[status(thm)],[f36635,f36592]) ).
fof(f203154,plain,
k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl) = sK20_skl,
inference(backward_demodulation,[status(thm)],[f203149,f162782]) ).
fof(f203159,plain,
! [X0] : ~ r2_hidden(X0,sK20_skl),
inference(backward_demodulation,[status(thm)],[f203149,f193348]) ).
fof(f203162,plain,
( r2_hidden(k2_group_1(sK12737_skl),k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl))
| ~ v1_group_1(sK12738_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(resolution,[status(thm)],[f162773,f162781]) ).
fof(f203171,definition,
( sQ3111_spl
<=> r2_hidden(k2_group_1(sK12737_skl),k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3111_spl])],[split_symbol_definition]) ).
fof(f203172,plain,
( ~ sQ3111_spl
| r2_hidden(k2_group_1(sK12737_skl),k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl)) ),
inference(component_clause,[status(thm)],[f203171]) ).
fof(f203174,plain,
( sQ3111_spl
| ~ sQ3089_spl
| ~ sQ3077_spl
| ~ sQ3076_spl
| ~ sQ3075_spl
| sQ3074_spl ),
inference(split_clause,[status(thm)],[f203162,f202857,f202860,f202863,f202866,f202978,f203171]) ).
fof(f203561,plain,
( ~ sQ3111_spl
| r2_hidden(k2_group_1(sK12737_skl),sK20_skl) ),
inference(forward_demodulation,[status(thm)],[f203154,f203172]) ).
fof(f203562,plain,
( ~ sQ3111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f203561,f203159]) ).
fof(f203563,plain,
~ sQ3111_spl,
inference(contradiction_clause,[status(thm)],[f203562]) ).
fof(f203564,plain,
$false,
inference(sat_refutation,[status(thm)],[f202874,f202876,f202878,f202880,f202989,f203174,f203563]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP642+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.44 % Computer : n013.cluster.edu
% 0.14/0.44 % Model : x86_64 x86_64
% 0.14/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.44 % Memory : 8046.5625MB
% 0.14/0.44 % OS : Linux 6.8.0-71-generic
% 0.14/0.44 % CPULimit : 300
% 0.14/0.44 % WCLimit : 300
% 0.14/0.44 % DateTime : Sun Sep 20 20:24:56 UTC 2026
% 0.14/0.44 % CPUTime :
% 11.79/12.08 % Drodi V4.1.1
% 28.83/14.45 % Refutation found
% 28.83/14.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.83/14.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 23.25/16.08 % Elapsed time: 15.151688 seconds
% 23.25/16.08 % CPU time: 29.529914 seconds
% 23.25/16.08 % Total memory used: 8.570 GB
% 23.25/16.08 % Net memory used: 8.524 GB
%------------------------------------------------------------------------------