%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP648+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:59 PM UTC 2026
% Result : Theorem 41.31s 14.33s
% Output : CNFRefutation 11.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 6
% Syntax : Number of formulae : 101 ( 17 unt; 0 def)
% Number of atoms : 595 ( 26 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 851 ( 357 ~; 390 |; 68 &)
% ( 8 <=>; 27 =>; 0 <=; 1 <~>)
% Maximal formula depth : 19 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 117 ( 107 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21855,axiom,
! [A] :
( ( l1_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
=> ( m1_group_2(B,A)
<=> ( u1_group_1(B) = k1_realset1(u1_group_1(A),u1_struct_0(B))
& r1_tarski(u1_struct_0(B),u1_struct_0(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21877,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> ! [C] :
( m1_group_2(C,A)
=> ( r1_tarski(u1_struct_0(B),u1_struct_0(C))
=> m1_group_2(B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22007,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f27005,axiom,
! [A,B] :
( ( m1_group_2(B,A)
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [C] :
( m1_group_6(C,A,B)
<=> m1_group_2(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36521,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> ! [C] :
( m1_group_2(C,A)
=> ! [D] :
( m1_subset_1(D,u1_struct_0(k11_group_4(A)))
=> ! [E] :
( m1_subset_1(E,u1_struct_0(k11_group_4(A)))
=> ( ( E = C
& D = B )
=> ( r3_lattices(k11_group_4(A),D,E)
<=> r1_tarski(u1_struct_0(B),u1_struct_0(C)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36522,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> ! [C] :
( m1_group_2(C,A)
=> ! [D] :
( m1_subset_1(D,u1_struct_0(k11_group_4(A)))
=> ! [E] :
( m1_subset_1(E,u1_struct_0(k11_group_4(A)))
=> ( ( E = C
& D = B )
=> ( r3_lattices(k11_group_4(A),D,E)
<=> m1_group_6(B,A,C) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36523,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)
=> ! [C] :
( m1_group_2(C,A)
=> ! [D] :
( m1_subset_1(D,u1_struct_0(k11_group_4(A)))
=> ! [E] :
( m1_subset_1(E,u1_struct_0(k11_group_4(A)))
=> ( ( E = C
& D = B )
=> ( r3_lattices(k11_group_4(A),D,E)
<=> m1_group_6(B,A,C) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f36522]) ).
fof(f108044,plain,
! [A] :
( ! [B] :
( ( m1_group_2(B,A)
<=> ( u1_group_1(B) = k1_realset1(u1_group_1(A),u1_struct_0(B))
& r1_tarski(u1_struct_0(B),u1_struct_0(A)) ) )
| ~ l1_group_1(B)
| ~ v3_group_1(B)
| v3_struct_0(B) )
| ~ l1_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21855]) ).
fof(f108045,plain,
! [A] :
( ! [B] :
( ( ( u1_group_1(B) != k1_realset1(u1_group_1(A),u1_struct_0(B))
| ~ r1_tarski(u1_struct_0(B),u1_struct_0(A))
| m1_group_2(B,A) )
& ( ( u1_group_1(B) = k1_realset1(u1_group_1(A),u1_struct_0(B))
& r1_tarski(u1_struct_0(B),u1_struct_0(A)) )
| ~ m1_group_2(B,A) ) )
| ~ l1_group_1(B)
| ~ v3_group_1(B)
| v3_struct_0(B) )
| ~ l1_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f108044]) ).
fof(f108046,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f108045]) ).
fof(f108092,plain,
! [A] :
( ! [B] :
( ! [C] :
( m1_group_2(B,C)
| ~ r1_tarski(u1_struct_0(B),u1_struct_0(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)],[f21877]) ).
fof(f108093,plain,
! [X0,X1,X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(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)],[f108092]) ).
fof(f108451,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)],[f22007]) ).
fof(f108452,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)],[f108451]) ).
fof(f108453,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)],[f108451]) ).
fof(f108454,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)],[f108451]) ).
fof(f126022,plain,
! [A,B] :
( ! [C] :
( m1_group_6(C,A,B)
<=> m1_group_2(C,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)],[f27005]) ).
fof(f126023,plain,
! [A,B] :
( ! [C] :
( ( ~ m1_group_2(C,B)
| m1_group_6(C,A,B) )
& ( m1_group_2(C,B)
| ~ m1_group_6(C,A,B) ) )
| ~ m1_group_2(B,A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f126022]) ).
fof(f126024,plain,
! [A,B] :
( ( ! [C] :
( ~ m1_group_2(C,B)
| m1_group_6(C,A,B) )
& ! [C] :
( m1_group_2(C,B)
| ~ m1_group_6(C,A,B) ) )
| ~ m1_group_2(B,A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f126023]) ).
fof(f126025,plain,
! [X0,X1,X2] :
( m1_group_2(X2,X1)
| ~ m1_group_6(X2,X0,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)],[f126024]) ).
fof(f126026,plain,
! [X0,X1,X2] :
( ~ m1_group_2(X2,X1)
| m1_group_6(X2,X0,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)],[f126024]) ).
fof(f162811,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( r3_lattices(k11_group_4(A),D,E)
<=> r1_tarski(u1_struct_0(B),u1_struct_0(C)) )
| E != C
| D != B
| ~ m1_subset_1(E,u1_struct_0(k11_group_4(A))) )
| ~ m1_subset_1(D,u1_struct_0(k11_group_4(A))) )
| ~ 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)],[f36521]) ).
fof(f162812,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( ( ~ r1_tarski(u1_struct_0(B),u1_struct_0(C))
| r3_lattices(k11_group_4(A),D,E) )
& ( r1_tarski(u1_struct_0(B),u1_struct_0(C))
| ~ r3_lattices(k11_group_4(A),D,E) ) )
| E != C
| D != B
| ~ m1_subset_1(E,u1_struct_0(k11_group_4(A))) )
| ~ m1_subset_1(D,u1_struct_0(k11_group_4(A))) )
| ~ 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(NNF_transformation,[status(thm)],[f162811]) ).
fof(f162813,plain,
! [X0,X1,X2,X3,X4] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ r3_lattices(k11_group_4(X0),X3,X4)
| X4 != X2
| X3 != X1
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(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)],[f162812]) ).
fof(f162814,plain,
! [X0,X1,X2,X3,X4] :
( ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| r3_lattices(k11_group_4(X0),X3,X4)
| X4 != X2
| X3 != X1
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(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)],[f162812]) ).
fof(f162815,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ( r3_lattices(k11_group_4(A),D,E)
<~> m1_group_6(B,A,C) )
& E = C
& D = B
& m1_subset_1(E,u1_struct_0(k11_group_4(A))) )
& m1_subset_1(D,u1_struct_0(k11_group_4(A))) )
& 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)],[f36523]) ).
fof(f162816,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ( ~ m1_group_6(B,A,C)
| ~ r3_lattices(k11_group_4(A),D,E) )
& ( m1_group_6(B,A,C)
| r3_lattices(k11_group_4(A),D,E) )
& E = C
& D = B
& m1_subset_1(E,u1_struct_0(k11_group_4(A))) )
& m1_subset_1(D,u1_struct_0(k11_group_4(A))) )
& 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(NNF_transformation,[status(thm)],[f162815]) ).
fof(f162817,plain,
( ( ~ m1_group_6(sK12738_skl,sK12737_skl,sK12739_skl)
| ~ r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) )
& ( m1_group_6(sK12738_skl,sK12737_skl,sK12739_skl)
| r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) )
& sK12741_skl = sK12739_skl
& sK12740_skl = sK12738_skl
& m1_subset_1(sK12741_skl,u1_struct_0(k11_group_4(sK12737_skl)))
& m1_subset_1(sK12740_skl,u1_struct_0(k11_group_4(sK12737_skl)))
& m1_group_2(sK12739_skl,sK12737_skl)
& m1_group_2(sK12738_skl,sK12737_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,sK12739_skl,sK12740_skl,sK12741_skl]),skolemize(A,sK12737_skl),skolemize(B,sK12738_skl),skolemize(C,sK12739_skl),skolemize(D,sK12740_skl),skolemize(E,sK12741_skl)],[f162816]) ).
fof(f162818,plain,
~ v3_struct_0(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162819,plain,
v3_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162820,plain,
v4_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162821,plain,
l1_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162822,plain,
m1_group_2(sK12738_skl,sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162823,plain,
m1_group_2(sK12739_skl,sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162824,plain,
m1_subset_1(sK12740_skl,u1_struct_0(k11_group_4(sK12737_skl))),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162825,plain,
m1_subset_1(sK12741_skl,u1_struct_0(k11_group_4(sK12737_skl))),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162826,plain,
sK12740_skl = sK12738_skl,
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162827,plain,
sK12741_skl = sK12739_skl,
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162828,plain,
( m1_group_6(sK12738_skl,sK12737_skl,sK12739_skl)
| r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) ),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f162829,plain,
( ~ m1_group_6(sK12738_skl,sK12737_skl,sK12739_skl)
| ~ r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) ),
inference(cnf_transformation,[status(thm)],[f162817]) ).
fof(f190075,plain,
! [X0,X1,X2] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ r3_lattices(k11_group_4(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(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(destructive_equality_resolution,[status(thm)],[f162813]) ).
fof(f190076,plain,
! [X0,X1,X2] :
( ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| r3_lattices(k11_group_4(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(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(destructive_equality_resolution,[status(thm)],[f162814]) ).
fof(f190986,plain,
m1_group_2(sK12740_skl,sK12737_skl),
inference(backward_demodulation,[status(thm)],[f162826,f162822]) ).
fof(f190987,plain,
m1_group_2(sK12741_skl,sK12737_skl),
inference(forward_demodulation,[status(thm)],[f162827,f162823]) ).
fof(f190998,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f108046,f108452]) ).
fof(f191006,plain,
( m1_group_6(sK12740_skl,sK12737_skl,sK12739_skl)
| r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) ),
inference(forward_demodulation,[status(thm)],[f162826,f162828]) ).
fof(f191007,plain,
( m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl)
| r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) ),
inference(forward_demodulation,[status(thm)],[f162827,f191006]) ).
fof(f191008,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f190998,f108453]) ).
fof(f191010,plain,
( v3_group_1(sK12741_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(resolution,[status(thm)],[f108453,f190987]) ).
fof(f191013,plain,
( v3_group_1(sK12741_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191010,f162818]) ).
fof(f191016,plain,
( v3_group_1(sK12741_skl)
| ~ l1_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191013,f162819]) ).
fof(f191017,plain,
v3_group_1(sK12741_skl),
inference(resolution,[status(thm)],[f191016,f162821]) ).
fof(f191019,plain,
( l1_group_1(sK12741_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(resolution,[status(thm)],[f108454,f190987]) ).
fof(f191022,plain,
( l1_group_1(sK12741_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191019,f162818]) ).
fof(f191036,plain,
( l1_group_1(sK12741_skl)
| ~ l1_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191022,f162819]) ).
fof(f191037,plain,
l1_group_1(sK12741_skl),
inference(resolution,[status(thm)],[f191036,f162821]) ).
fof(f191041,plain,
( ~ m1_group_6(sK12740_skl,sK12737_skl,sK12739_skl)
| ~ r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) ),
inference(forward_demodulation,[status(thm)],[f162826,f162829]) ).
fof(f191042,plain,
( ~ m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl)
| ~ r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) ),
inference(forward_demodulation,[status(thm)],[f162827,f191041]) ).
fof(f191089,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f191008,f108454]) ).
fof(f191170,plain,
! [X0] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(sK12741_skl))
| ~ r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_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)],[f190075,f162825]) ).
fof(f191172,plain,
! [X0] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(sK12741_skl))
| ~ r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191170,f162818]) ).
fof(f191174,plain,
! [X0] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(sK12741_skl))
| ~ r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191172,f162819]) ).
fof(f191176,plain,
( r1_tarski(u1_struct_0(sK12740_skl),u1_struct_0(sK12741_skl))
| ~ r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(sK12740_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl) ),
inference(resolution,[status(thm)],[f191174,f162824]) ).
fof(f191178,plain,
( r1_tarski(u1_struct_0(sK12740_skl),u1_struct_0(sK12741_skl))
| ~ r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(sK12740_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191176,f162820]) ).
fof(f191179,plain,
( r1_tarski(u1_struct_0(sK12740_skl),u1_struct_0(sK12741_skl))
| ~ r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(sK12740_skl,sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191178,f162821]) ).
fof(f191180,plain,
( m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl)
| r1_tarski(u1_struct_0(sK12740_skl),u1_struct_0(sK12741_skl))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(sK12740_skl,sK12737_skl) ),
inference(resolution,[status(thm)],[f191179,f191007]) ).
fof(f191181,plain,
( m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl)
| r1_tarski(u1_struct_0(sK12740_skl),u1_struct_0(sK12741_skl))
| ~ m1_group_2(sK12741_skl,sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191180,f190986]) ).
fof(f191182,plain,
( m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl)
| r1_tarski(u1_struct_0(sK12740_skl),u1_struct_0(sK12741_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f191181,f190987]) ).
fof(f191183,plain,
! [X0] :
( m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,X0)
| ~ m1_group_2(sK12740_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl) ),
inference(resolution,[status(thm)],[f191182,f108093]) ).
fof(f191190,plain,
! [X0] :
( m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl)
| m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,X0)
| ~ m1_group_2(sK12740_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f191183,f126025]) ).
fof(f191193,plain,
! [X0] :
( ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl)
| m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,X0)
| ~ m1_group_2(sK12740_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f191190]) ).
fof(f191194,plain,
! [X0] :
( ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,X0)
| ~ m1_group_2(sK12740_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f191193,f162818]) ).
fof(f191196,plain,
! [X0] :
( ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,X0)
| ~ m1_group_2(sK12740_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f191194,f162819]) ).
fof(f191198,plain,
( ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_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)],[f191196,f190986]) ).
fof(f191202,plain,
( m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f191198]) ).
fof(f191203,plain,
( m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191202,f162818]) ).
fof(f191206,plain,
( m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191203,f162819]) ).
fof(f191207,plain,
( m1_group_2(sK12740_skl,sK12741_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl) ),
inference(resolution,[status(thm)],[f191206,f190987]) ).
fof(f191208,plain,
( m1_group_2(sK12740_skl,sK12741_skl)
| ~ l1_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191207,f162820]) ).
fof(f191209,plain,
m1_group_2(sK12740_skl,sK12741_skl),
inference(forward_subsumption_resolution,[status(thm)],[f191208,f162821]) ).
fof(f191241,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK12741_skl))
| r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_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)],[f190076,f162825]) ).
fof(f191246,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK12741_skl))
| r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191241,f162818]) ).
fof(f191251,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK12741_skl))
| r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191246,f162819]) ).
fof(f191253,plain,
! [X0] :
( ~ m1_group_2(X0,sK12741_skl)
| ~ l1_group_1(sK12741_skl)
| ~ v3_group_1(sK12741_skl)
| v3_struct_0(sK12741_skl)
| r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl) ),
inference(resolution,[status(thm)],[f191251,f191089]) ).
fof(f191255,plain,
! [X0] :
( ~ m1_group_2(X0,sK12741_skl)
| ~ l1_group_1(sK12741_skl)
| ~ v3_group_1(sK12741_skl)
| v3_struct_0(sK12741_skl)
| r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_skl)
| ~ l1_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191253,f162820]) ).
fof(f191290,plain,
! [X0] :
( ~ m1_group_2(X0,sK12741_skl)
| ~ l1_group_1(sK12741_skl)
| ~ v3_group_1(sK12741_skl)
| v3_struct_0(sK12741_skl)
| r3_lattices(k11_group_4(sK12737_skl),X0,sK12741_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK12737_skl)))
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(X0,sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191255,f162821]) ).
fof(f191292,plain,
( ~ m1_group_2(sK12740_skl,sK12741_skl)
| ~ l1_group_1(sK12741_skl)
| ~ v3_group_1(sK12741_skl)
| v3_struct_0(sK12741_skl)
| r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ m1_group_2(sK12740_skl,sK12737_skl) ),
inference(resolution,[status(thm)],[f191290,f162824]) ).
fof(f191294,plain,
( ~ m1_group_2(sK12740_skl,sK12741_skl)
| ~ l1_group_1(sK12741_skl)
| ~ v3_group_1(sK12741_skl)
| v3_struct_0(sK12741_skl)
| r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191292,f190986]) ).
fof(f191323,plain,
( ~ m1_group_2(sK12740_skl,sK12741_skl)
| ~ l1_group_1(sK12741_skl)
| ~ v3_group_1(sK12741_skl)
| v3_struct_0(sK12741_skl)
| r3_lattices(k11_group_4(sK12737_skl),sK12740_skl,sK12741_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191294,f190987]) ).
fof(f191325,plain,
( ~ m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl)
| ~ m1_group_2(sK12740_skl,sK12741_skl)
| ~ l1_group_1(sK12741_skl)
| ~ v3_group_1(sK12741_skl)
| v3_struct_0(sK12741_skl) ),
inference(resolution,[status(thm)],[f191323,f191042]) ).
fof(f191326,plain,
( ~ m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl)
| ~ m1_group_2(sK12740_skl,sK12741_skl)
| ~ l1_group_1(sK12741_skl)
| v3_struct_0(sK12741_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191325,f191017]) ).
fof(f191327,plain,
( ~ m1_group_6(sK12740_skl,sK12737_skl,sK12741_skl)
| ~ m1_group_2(sK12740_skl,sK12741_skl)
| v3_struct_0(sK12741_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191326,f191037]) ).
fof(f191328,plain,
( ~ m1_group_2(sK12740_skl,sK12741_skl)
| ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl)
| ~ m1_group_2(sK12740_skl,sK12741_skl)
| v3_struct_0(sK12741_skl) ),
inference(resolution,[status(thm)],[f191327,f126026]) ).
fof(f191329,plain,
( ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl)
| ~ m1_group_2(sK12740_skl,sK12741_skl)
| v3_struct_0(sK12741_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f191328]) ).
fof(f191330,plain,
( ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl)
| ~ m1_group_2(sK12740_skl,sK12741_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191329,f108452]) ).
fof(f191331,plain,
( ~ m1_group_2(sK12741_skl,sK12737_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191330,f191209]) ).
fof(f191332,plain,
( ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(resolution,[status(thm)],[f191331,f190987]) ).
fof(f191333,plain,
( ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191332,f162818]) ).
fof(f191334,plain,
( ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f191333,f162819]) ).
fof(f191335,plain,
~ v4_group_1(sK12737_skl),
inference(resolution,[status(thm)],[f191334,f162821]) ).
fof(f191336,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f191335,f162820]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP648+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n019.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 20 20:26:40 UTC 2026
% 0.15/0.43 % CPUTime :
% 9.96/10.21 % Drodi V4.1.1
% 41.31/14.33 % Refutation found
% 41.31/14.33 % SZS status Theorem for theBenchmark: Theorem is valid
% 41.31/14.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.16/15.24 % Elapsed time: 14.674215 seconds
% 11.16/15.24 % CPU time: 43.135406 seconds
% 11.16/15.24 % Total memory used: 11.539 GB
% 11.16/15.24 % Net memory used: 11.453 GB
%------------------------------------------------------------------------------