%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP642+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 : n026.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 1.22s 1.63s
% Output : CNFRefutation 1.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of formulae : 45 ( 14 unt; 5 def)
% Number of atoms : 127 ( 13 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 131 ( 49 ~; 43 |; 27 &)
% ( 6 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 6 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 28 ( 24 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5658,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f5659,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f5660,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)],[f5659]) ).
fof(f5750,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(f5751,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)],[f5750]) ).
fof(f5752,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))],[f5751]) ).
fof(f5753,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| X0 != k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f5752]) ).
fof(f22086,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)],[f5658]) ).
fof(f22087,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)],[f22086]) ).
fof(f22088,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)],[f5660]) ).
fof(f22089,plain,
( k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl) = k1_xboole_0
& 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)],[f22088]) ).
fof(f22090,plain,
~ v3_struct_0(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22089]) ).
fof(f22091,plain,
v3_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22089]) ).
fof(f22092,plain,
v4_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22089]) ).
fof(f22093,plain,
l1_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22089]) ).
fof(f22094,plain,
v1_group_1(sK1496_skl),
inference(cnf_transformation,[status(thm)],[f22089]) ).
fof(f22095,plain,
m1_group_2(sK1496_skl,sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22089]) ).
fof(f22096,plain,
k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl) = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f22089]) ).
fof(f25839,plain,
! [X0] : ~ r2_hidden(X0,k1_xboole_0),
inference(destructive_equality_resolution,[status(thm)],[f5753]) ).
fof(f27198,definition,
( sQ621_spl
<=> v3_struct_0(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ621_spl])],[split_symbol_definition]) ).
fof(f27199,plain,
( ~ sQ621_spl
| v3_struct_0(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27198]) ).
fof(f27204,definition,
( sQ623_spl
<=> m1_group_2(sK1496_skl,sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ623_spl])],[split_symbol_definition]) ).
fof(f27206,plain,
( sQ623_spl
| ~ m1_group_2(sK1496_skl,sK1495_skl) ),
inference(component_clause,[status(thm)],[f27204]) ).
fof(f27209,definition,
( sQ624_spl
<=> v3_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition]) ).
fof(f27211,plain,
( sQ624_spl
| ~ v3_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27209]) ).
fof(f27214,plain,
( sQ623_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27206,f22095]) ).
fof(f27215,plain,
sQ623_spl,
inference(contradiction_clause,[status(thm)],[f27214]) ).
fof(f27216,plain,
( ~ sQ621_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27199,f22090]) ).
fof(f27217,plain,
~ sQ621_spl,
inference(contradiction_clause,[status(thm)],[f27216]) ).
fof(f27218,plain,
( sQ624_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27211,f22091]) ).
fof(f27219,plain,
sQ624_spl,
inference(contradiction_clause,[status(thm)],[f27218]) ).
fof(f27256,definition,
( sQ625_spl
<=> v4_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition]) ).
fof(f27258,plain,
( sQ625_spl
| ~ v4_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27256]) ).
fof(f27267,plain,
( sQ625_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27258,f22092]) ).
fof(f27268,plain,
sQ625_spl,
inference(contradiction_clause,[status(thm)],[f27267]) ).
fof(f27295,plain,
! [X0] :
( r2_hidden(k2_group_1(X0),k1_funct_1(k1_latsubgr(X0),sK1496_skl))
| ~ m1_group_2(sK1496_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f22087,f22094]) ).
fof(f27446,plain,
( r2_hidden(k2_group_1(sK1495_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))
| ~ m1_group_2(sK1496_skl,sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27295,f22093]) ).
fof(f27452,definition,
( sQ645_spl
<=> r2_hidden(k2_group_1(sK1495_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)) ),
introduced(definition,[new_symbols(definition,[sQ645_spl])],[split_symbol_definition]) ).
fof(f27453,plain,
( ~ sQ645_spl
| r2_hidden(k2_group_1(sK1495_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)) ),
inference(component_clause,[status(thm)],[f27452]) ).
fof(f27461,plain,
( sQ645_spl
| ~ sQ623_spl
| ~ sQ625_spl
| ~ sQ624_spl
| sQ621_spl ),
inference(split_clause,[status(thm)],[f27446,f27198,f27209,f27256,f27204,f27452]) ).
fof(f27463,plain,
( ~ sQ645_spl
| r2_hidden(k2_group_1(sK1495_skl),k1_xboole_0) ),
inference(forward_demodulation,[status(thm)],[f22096,f27453]) ).
fof(f27464,plain,
( ~ sQ645_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27463,f25839]) ).
fof(f27465,plain,
~ sQ645_spl,
inference(contradiction_clause,[status(thm)],[f27464]) ).
fof(f27466,plain,
$false,
inference(sat_refutation,[status(thm)],[f27215,f27217,f27219,f27268,f27461,f27465]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP642+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n026.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 20 20:27:54 UTC 2026
% 0.17/0.45 % CPUTime :
% 1.16/1.41 % Drodi V4.1.1
% 1.22/1.63 % Refutation found
% 1.22/1.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.22/1.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.25/1.91 % Elapsed time: 1.442848 seconds
% 1.25/1.91 % CPU time: 3.071368 seconds
% 1.25/1.91 % Total memory used: 987.388 MB
% 1.25/1.91 % Net memory used: 980.338 MB
%------------------------------------------------------------------------------