%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP648+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 : n001.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:58 PM UTC 2026
% Result : Theorem 1.23s 1.77s
% Output : CNFRefutation 1.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 101
% Syntax : Number of formulae : 402 ( 25 unt; 83 def)
% Number of atoms : 2679 ( 29 equ)
% Maximal formula atoms : 17 ( 6 avg)
% Number of connectives : 4071 (1794 ~;1999 |; 136 &)
% ( 91 <=>; 50 =>; 0 <=; 1 <~>)
% Maximal formula depth : 20 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 110 ( 108 usr; 84 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 439 ( 428 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [A,B] : r1_tarski(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
? [A] : ~ v1_xboole_0(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f558,axiom,
! [A,B] :
( ( ~ v1_xboole_0(B)
& ~ v1_xboole_0(A) )
=> ~ r1_subset_1(A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f561,axiom,
! [A,B] :
( ( ~ v1_xboole_0(B)
& ~ v1_xboole_0(A) )
=> ~ r2_subset_1(A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4339,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> v4_group_1(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4388,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(f4407,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> m1_group_2(A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4409,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_group_1(B)
& v4_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( l1_group_1(C)
& v4_group_1(C)
& v3_group_1(C)
& ~ v3_struct_0(C) )
=> ( ( m1_group_2(B,C)
& m1_group_2(A,B) )
=> m1_group_2(A,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4410,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(f4540,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(f5000,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( v15_lattices(k11_group_4(A))
& v14_lattices(k11_group_4(A))
& v13_lattices(k11_group_4(A))
& v10_lattices(k11_group_4(A))
& v9_lattices(k11_group_4(A))
& v8_lattices(k11_group_4(A))
& v7_lattices(k11_group_4(A))
& v6_lattices(k11_group_4(A))
& v5_lattices(k11_group_4(A))
& v4_lattices(k11_group_4(A))
& v3_lattices(k11_group_4(A))
& ~ v3_struct_0(k11_group_4(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5249,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)
& v1_group_3(C,A) )
=> ( m1_group_6(C,A,B)
=> ( m1_group_6(C,A,B)
& v1_group_3(C,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5251,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)
& v1_group_3(C,A) )
=> ( m1_group_6(k9_group_2(A,C,B),A,B)
& v1_group_3(k9_group_2(A,C,B),B)
& m1_group_6(k9_group_2(A,B,C),A,B)
& v1_group_3(k9_group_2(A,B,C),B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5348,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,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5350,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(f5669,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(k11_group_4(A)))
=> ! [C] :
( m1_group_2(C,A)
=> ( B = C
=> ( m1_group_2(C,A)
& v1_group_1(C) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5670,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(f5671,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(f5672,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)],[f5671]) ).
fof(f5748,plain,
! [A] : r1_tarski(A,A),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f5749,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[status(thm)],[f5748]) ).
fof(f5754,plain,
~ v1_xboole_0(sK21_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(A,sK21_skl)],[f26]) ).
fof(f5755,plain,
~ v1_xboole_0(sK21_skl),
inference(cnf_transformation,[status(thm)],[f5754]) ).
fof(f6860,plain,
! [A,B] :
( ~ r1_subset_1(A,A)
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f558]) ).
fof(f6861,plain,
! [A] :
( ~ r1_subset_1(A,A)
| ! [B] : v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(miniscoping,[status(thm)],[f6860]) ).
fof(f6862,plain,
! [X0,X1] :
( ~ r1_subset_1(X0,X0)
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f6861]) ).
fof(f6869,plain,
! [A,B] :
( ~ r2_subset_1(A,A)
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f561]) ).
fof(f6870,plain,
! [A] :
( ~ r2_subset_1(A,A)
| ! [B] : v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(miniscoping,[status(thm)],[f6869]) ).
fof(f6871,plain,
! [X0,X1] :
( ~ r2_subset_1(X0,X0)
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f6870]) ).
fof(f17662,plain,
! [A] :
( ! [B] :
( v4_group_1(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)],[f4339]) ).
fof(f17663,plain,
! [X0,X1] :
( v4_group_1(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)],[f17662]) ).
fof(f17803,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)],[f4388]) ).
fof(f17804,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)],[f17803]) ).
fof(f17805,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)],[f17804]) ).
fof(f17845,plain,
! [A] :
( m1_group_2(A,A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4407]) ).
fof(f17846,plain,
! [X0] :
( m1_group_2(X0,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f17845]) ).
fof(f17849,plain,
! [A] :
( ! [B] :
( ! [C] :
( m1_group_2(A,C)
| ~ m1_group_2(B,C)
| ~ m1_group_2(A,B)
| ~ l1_group_1(C)
| ~ v4_group_1(C)
| ~ v3_group_1(C)
| v3_struct_0(C) )
| ~ l1_group_1(B)
| ~ v4_group_1(B)
| ~ v3_group_1(B)
| v3_struct_0(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4409]) ).
fof(f17850,plain,
! [X0,X1,X2] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X1,X2)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f17849]) ).
fof(f17851,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)],[f4410]) ).
fof(f17852,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)],[f17851]) ).
fof(f18210,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)],[f4540]) ).
fof(f18211,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)],[f18210]) ).
fof(f18212,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)],[f18210]) ).
fof(f18213,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)],[f18210]) ).
fof(f19601,plain,
! [A] :
( ( v15_lattices(k11_group_4(A))
& v14_lattices(k11_group_4(A))
& v13_lattices(k11_group_4(A))
& v10_lattices(k11_group_4(A))
& v9_lattices(k11_group_4(A))
& v8_lattices(k11_group_4(A))
& v7_lattices(k11_group_4(A))
& v6_lattices(k11_group_4(A))
& v5_lattices(k11_group_4(A))
& v4_lattices(k11_group_4(A))
& v3_lattices(k11_group_4(A))
& ~ v3_struct_0(k11_group_4(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5000]) ).
fof(f19602,plain,
! [X0] :
( ~ v3_struct_0(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f19601]) ).
fof(f20476,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( m1_group_6(C,A,B)
& v1_group_3(C,B) )
| ~ m1_group_6(C,A,B)
| ~ m1_group_2(C,A)
| ~ v1_group_3(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)],[f5249]) ).
fof(f20477,plain,
! [X0,X1,X2] :
( v1_group_3(X2,X1)
| ~ m1_group_6(X2,X0,X1)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(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)],[f20476]) ).
fof(f20481,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( m1_group_6(k9_group_2(A,C,B),A,B)
& v1_group_3(k9_group_2(A,C,B),B)
& m1_group_6(k9_group_2(A,B,C),A,B)
& v1_group_3(k9_group_2(A,B,C),B) )
| ~ m1_group_2(C,A)
| ~ v1_group_3(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)],[f5251]) ).
fof(f20483,plain,
! [X0,X1,X2] :
( m1_group_6(k9_group_2(X0,X1,X2),X0,X1)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(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)],[f20481]) ).
fof(f20485,plain,
! [X0,X1,X2] :
( m1_group_6(k9_group_2(X0,X2,X1),X0,X1)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(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)],[f20481]) ).
fof(f20774,plain,
! [A,B] :
( ! [C] :
( m1_group_2(C,A)
| ~ 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(pre_NNF_transformation,[status(thm)],[f5348]) ).
fof(f20775,plain,
! [X0,X1,X2] :
( m1_group_2(X2,X0)
| ~ 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)],[f20774]) ).
fof(f20779,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)],[f5350]) ).
fof(f20780,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)],[f20779]) ).
fof(f20781,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)],[f20780]) ).
fof(f20782,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)],[f20781]) ).
fof(f20783,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)],[f20781]) ).
fof(f22122,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
| B != C
| ~ m1_group_2(C,A) )
| ~ m1_subset_1(B,u1_struct_0(k11_group_4(A))) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5669]) ).
fof(f22123,plain,
! [X0,X1,X2] :
( v1_group_1(X2)
| X1 != X2
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f22122]) ).
fof(f22125,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)],[f5670]) ).
fof(f22126,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)],[f22125]) ).
fof(f22127,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)],[f22126]) ).
fof(f22128,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)],[f22126]) ).
fof(f22129,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)],[f5672]) ).
fof(f22130,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)],[f22129]) ).
fof(f22131,plain,
( ( ~ m1_group_6(sK1496_skl,sK1495_skl,sK1497_skl)
| ~ r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1499_skl) )
& ( m1_group_6(sK1496_skl,sK1495_skl,sK1497_skl)
| r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1499_skl) )
& sK1499_skl = sK1497_skl
& sK1498_skl = sK1496_skl
& m1_subset_1(sK1499_skl,u1_struct_0(k11_group_4(sK1495_skl)))
& m1_subset_1(sK1498_skl,u1_struct_0(k11_group_4(sK1495_skl)))
& m1_group_2(sK1497_skl,sK1495_skl)
& m1_group_2(sK1496_skl,sK1495_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,sK1497_skl,sK1498_skl,sK1499_skl]),skolemize(A,sK1495_skl),skolemize(B,sK1496_skl),skolemize(C,sK1497_skl),skolemize(D,sK1498_skl),skolemize(E,sK1499_skl)],[f22130]) ).
fof(f22132,plain,
~ v3_struct_0(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22133,plain,
v3_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22134,plain,
v4_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22135,plain,
l1_group_1(sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22136,plain,
m1_group_2(sK1496_skl,sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22137,plain,
m1_group_2(sK1497_skl,sK1495_skl),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22138,plain,
m1_subset_1(sK1498_skl,u1_struct_0(k11_group_4(sK1495_skl))),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22139,plain,
m1_subset_1(sK1499_skl,u1_struct_0(k11_group_4(sK1495_skl))),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22140,plain,
sK1498_skl = sK1496_skl,
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22141,plain,
sK1499_skl = sK1497_skl,
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22142,plain,
( m1_group_6(sK1496_skl,sK1495_skl,sK1497_skl)
| r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1499_skl) ),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f22143,plain,
( ~ m1_group_6(sK1496_skl,sK1495_skl,sK1497_skl)
| ~ r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1499_skl) ),
inference(cnf_transformation,[status(thm)],[f22131]) ).
fof(f23594,definition,
! [X0] :
( sQ13_spl
<=> ( ~ r1_subset_1(X0,X0)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f23597,definition,
! [X1] :
( sQ14_spl
<=> v1_xboole_0(X1) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f23598,plain,
! [X0] :
( ~ sQ14_spl
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f23597]) ).
fof(f23600,plain,
( sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f6862,f23594,f23597]) ).
fof(f23601,definition,
! [X0] :
( sQ15_spl
<=> ( ~ r2_subset_1(X0,X0)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f23604,plain,
( sQ14_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f6871,f23601,f23597]) ).
fof(f25241,definition,
( sQ450_spl
<=> r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ450_spl])],[split_symbol_definition]) ).
fof(f25244,definition,
( sQ451_spl
<=> m1_group_6(sK1496_skl,sK1495_skl,sK1497_skl) ),
introduced(definition,[new_symbols(definition,[sQ451_spl])],[split_symbol_definition]) ).
fof(f25245,plain,
( ~ sQ451_spl
| m1_group_6(sK1496_skl,sK1495_skl,sK1497_skl) ),
inference(component_clause,[status(thm)],[f25244]) ).
fof(f25246,plain,
( sQ451_spl
| ~ m1_group_6(sK1496_skl,sK1495_skl,sK1497_skl) ),
inference(component_clause,[status(thm)],[f25244]) ).
fof(f25247,plain,
( sQ451_spl
| sQ450_spl ),
inference(split_clause,[status(thm)],[f22142,f25241,f25244]) ).
fof(f25248,plain,
( ~ sQ451_spl
| ~ sQ450_spl ),
inference(split_clause,[status(thm)],[f22143,f25241,f25244]) ).
fof(f26946,plain,
! [X0,X1] :
( v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f22123]) ).
fof(f26947,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)],[f22127]) ).
fof(f26948,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)],[f22128]) ).
fof(f27124,plain,
m1_group_2(sK1498_skl,sK1495_skl),
inference(forward_demodulation,[status(thm)],[f22140,f22136]) ).
fof(f27125,plain,
m1_group_2(sK1499_skl,sK1495_skl),
inference(forward_demodulation,[status(thm)],[f22141,f22137]) ).
fof(f27126,plain,
( ~ sQ451_spl
| m1_group_6(sK1498_skl,sK1495_skl,sK1497_skl) ),
inference(forward_demodulation,[status(thm)],[f22140,f25245]) ).
fof(f27127,plain,
( ~ sQ451_spl
| m1_group_6(sK1498_skl,sK1495_skl,sK1499_skl) ),
inference(forward_demodulation,[status(thm)],[f22141,f27126]) ).
fof(f27128,plain,
( ~ v3_struct_0(sK1499_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18211,f27125]) ).
fof(f27129,plain,
( ~ v3_struct_0(sK1498_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18211,f27124]) ).
fof(f27131,definition,
( sQ611_spl
<=> v3_struct_0(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ611_spl])],[split_symbol_definition]) ).
fof(f27132,plain,
( ~ sQ611_spl
| v3_struct_0(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27131]) ).
fof(f27134,definition,
( sQ612_spl
<=> v3_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition]) ).
fof(f27136,plain,
( sQ612_spl
| ~ v3_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27134]) ).
fof(f27137,definition,
( sQ613_spl
<=> l1_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f27139,plain,
( sQ613_spl
| ~ l1_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27137]) ).
fof(f27140,definition,
( sQ614_spl
<=> v3_struct_0(sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition]) ).
fof(f27143,plain,
( ~ sQ614_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27128,f27131,f27134,f27137,f27140]) ).
fof(f27144,definition,
( sQ615_spl
<=> v3_struct_0(sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition]) ).
fof(f27147,plain,
( ~ sQ615_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27129,f27131,f27134,f27137,f27144]) ).
fof(f27148,plain,
( sQ613_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27139,f22135]) ).
fof(f27149,plain,
sQ613_spl,
inference(contradiction_clause,[status(thm)],[f27148]) ).
fof(f27150,plain,
( sQ612_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27136,f22133]) ).
fof(f27151,plain,
sQ612_spl,
inference(contradiction_clause,[status(thm)],[f27150]) ).
fof(f27152,plain,
( ~ sQ611_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27132,f22132]) ).
fof(f27153,plain,
~ sQ611_spl,
inference(contradiction_clause,[status(thm)],[f27152]) ).
fof(f27154,plain,
( sQ451_spl
| ~ m1_group_6(sK1498_skl,sK1495_skl,sK1497_skl) ),
inference(forward_demodulation,[status(thm)],[f22140,f25246]) ).
fof(f27155,plain,
( sQ451_spl
| ~ m1_group_6(sK1498_skl,sK1495_skl,sK1499_skl) ),
inference(forward_demodulation,[status(thm)],[f22141,f27154]) ).
fof(f27158,plain,
( v3_group_1(sK1499_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18212,f27125]) ).
fof(f27159,plain,
( v3_group_1(sK1498_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18212,f27124]) ).
fof(f27161,definition,
( sQ616_spl
<=> v3_group_1(sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition]) ).
fof(f27164,plain,
( sQ616_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27158,f27131,f27134,f27137,f27161]) ).
fof(f27165,definition,
( sQ617_spl
<=> v3_group_1(sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f27168,plain,
( sQ617_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27159,f27131,f27134,f27137,f27165]) ).
fof(f27169,plain,
( l1_group_1(sK1499_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18213,f27125]) ).
fof(f27170,plain,
( l1_group_1(sK1498_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f18213,f27124]) ).
fof(f27172,definition,
( sQ618_spl
<=> l1_group_1(sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition]) ).
fof(f27175,plain,
( sQ618_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27169,f27131,f27134,f27137,f27172]) ).
fof(f27176,definition,
( sQ619_spl
<=> l1_group_1(sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ619_spl])],[split_symbol_definition]) ).
fof(f27179,plain,
( sQ619_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27170,f27131,f27134,f27137,f27176]) ).
fof(f27180,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5755,f23598]) ).
fof(f27181,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f27180]) ).
fof(f27185,plain,
( v4_group_1(sK1499_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f17663,f27125]) ).
fof(f27186,plain,
( v4_group_1(sK1498_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f17663,f27124]) ).
fof(f27188,definition,
( sQ620_spl
<=> v4_group_1(sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition]) ).
fof(f27190,plain,
( sQ620_spl
| ~ v4_group_1(sK1495_skl) ),
inference(component_clause,[status(thm)],[f27188]) ).
fof(f27191,definition,
( sQ621_spl
<=> v4_group_1(sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ621_spl])],[split_symbol_definition]) ).
fof(f27194,plain,
( sQ621_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27185,f27131,f27134,f27188,f27137,f27191]) ).
fof(f27195,definition,
( sQ622_spl
<=> v4_group_1(sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ622_spl])],[split_symbol_definition]) ).
fof(f27198,plain,
( sQ622_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27186,f27131,f27134,f27188,f27137,f27195]) ).
fof(f27199,plain,
( sQ620_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27190,f22134]) ).
fof(f27200,plain,
sQ620_spl,
inference(contradiction_clause,[status(thm)],[f27199]) ).
fof(f27204,definition,
( sQ623_spl
<=> v3_struct_0(k11_group_4(sK1495_skl)) ),
introduced(definition,[new_symbols(definition,[sQ623_spl])],[split_symbol_definition]) ).
fof(f27205,plain,
( ~ sQ623_spl
| v3_struct_0(k11_group_4(sK1495_skl)) ),
inference(component_clause,[status(thm)],[f27204]) ).
fof(f27213,definition,
( sQ626_spl
<=> m1_subset_1(sK1499_skl,u1_struct_0(k11_group_4(sK1495_skl))) ),
introduced(definition,[new_symbols(definition,[sQ626_spl])],[split_symbol_definition]) ).
fof(f27215,plain,
( sQ626_spl
| ~ m1_subset_1(sK1499_skl,u1_struct_0(k11_group_4(sK1495_skl))) ),
inference(component_clause,[status(thm)],[f27213]) ).
fof(f27220,plain,
( ~ sQ623_spl
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27205,f19602]) ).
fof(f27221,plain,
( ~ sQ623_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27220,f27131,f27134,f27188,f27137,f27204]) ).
fof(f27227,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)],[f17805,f18211]) ).
fof(f27228,plain,
! [X0,X1,X2] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X1,X2)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f17850,f18211]) ).
fof(f27229,plain,
! [X0] :
( m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(resolution,[status(thm)],[f27228,f27125]) ).
fof(f27230,plain,
! [X0] :
( m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(sK1498_skl)
| ~ v4_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(resolution,[status(thm)],[f27228,f27124]) ).
fof(f27232,definition,
! [X0] :
( sQ629_spl
<=> ( m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ629_spl])],[split_symbol_definition]) ).
fof(f27233,plain,
! [X0] :
( ~ sQ629_spl
| m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(component_clause,[status(thm)],[f27232]) ).
fof(f27235,plain,
( ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| ~ sQ618_spl
| ~ sQ621_spl
| ~ sQ616_spl
| sQ614_spl
| sQ629_spl ),
inference(split_clause,[status(thm)],[f27229,f27232,f27140,f27161,f27191,f27172,f27131,f27134,f27188,f27137]) ).
fof(f27236,definition,
! [X0] :
( sQ630_spl
<=> ( m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ630_spl])],[split_symbol_definition]) ).
fof(f27237,plain,
! [X0] :
( ~ sQ630_spl
| m1_group_2(X0,sK1495_skl)
| ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(component_clause,[status(thm)],[f27236]) ).
fof(f27239,plain,
( ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| ~ sQ619_spl
| ~ sQ622_spl
| ~ sQ617_spl
| sQ615_spl
| sQ630_spl ),
inference(split_clause,[status(thm)],[f27230,f27236,f27144,f27165,f27195,f27176,f27131,f27134,f27188,f27137]) ).
fof(f27246,plain,
( ~ sQ629_spl
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl)
| m1_group_2(sK1499_skl,sK1495_skl)
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl) ),
inference(resolution,[status(thm)],[f27233,f17846]) ).
fof(f27247,definition,
( sQ631_spl
<=> m1_group_2(sK1499_skl,sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition]) ).
fof(f27250,plain,
( ~ sQ629_spl
| sQ614_spl
| sQ631_spl
| ~ sQ618_spl
| ~ sQ621_spl
| ~ sQ616_spl ),
inference(split_clause,[status(thm)],[f27246,f27161,f27191,f27172,f27247,f27140,f27232]) ).
fof(f27251,plain,
( ~ sQ630_spl
| ~ l1_group_1(sK1498_skl)
| ~ v4_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl)
| m1_group_2(sK1498_skl,sK1495_skl)
| ~ l1_group_1(sK1498_skl)
| ~ v4_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl) ),
inference(resolution,[status(thm)],[f27237,f17846]) ).
fof(f27252,definition,
( sQ632_spl
<=> m1_group_2(sK1498_skl,sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition]) ).
fof(f27255,plain,
( ~ sQ630_spl
| sQ615_spl
| sQ632_spl
| ~ sQ619_spl
| ~ sQ622_spl
| ~ sQ617_spl ),
inference(split_clause,[status(thm)],[f27251,f27165,f27195,f27176,f27252,f27144,f27236]) ).
fof(f27256,plain,
( sQ451_spl
| ~ m1_group_2(sK1498_skl,sK1499_skl)
| ~ m1_group_2(sK1499_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f20783,f27155]) ).
fof(f27259,definition,
( sQ633_spl
<=> m1_group_2(sK1498_skl,sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ633_spl])],[split_symbol_definition]) ).
fof(f27262,plain,
( sQ451_spl
| ~ sQ633_spl
| ~ sQ631_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27256,f27131,f27134,f27188,f27137,f27247,f27259,f25244]) ).
fof(f27264,plain,
( ~ sQ451_spl
| m1_group_2(sK1498_skl,sK1499_skl)
| ~ m1_group_2(sK1499_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27127,f20782]) ).
fof(f27266,plain,
( ~ sQ451_spl
| sQ633_spl
| ~ sQ631_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27264,f27131,f27134,f27188,f27137,f27247,f27259,f25244]) ).
fof(f27294,plain,
( v1_group_1(sK1499_skl)
| ~ m1_group_2(sK1499_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f26946,f22139]) ).
fof(f27295,plain,
( v1_group_1(sK1498_skl)
| ~ m1_group_2(sK1498_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f26946,f22138]) ).
fof(f27296,definition,
( sQ635_spl
<=> v1_group_1(sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ635_spl])],[split_symbol_definition]) ).
fof(f27299,plain,
( sQ635_spl
| ~ sQ631_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27294,f27131,f27134,f27188,f27137,f27247,f27296]) ).
fof(f27300,definition,
( sQ636_spl
<=> v1_group_1(sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ636_spl])],[split_symbol_definition]) ).
fof(f27303,plain,
( sQ636_spl
| ~ sQ632_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27295,f27131,f27134,f27188,f27137,f27252,f27300]) ).
fof(f27305,plain,
! [X0,X1] :
( m1_group_2(X1,X1)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f17852,f5749]) ).
fof(f27306,plain,
! [X0,X1] :
( m1_group_2(X1,X1)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27305]) ).
fof(f27310,plain,
( m1_group_2(sK1499_skl,sK1499_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27306,f27125]) ).
fof(f27311,plain,
( m1_group_2(sK1498_skl,sK1498_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27306,f27124]) ).
fof(f27313,definition,
( sQ637_spl
<=> m1_group_2(sK1499_skl,sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ637_spl])],[split_symbol_definition]) ).
fof(f27316,plain,
( sQ637_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27310,f27131,f27134,f27188,f27137,f27313]) ).
fof(f27317,definition,
( sQ638_spl
<=> m1_group_2(sK1498_skl,sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f27318,plain,
( ~ sQ638_spl
| m1_group_2(sK1498_skl,sK1498_skl) ),
inference(component_clause,[status(thm)],[f27317]) ).
fof(f27320,plain,
( sQ638_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27311,f27131,f27134,f27188,f27137,f27317]) ).
fof(f27348,plain,
! [X0,X1,X2] :
( v1_group_3(X2,X1)
| ~ m1_group_6(X2,X0,X1)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f20477,f20775]) ).
fof(f27349,plain,
! [X0,X1,X2] :
( ~ m1_group_2(X2,X1)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_group_3(X2,X1)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27348,f20783]) ).
fof(f27350,plain,
! [X0,X1,X2] :
( ~ m1_group_2(X2,X1)
| v1_group_3(X2,X1)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27349]) ).
fof(f27354,plain,
! [X0] :
( ~ sQ638_spl
| v1_group_3(sK1498_skl,sK1498_skl)
| ~ v1_group_3(sK1498_skl,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27350,f27318]) ).
fof(f27355,plain,
! [X0] :
( v1_group_3(sK1498_skl,sK1495_skl)
| ~ v1_group_3(sK1498_skl,X0)
| ~ m1_group_2(sK1495_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27350,f27124]) ).
fof(f27356,plain,
! [X0,X1] :
( ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| v1_group_3(X1,X1)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27350,f17846]) ).
fof(f27371,definition,
! [X0] :
( sQ643_spl
<=> ( ~ v1_group_3(sK1498_skl,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ643_spl])],[split_symbol_definition]) ).
fof(f27372,plain,
! [X0] :
( ~ sQ643_spl
| ~ v1_group_3(sK1498_skl,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f27371]) ).
fof(f27374,definition,
( sQ644_spl
<=> v1_group_3(sK1498_skl,sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition]) ).
fof(f27377,plain,
( ~ sQ638_spl
| sQ644_spl
| sQ643_spl ),
inference(split_clause,[status(thm)],[f27354,f27371,f27374,f27317]) ).
fof(f27378,definition,
! [X0] :
( sQ645_spl
<=> ( ~ v1_group_3(sK1498_skl,X0)
| ~ m1_group_2(sK1495_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ645_spl])],[split_symbol_definition]) ).
fof(f27379,plain,
! [X0] :
( ~ sQ645_spl
| ~ v1_group_3(sK1498_skl,X0)
| ~ m1_group_2(sK1495_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f27378]) ).
fof(f27381,definition,
( sQ646_spl
<=> v1_group_3(sK1498_skl,sK1495_skl) ),
introduced(definition,[new_symbols(definition,[sQ646_spl])],[split_symbol_definition]) ).
fof(f27384,plain,
( sQ646_spl
| sQ645_spl ),
inference(split_clause,[status(thm)],[f27355,f27378,f27381]) ).
fof(f27385,plain,
! [X0,X1] :
( ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v1_group_3(X1,X1)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f27356,f18211]) ).
fof(f27387,plain,
( ~ sQ643_spl
| ~ v1_group_3(sK1498_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27372,f27124]) ).
fof(f27388,plain,
( ~ sQ643_spl
| ~ l1_group_1(sK1498_skl)
| ~ v4_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl)
| ~ v1_group_3(sK1498_skl,sK1498_skl)
| ~ l1_group_1(sK1498_skl)
| ~ v4_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl) ),
inference(resolution,[status(thm)],[f27372,f17846]) ).
fof(f27390,plain,
( ~ sQ643_spl
| ~ sQ646_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27387,f27131,f27134,f27188,f27137,f27381,f27371]) ).
fof(f27391,plain,
( ~ sQ643_spl
| ~ sQ644_spl
| ~ sQ619_spl
| ~ sQ622_spl
| ~ sQ617_spl
| sQ615_spl ),
inference(split_clause,[status(thm)],[f27388,f27144,f27165,f27195,f27176,f27374,f27371]) ).
fof(f27399,plain,
! [X0,X1,X2] :
( m1_group_2(k9_group_2(X0,X1,X2),X1)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f20483,f20782]) ).
fof(f27400,plain,
! [X0,X1,X2] :
( m1_group_2(k9_group_2(X0,X1,X2),X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f20483,f20775]) ).
fof(f27402,plain,
! [X0,X1,X2] :
( m1_group_2(k9_group_2(X0,X1,X2),X1)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27399]) ).
fof(f27403,plain,
! [X0,X1,X2] :
( m1_group_2(k9_group_2(X0,X1,X2),X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27400]) ).
fof(f27417,plain,
( ~ sQ645_spl
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ v1_group_3(sK1498_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27379,f17846]) ).
fof(f27418,plain,
( ~ sQ645_spl
| ~ sQ646_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27417,f27131,f27134,f27188,f27137,f27381,f27378]) ).
fof(f27421,plain,
! [X0,X1] :
( ~ sQ630_spl
| m1_group_2(k9_group_2(X0,sK1498_skl,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27402,f27237]) ).
fof(f27422,plain,
! [X0,X1] :
( ~ sQ629_spl
| m1_group_2(k9_group_2(X0,sK1499_skl,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27402,f27233]) ).
fof(f27436,plain,
! [X0,X1] :
( ~ sQ630_spl
| m1_group_2(k9_group_2(X0,sK1498_skl,X1),k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27421,f27306]) ).
fof(f27438,plain,
! [X0,X1] :
( ~ sQ630_spl
| v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27421,f17663]) ).
fof(f27439,plain,
! [X0,X1] :
( ~ sQ630_spl
| l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27421,f18213]) ).
fof(f27440,plain,
! [X0,X1] :
( ~ sQ630_spl
| v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27421,f18212]) ).
fof(f27441,plain,
! [X0,X1] :
( ~ sQ630_spl
| ~ v3_struct_0(k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27421,f18211]) ).
fof(f27442,definition,
! [X0,X1] :
( sQ647_spl
<=> ( m1_group_2(k9_group_2(X0,sK1498_skl,X1),k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ647_spl])],[split_symbol_definition]) ).
fof(f27445,plain,
( ~ sQ630_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ647_spl ),
inference(split_clause,[status(thm)],[f27436,f27442,f27131,f27134,f27188,f27137,f27236]) ).
fof(f27446,definition,
! [X0,X1] :
( sQ648_spl
<=> ( v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ648_spl])],[split_symbol_definition]) ).
fof(f27449,plain,
( ~ sQ630_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ648_spl ),
inference(split_clause,[status(thm)],[f27438,f27446,f27131,f27134,f27188,f27137,f27236]) ).
fof(f27450,definition,
! [X0,X1] :
( sQ649_spl
<=> ( l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition]) ).
fof(f27453,plain,
( ~ sQ630_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ649_spl ),
inference(split_clause,[status(thm)],[f27439,f27450,f27131,f27134,f27137,f27236]) ).
fof(f27454,definition,
! [X0,X1] :
( sQ650_spl
<=> ( v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ650_spl])],[split_symbol_definition]) ).
fof(f27457,plain,
( ~ sQ630_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ650_spl ),
inference(split_clause,[status(thm)],[f27440,f27454,f27131,f27134,f27137,f27236]) ).
fof(f27458,definition,
! [X0,X1] :
( sQ651_spl
<=> ( ~ v3_struct_0(k9_group_2(X0,sK1498_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1498_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition]) ).
fof(f27461,plain,
( ~ sQ630_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ651_spl ),
inference(split_clause,[status(thm)],[f27441,f27458,f27131,f27134,f27137,f27236]) ).
fof(f27463,plain,
! [X0,X1] :
( ~ sQ629_spl
| m1_group_2(k9_group_2(X0,sK1499_skl,X1),k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27422,f27306]) ).
fof(f27465,plain,
! [X0,X1] :
( ~ sQ629_spl
| v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27422,f17663]) ).
fof(f27466,plain,
! [X0,X1] :
( ~ sQ629_spl
| l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27422,f18213]) ).
fof(f27467,plain,
! [X0,X1] :
( ~ sQ629_spl
| v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27422,f18212]) ).
fof(f27468,plain,
! [X0,X1] :
( ~ sQ629_spl
| ~ v3_struct_0(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27422,f18211]) ).
fof(f27469,definition,
! [X0,X1] :
( sQ652_spl
<=> ( m1_group_2(k9_group_2(X0,sK1499_skl,X1),k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ652_spl])],[split_symbol_definition]) ).
fof(f27472,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ652_spl ),
inference(split_clause,[status(thm)],[f27463,f27469,f27131,f27134,f27188,f27137,f27232]) ).
fof(f27473,definition,
! [X0,X1] :
( sQ653_spl
<=> ( v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ653_spl])],[split_symbol_definition]) ).
fof(f27476,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ653_spl ),
inference(split_clause,[status(thm)],[f27465,f27473,f27131,f27134,f27188,f27137,f27232]) ).
fof(f27477,definition,
! [X0,X1] :
( sQ654_spl
<=> ( l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f27480,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ654_spl ),
inference(split_clause,[status(thm)],[f27466,f27477,f27131,f27134,f27137,f27232]) ).
fof(f27481,definition,
! [X0,X1] :
( sQ655_spl
<=> ( v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ655_spl])],[split_symbol_definition]) ).
fof(f27484,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ655_spl ),
inference(split_clause,[status(thm)],[f27467,f27481,f27131,f27134,f27137,f27232]) ).
fof(f27485,definition,
! [X0,X1] :
( sQ656_spl
<=> ( ~ v3_struct_0(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition]) ).
fof(f27488,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ656_spl ),
inference(split_clause,[status(thm)],[f27468,f27485,f27131,f27134,f27137,f27232]) ).
fof(f27489,plain,
! [X0,X1] :
( ~ sQ630_spl
| m1_group_2(k9_group_2(sK1498_skl,X0,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(sK1498_skl)
| ~ v4_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl) ),
inference(resolution,[status(thm)],[f27403,f27237]) ).
fof(f27490,plain,
! [X0,X1] :
( ~ sQ629_spl
| m1_group_2(k9_group_2(sK1499_skl,X0,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl) ),
inference(resolution,[status(thm)],[f27403,f27233]) ).
fof(f27494,plain,
! [X0,X1,X2] :
( v4_group_1(k9_group_2(X0,X1,X2))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27403,f17663]) ).
fof(f27495,plain,
! [X0,X1,X2] :
( l1_group_1(k9_group_2(X0,X1,X2))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27403,f18213]) ).
fof(f27496,plain,
! [X0,X1,X2] :
( v3_group_1(k9_group_2(X0,X1,X2))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27403,f18212]) ).
fof(f27498,definition,
! [X0,X1] :
( sQ657_spl
<=> ( m1_group_2(k9_group_2(sK1498_skl,X0,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition]) ).
fof(f27499,plain,
! [X0,X1] :
( ~ sQ657_spl
| m1_group_2(k9_group_2(sK1498_skl,X0,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ),
inference(component_clause,[status(thm)],[f27498]) ).
fof(f27501,plain,
( ~ sQ630_spl
| sQ657_spl
| ~ sQ619_spl
| ~ sQ622_spl
| ~ sQ617_spl
| sQ615_spl ),
inference(split_clause,[status(thm)],[f27489,f27144,f27165,f27195,f27176,f27498,f27236]) ).
fof(f27502,definition,
! [X0,X1] :
( sQ658_spl
<=> ( m1_group_2(k9_group_2(sK1499_skl,X0,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition]) ).
fof(f27503,plain,
! [X0,X1] :
( ~ sQ658_spl
| m1_group_2(k9_group_2(sK1499_skl,X0,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(component_clause,[status(thm)],[f27502]) ).
fof(f27505,plain,
( ~ sQ629_spl
| sQ658_spl
| ~ sQ618_spl
| ~ sQ621_spl
| ~ sQ616_spl
| sQ614_spl ),
inference(split_clause,[status(thm)],[f27490,f27140,f27161,f27191,f27172,f27502,f27232]) ).
fof(f27509,plain,
! [X0,X1,X2] :
( v4_group_1(k9_group_2(X0,X1,X2))
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27494]) ).
fof(f27510,plain,
! [X0,X1,X2] :
( l1_group_1(k9_group_2(X0,X1,X2))
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27495]) ).
fof(f27511,plain,
! [X0,X1,X2] :
( v3_group_1(k9_group_2(X0,X1,X2))
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27496]) ).
fof(f27513,plain,
! [X0,X1] :
( ~ sQ629_spl
| m1_group_2(k9_group_2(X0,sK1499_skl,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f27422,f27509]) ).
fof(f27517,plain,
! [X0,X1,X2] :
( m1_group_2(k9_group_2(X0,X2,X1),X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f20485,f20775]) ).
fof(f27520,plain,
! [X0,X1,X2] :
( m1_group_2(k9_group_2(X0,X2,X1),X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27517]) ).
fof(f27535,plain,
! [X0,X1] :
( ~ sQ630_spl
| m1_group_2(k9_group_2(sK1498_skl,X1,X0),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X1,X0))
| ~ v4_group_1(k9_group_2(sK1498_skl,X1,X0))
| ~ v3_group_1(k9_group_2(sK1498_skl,X1,X0))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(sK1498_skl)
| ~ v4_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl) ),
inference(resolution,[status(thm)],[f27520,f27237]) ).
fof(f27536,plain,
! [X0,X1] :
( ~ sQ629_spl
| m1_group_2(k9_group_2(sK1499_skl,X1,X0),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X1,X0))
| ~ v4_group_1(k9_group_2(sK1499_skl,X1,X0))
| ~ v3_group_1(k9_group_2(sK1499_skl,X1,X0))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl) ),
inference(resolution,[status(thm)],[f27520,f27233]) ).
fof(f27541,plain,
! [X0,X1,X2] :
( l1_group_1(k9_group_2(X0,X2,X1))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27520,f18213]) ).
fof(f27544,definition,
! [X0,X1] :
( sQ659_spl
<=> ( m1_group_2(k9_group_2(sK1498_skl,X1,X0),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X1,X0))
| ~ v4_group_1(k9_group_2(sK1498_skl,X1,X0))
| ~ v3_group_1(k9_group_2(sK1498_skl,X1,X0))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ659_spl])],[split_symbol_definition]) ).
fof(f27547,plain,
( ~ sQ630_spl
| sQ659_spl
| ~ sQ619_spl
| ~ sQ622_spl
| ~ sQ617_spl
| sQ615_spl ),
inference(split_clause,[status(thm)],[f27535,f27144,f27165,f27195,f27176,f27544,f27236]) ).
fof(f27548,definition,
! [X0,X1] :
( sQ660_spl
<=> ( m1_group_2(k9_group_2(sK1499_skl,X1,X0),sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X1,X0))
| ~ v4_group_1(k9_group_2(sK1499_skl,X1,X0))
| ~ v3_group_1(k9_group_2(sK1499_skl,X1,X0))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ660_spl])],[split_symbol_definition]) ).
fof(f27551,plain,
( ~ sQ629_spl
| sQ660_spl
| ~ sQ618_spl
| ~ sQ621_spl
| ~ sQ616_spl
| sQ614_spl ),
inference(split_clause,[status(thm)],[f27536,f27140,f27161,f27191,f27172,f27548,f27232]) ).
fof(f27556,plain,
! [X0,X1,X2] :
( l1_group_1(k9_group_2(X0,X2,X1))
| ~ m1_group_2(X2,X0)
| ~ v1_group_3(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27541]) ).
fof(f27569,plain,
! [X0,X1] :
( ~ sQ658_spl
| m1_group_2(k9_group_2(sK1499_skl,X0,X1),k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(resolution,[status(thm)],[f27503,f27306]) ).
fof(f27571,plain,
! [X0,X1] :
( ~ sQ658_spl
| v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(resolution,[status(thm)],[f27503,f17663]) ).
fof(f27572,plain,
! [X0,X1] :
( ~ sQ658_spl
| l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(resolution,[status(thm)],[f27503,f18213]) ).
fof(f27573,plain,
! [X0,X1] :
( ~ sQ658_spl
| v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(resolution,[status(thm)],[f27503,f18212]) ).
fof(f27574,plain,
! [X0,X1] :
( ~ sQ658_spl
| ~ v3_struct_0(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(resolution,[status(thm)],[f27503,f18211]) ).
fof(f27575,definition,
! [X0,X1] :
( sQ661_spl
<=> ( m1_group_2(k9_group_2(sK1499_skl,X0,X1),k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ661_spl])],[split_symbol_definition]) ).
fof(f27578,plain,
( ~ sQ658_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ661_spl ),
inference(split_clause,[status(thm)],[f27569,f27575,f27131,f27134,f27188,f27137,f27502]) ).
fof(f27579,definition,
! [X0,X1] :
( sQ662_spl
<=> ( v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ662_spl])],[split_symbol_definition]) ).
fof(f27582,plain,
( ~ sQ658_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ662_spl ),
inference(split_clause,[status(thm)],[f27571,f27579,f27131,f27134,f27188,f27137,f27502]) ).
fof(f27583,definition,
! [X0,X1] :
( sQ663_spl
<=> ( l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ663_spl])],[split_symbol_definition]) ).
fof(f27586,plain,
( ~ sQ658_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ663_spl ),
inference(split_clause,[status(thm)],[f27572,f27583,f27131,f27134,f27137,f27502]) ).
fof(f27587,definition,
! [X0,X1] :
( sQ664_spl
<=> ( v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ664_spl])],[split_symbol_definition]) ).
fof(f27590,plain,
( ~ sQ658_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ664_spl ),
inference(split_clause,[status(thm)],[f27573,f27587,f27131,f27134,f27137,f27502]) ).
fof(f27591,definition,
! [X0,X1] :
( sQ665_spl
<=> ( ~ v3_struct_0(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ665_spl])],[split_symbol_definition]) ).
fof(f27592,plain,
! [X0,X1] :
( ~ sQ665_spl
| ~ v3_struct_0(k9_group_2(sK1499_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(component_clause,[status(thm)],[f27591]) ).
fof(f27594,plain,
( ~ sQ658_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ665_spl ),
inference(split_clause,[status(thm)],[f27574,f27591,f27131,f27134,f27137,f27502]) ).
fof(f27595,plain,
! [X0,X1] :
( ~ sQ665_spl
| ~ m1_group_2(X0,sK1499_skl)
| ~ v1_group_3(X0,sK1499_skl)
| ~ m1_group_2(X1,sK1499_skl)
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl)
| ~ v3_struct_0(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(resolution,[status(thm)],[f27592,f27556]) ).
fof(f27596,plain,
! [X0,X1] :
( ~ sQ665_spl
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl)
| ~ v3_struct_0(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ),
inference(resolution,[status(thm)],[f27592,f27510]) ).
fof(f27597,definition,
! [X0,X1] :
( sQ666_spl
<=> ( ~ m1_group_2(X0,sK1499_skl)
| ~ v1_group_3(X0,sK1499_skl)
| ~ m1_group_2(X1,sK1499_skl)
| ~ v3_struct_0(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ666_spl])],[split_symbol_definition]) ).
fof(f27600,plain,
( ~ sQ665_spl
| ~ sQ618_spl
| ~ sQ621_spl
| ~ sQ616_spl
| sQ614_spl
| sQ666_spl ),
inference(split_clause,[status(thm)],[f27595,f27597,f27140,f27161,f27191,f27172,f27591]) ).
fof(f27601,definition,
! [X0,X1] :
( sQ667_spl
<=> ( ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ v3_struct_0(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ667_spl])],[split_symbol_definition]) ).
fof(f27604,plain,
( ~ sQ665_spl
| ~ sQ618_spl
| ~ sQ621_spl
| ~ sQ616_spl
| sQ614_spl
| sQ667_spl ),
inference(split_clause,[status(thm)],[f27596,f27601,f27140,f27161,f27191,f27172,f27591]) ).
fof(f27608,plain,
! [X0,X1] :
( ~ sQ657_spl
| m1_group_2(k9_group_2(sK1498_skl,X0,X1),k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ),
inference(resolution,[status(thm)],[f27499,f27306]) ).
fof(f27610,plain,
! [X0,X1] :
( ~ sQ657_spl
| v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ),
inference(resolution,[status(thm)],[f27499,f17663]) ).
fof(f27611,plain,
! [X0,X1] :
( ~ sQ657_spl
| l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ),
inference(resolution,[status(thm)],[f27499,f18213]) ).
fof(f27612,plain,
! [X0,X1] :
( ~ sQ657_spl
| v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ),
inference(resolution,[status(thm)],[f27499,f18212]) ).
fof(f27613,plain,
! [X0,X1] :
( ~ sQ657_spl
| ~ v3_struct_0(k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ),
inference(resolution,[status(thm)],[f27499,f18211]) ).
fof(f27614,definition,
! [X0,X1] :
( sQ668_spl
<=> ( m1_group_2(k9_group_2(sK1498_skl,X0,X1),k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ668_spl])],[split_symbol_definition]) ).
fof(f27617,plain,
( ~ sQ657_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ668_spl ),
inference(split_clause,[status(thm)],[f27608,f27614,f27131,f27134,f27188,f27137,f27498]) ).
fof(f27618,definition,
! [X0,X1] :
( sQ669_spl
<=> ( v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ669_spl])],[split_symbol_definition]) ).
fof(f27621,plain,
( ~ sQ657_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ669_spl ),
inference(split_clause,[status(thm)],[f27610,f27618,f27131,f27134,f27188,f27137,f27498]) ).
fof(f27622,definition,
! [X0,X1] :
( sQ670_spl
<=> ( l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ670_spl])],[split_symbol_definition]) ).
fof(f27625,plain,
( ~ sQ657_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ670_spl ),
inference(split_clause,[status(thm)],[f27611,f27622,f27131,f27134,f27137,f27498]) ).
fof(f27626,definition,
! [X0,X1] :
( sQ671_spl
<=> ( v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ671_spl])],[split_symbol_definition]) ).
fof(f27629,plain,
( ~ sQ657_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ671_spl ),
inference(split_clause,[status(thm)],[f27612,f27626,f27131,f27134,f27137,f27498]) ).
fof(f27630,definition,
! [X0,X1] :
( sQ672_spl
<=> ( ~ v3_struct_0(k9_group_2(sK1498_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ672_spl])],[split_symbol_definition]) ).
fof(f27633,plain,
( ~ sQ657_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ672_spl ),
inference(split_clause,[status(thm)],[f27613,f27630,f27131,f27134,f27137,f27498]) ).
fof(f27634,plain,
! [X0,X1] :
( ~ sQ629_spl
| m1_group_2(k9_group_2(X0,sK1499_skl,X1),sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f27513,f27511]) ).
fof(f27636,plain,
! [X0,X1] :
( ~ sQ629_spl
| m1_group_2(k9_group_2(X0,sK1499_skl,X1),k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27634,f27306]) ).
fof(f27638,plain,
! [X0,X1] :
( ~ sQ629_spl
| v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27634,f17663]) ).
fof(f27639,plain,
! [X0,X1] :
( ~ sQ629_spl
| l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27634,f18213]) ).
fof(f27640,plain,
! [X0,X1] :
( ~ sQ629_spl
| v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27634,f18212]) ).
fof(f27641,plain,
! [X0,X1] :
( ~ sQ629_spl
| ~ v3_struct_0(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27634,f18211]) ).
fof(f27643,definition,
! [X0,X1] :
( sQ673_spl
<=> ( m1_group_2(k9_group_2(X0,sK1499_skl,X1),k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ673_spl])],[split_symbol_definition]) ).
fof(f27646,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ673_spl ),
inference(split_clause,[status(thm)],[f27636,f27643,f27131,f27134,f27188,f27137,f27232]) ).
fof(f27648,definition,
! [X0,X1] :
( sQ674_spl
<=> ( v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ674_spl])],[split_symbol_definition]) ).
fof(f27651,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl
| sQ674_spl ),
inference(split_clause,[status(thm)],[f27638,f27648,f27131,f27134,f27188,f27137,f27232]) ).
fof(f27652,definition,
! [X0,X1] :
( sQ675_spl
<=> ( l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ675_spl])],[split_symbol_definition]) ).
fof(f27655,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ675_spl ),
inference(split_clause,[status(thm)],[f27639,f27652,f27131,f27134,f27137,f27232]) ).
fof(f27656,definition,
! [X0,X1] :
( sQ676_spl
<=> ( v3_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ676_spl])],[split_symbol_definition]) ).
fof(f27659,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ676_spl ),
inference(split_clause,[status(thm)],[f27640,f27656,f27131,f27134,f27137,f27232]) ).
fof(f27660,definition,
! [X0,X1] :
( sQ677_spl
<=> ( ~ v3_struct_0(k9_group_2(X0,sK1499_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ677_spl])],[split_symbol_definition]) ).
fof(f27663,plain,
( ~ sQ629_spl
| ~ sQ613_spl
| ~ sQ612_spl
| sQ611_spl
| sQ677_spl ),
inference(split_clause,[status(thm)],[f27641,f27660,f27131,f27134,f27137,f27232]) ).
fof(f27665,plain,
! [X0,X1] :
( ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| v1_group_3(X1,X1)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f27385,f18212]) ).
fof(f27666,plain,
! [X0,X1] :
( ~ sQ657_spl
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| v1_group_3(k9_group_2(sK1498_skl,X0,X1),k9_group_2(sK1498_skl,X0,X1))
| ~ v1_group_3(k9_group_2(sK1498_skl,X0,X1),sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27665,f27499]) ).
fof(f27667,plain,
! [X0,X1] :
( ~ sQ658_spl
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| v1_group_3(k9_group_2(sK1499_skl,X0,X1),k9_group_2(sK1499_skl,X0,X1))
| ~ v1_group_3(k9_group_2(sK1499_skl,X0,X1),sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27665,f27503]) ).
fof(f27668,plain,
! [X0,X1] :
( ~ sQ629_spl
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| v1_group_3(k9_group_2(X0,sK1499_skl,X1),k9_group_2(X0,sK1499_skl,X1))
| ~ v1_group_3(k9_group_2(X0,sK1499_skl,X1),sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27665,f27634]) ).
fof(f27678,definition,
! [X0,X1] :
( sQ678_spl
<=> ( ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ m1_group_2(X1,sK1498_skl)
| ~ v1_group_3(X1,sK1498_skl)
| ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(k9_group_2(sK1498_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1498_skl,X0,X1))
| v1_group_3(k9_group_2(sK1498_skl,X0,X1),k9_group_2(sK1498_skl,X0,X1))
| ~ v1_group_3(k9_group_2(sK1498_skl,X0,X1),sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ678_spl])],[split_symbol_definition]) ).
fof(f27681,plain,
( ~ sQ657_spl
| sQ678_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27666,f27131,f27134,f27188,f27137,f27678,f27498]) ).
fof(f27682,definition,
! [X0,X1] :
( sQ679_spl
<=> ( ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ m1_group_2(X1,sK1499_skl)
| ~ v1_group_3(X1,sK1499_skl)
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(k9_group_2(sK1499_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK1499_skl,X0,X1))
| v1_group_3(k9_group_2(sK1499_skl,X0,X1),k9_group_2(sK1499_skl,X0,X1))
| ~ v1_group_3(k9_group_2(sK1499_skl,X0,X1),sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ679_spl])],[split_symbol_definition]) ).
fof(f27685,plain,
( ~ sQ658_spl
| sQ679_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27667,f27131,f27134,f27188,f27137,f27682,f27502]) ).
fof(f27686,definition,
! [X0,X1] :
( sQ680_spl
<=> ( ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(k9_group_2(X0,sK1499_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK1499_skl,X1))
| v1_group_3(k9_group_2(X0,sK1499_skl,X1),k9_group_2(X0,sK1499_skl,X1))
| ~ v1_group_3(k9_group_2(X0,sK1499_skl,X1),sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ680_spl])],[split_symbol_definition]) ).
fof(f27689,plain,
( ~ sQ629_spl
| sQ680_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27668,f27131,f27134,f27188,f27137,f27686,f27232]) ).
fof(f27720,plain,
! [X0] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(sK1499_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(sK1499_skl,sK1495_skl)
| ~ m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f26947,f22139]) ).
fof(f27721,plain,
! [X0] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(sK1498_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),X0,sK1498_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(sK1498_skl,sK1495_skl)
| ~ m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f26947,f22138]) ).
fof(f27722,definition,
! [X0] :
( sQ681_spl
<=> ( r1_tarski(u1_struct_0(X0),u1_struct_0(sK1499_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ681_spl])],[split_symbol_definition]) ).
fof(f27723,plain,
! [X0] :
( ~ sQ681_spl
| r1_tarski(u1_struct_0(X0),u1_struct_0(sK1499_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ),
inference(component_clause,[status(thm)],[f27722]) ).
fof(f27725,plain,
( ~ sQ631_spl
| sQ681_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27720,f27131,f27134,f27188,f27137,f27722,f27247]) ).
fof(f27726,definition,
! [X0] :
( sQ682_spl
<=> ( r1_tarski(u1_struct_0(X0),u1_struct_0(sK1498_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),X0,sK1498_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ682_spl])],[split_symbol_definition]) ).
fof(f27727,plain,
! [X0] :
( ~ sQ682_spl
| r1_tarski(u1_struct_0(X0),u1_struct_0(sK1498_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),X0,sK1498_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ),
inference(component_clause,[status(thm)],[f27726]) ).
fof(f27729,plain,
( ~ sQ632_spl
| sQ682_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27721,f27131,f27134,f27188,f27137,f27726,f27252]) ).
fof(f27742,plain,
( ~ sQ681_spl
| r1_tarski(u1_struct_0(sK1499_skl),u1_struct_0(sK1499_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),sK1499_skl,sK1499_skl)
| ~ m1_group_2(sK1499_skl,sK1495_skl) ),
inference(resolution,[status(thm)],[f27723,f22139]) ).
fof(f27743,plain,
( ~ sQ681_spl
| r1_tarski(u1_struct_0(sK1498_skl),u1_struct_0(sK1499_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1499_skl)
| ~ m1_group_2(sK1498_skl,sK1495_skl) ),
inference(resolution,[status(thm)],[f27723,f22138]) ).
fof(f27744,definition,
( sQ683_spl
<=> r3_lattices(k11_group_4(sK1495_skl),sK1499_skl,sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ683_spl])],[split_symbol_definition]) ).
fof(f27747,definition,
( sQ684_spl
<=> r1_tarski(u1_struct_0(sK1499_skl),u1_struct_0(sK1499_skl)) ),
introduced(definition,[new_symbols(definition,[sQ684_spl])],[split_symbol_definition]) ).
fof(f27750,plain,
( ~ sQ681_spl
| sQ684_spl
| ~ sQ683_spl
| ~ sQ631_spl ),
inference(split_clause,[status(thm)],[f27742,f27247,f27744,f27747,f27722]) ).
fof(f27751,definition,
( sQ685_spl
<=> r1_tarski(u1_struct_0(sK1498_skl),u1_struct_0(sK1499_skl)) ),
introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition]) ).
fof(f27752,plain,
( ~ sQ685_spl
| r1_tarski(u1_struct_0(sK1498_skl),u1_struct_0(sK1499_skl)) ),
inference(component_clause,[status(thm)],[f27751]) ).
fof(f27754,plain,
( ~ sQ681_spl
| sQ685_spl
| ~ sQ450_spl
| ~ sQ632_spl ),
inference(split_clause,[status(thm)],[f27743,f27252,f25241,f27751,f27722]) ).
fof(f27765,definition,
( sQ686_spl
<=> v1_group_3(sK1498_skl,sK1499_skl) ),
introduced(definition,[new_symbols(definition,[sQ686_spl])],[split_symbol_definition]) ).
fof(f27771,definition,
! [X0] :
( sQ687_spl
<=> ( ~ v1_group_3(sK1498_skl,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ687_spl])],[split_symbol_definition]) ).
fof(f27772,plain,
! [X0] :
( ~ sQ687_spl
| ~ v1_group_3(sK1498_skl,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f27771]) ).
fof(f27782,plain,
! [X0] :
( ~ sQ685_spl
| m1_group_2(sK1498_skl,sK1499_skl)
| ~ m1_group_2(sK1499_skl,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27752,f17852]) ).
fof(f27783,definition,
! [X0] :
( sQ688_spl
<=> ( ~ m1_group_2(sK1499_skl,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ688_spl])],[split_symbol_definition]) ).
fof(f27784,plain,
! [X0] :
( ~ sQ688_spl
| ~ m1_group_2(sK1499_skl,X0)
| ~ m1_group_2(sK1498_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f27783]) ).
fof(f27786,plain,
( ~ sQ685_spl
| sQ633_spl
| sQ688_spl ),
inference(split_clause,[status(thm)],[f27782,f27783,f27259,f27751]) ).
fof(f27788,plain,
( ~ sQ687_spl
| ~ v1_group_3(sK1498_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27772,f27125]) ).
fof(f27789,plain,
( ~ sQ687_spl
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl)
| ~ v1_group_3(sK1498_skl,sK1499_skl)
| ~ l1_group_1(sK1499_skl)
| ~ v4_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl) ),
inference(resolution,[status(thm)],[f27772,f17846]) ).
fof(f27791,plain,
( ~ sQ687_spl
| ~ sQ646_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27788,f27131,f27134,f27188,f27137,f27381,f27771]) ).
fof(f27792,plain,
( ~ sQ687_spl
| ~ sQ686_spl
| ~ sQ618_spl
| ~ sQ621_spl
| ~ sQ616_spl
| sQ614_spl ),
inference(split_clause,[status(thm)],[f27789,f27140,f27161,f27191,f27172,f27765,f27771]) ).
fof(f27794,plain,
( ~ sQ688_spl
| ~ m1_group_2(sK1499_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27784,f27124]) ).
fof(f27796,definition,
( sQ689_spl
<=> m1_group_2(sK1499_skl,sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ689_spl])],[split_symbol_definition]) ).
fof(f27797,plain,
( ~ sQ689_spl
| m1_group_2(sK1499_skl,sK1498_skl) ),
inference(component_clause,[status(thm)],[f27796]) ).
fof(f27800,plain,
( ~ sQ688_spl
| ~ sQ631_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27794,f27131,f27134,f27188,f27137,f27247,f27783]) ).
fof(f27851,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK1499_skl))
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(sK1499_skl,sK1495_skl)
| ~ m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f26948,f22139]) ).
fof(f27852,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK1498_skl))
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1498_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(sK1498_skl,sK1495_skl)
| ~ m1_group_2(X0,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f26948,f22138]) ).
fof(f27854,plain,
! [X0,X1] :
( r3_lattices(k11_group_4(X0),X1,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f26948,f5749]) ).
fof(f27855,definition,
! [X0] :
( sQ692_spl
<=> ( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK1499_skl))
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ692_spl])],[split_symbol_definition]) ).
fof(f27856,plain,
! [X0] :
( ~ sQ692_spl
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK1499_skl))
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ),
inference(component_clause,[status(thm)],[f27855]) ).
fof(f27858,plain,
( ~ sQ631_spl
| sQ692_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27851,f27131,f27134,f27188,f27137,f27855,f27247]) ).
fof(f27859,definition,
! [X0] :
( sQ693_spl
<=> ( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK1498_skl))
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1498_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ693_spl])],[split_symbol_definition]) ).
fof(f27860,plain,
! [X0] :
( ~ sQ693_spl
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK1498_skl))
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1498_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ),
inference(component_clause,[status(thm)],[f27859]) ).
fof(f27862,plain,
( ~ sQ632_spl
| sQ693_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27852,f27131,f27134,f27188,f27137,f27859,f27252]) ).
fof(f27864,plain,
! [X0,X1] :
( r3_lattices(k11_group_4(X0),X1,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27854]) ).
fof(f27889,plain,
( ~ sQ682_spl
| r1_tarski(u1_struct_0(sK1499_skl),u1_struct_0(sK1498_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),sK1499_skl,sK1498_skl)
| ~ m1_group_2(sK1499_skl,sK1495_skl) ),
inference(resolution,[status(thm)],[f27727,f22139]) ).
fof(f27890,plain,
( ~ sQ682_spl
| r1_tarski(u1_struct_0(sK1498_skl),u1_struct_0(sK1498_skl))
| ~ r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1498_skl)
| ~ m1_group_2(sK1498_skl,sK1495_skl) ),
inference(resolution,[status(thm)],[f27727,f22138]) ).
fof(f27891,definition,
( sQ694_spl
<=> r3_lattices(k11_group_4(sK1495_skl),sK1499_skl,sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ694_spl])],[split_symbol_definition]) ).
fof(f27894,definition,
( sQ695_spl
<=> r1_tarski(u1_struct_0(sK1499_skl),u1_struct_0(sK1498_skl)) ),
introduced(definition,[new_symbols(definition,[sQ695_spl])],[split_symbol_definition]) ).
fof(f27895,plain,
( ~ sQ695_spl
| r1_tarski(u1_struct_0(sK1499_skl),u1_struct_0(sK1498_skl)) ),
inference(component_clause,[status(thm)],[f27894]) ).
fof(f27896,plain,
( sQ695_spl
| ~ r1_tarski(u1_struct_0(sK1499_skl),u1_struct_0(sK1498_skl)) ),
inference(component_clause,[status(thm)],[f27894]) ).
fof(f27897,plain,
( ~ sQ682_spl
| sQ695_spl
| ~ sQ694_spl
| ~ sQ631_spl ),
inference(split_clause,[status(thm)],[f27889,f27247,f27891,f27894,f27726]) ).
fof(f27898,definition,
( sQ696_spl
<=> r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1498_skl) ),
introduced(definition,[new_symbols(definition,[sQ696_spl])],[split_symbol_definition]) ).
fof(f27901,definition,
( sQ697_spl
<=> r1_tarski(u1_struct_0(sK1498_skl),u1_struct_0(sK1498_skl)) ),
introduced(definition,[new_symbols(definition,[sQ697_spl])],[split_symbol_definition]) ).
fof(f27904,plain,
( ~ sQ682_spl
| sQ697_spl
| ~ sQ696_spl
| ~ sQ632_spl ),
inference(split_clause,[status(thm)],[f27890,f27252,f27898,f27901,f27726]) ).
fof(f27905,plain,
! [X0] :
( ~ sQ692_spl
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| v3_struct_0(sK1499_skl)
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ),
inference(resolution,[status(thm)],[f27856,f27227]) ).
fof(f27906,plain,
( ~ sQ692_spl
| r3_lattices(k11_group_4(sK1495_skl),sK1499_skl,sK1499_skl)
| ~ m1_subset_1(sK1499_skl,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(sK1499_skl,sK1495_skl) ),
inference(resolution,[status(thm)],[f27856,f5749]) ).
fof(f27907,definition,
! [X0] :
( sQ698_spl
<=> ( ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ698_spl])],[split_symbol_definition]) ).
fof(f27908,plain,
! [X0] :
( ~ sQ698_spl
| ~ m1_group_2(X0,sK1499_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1499_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ),
inference(component_clause,[status(thm)],[f27907]) ).
fof(f27910,plain,
( ~ sQ692_spl
| ~ sQ618_spl
| ~ sQ616_spl
| sQ614_spl
| sQ698_spl ),
inference(split_clause,[status(thm)],[f27905,f27907,f27140,f27161,f27172,f27855]) ).
fof(f27911,plain,
( ~ sQ692_spl
| sQ683_spl
| ~ sQ626_spl
| ~ sQ631_spl ),
inference(split_clause,[status(thm)],[f27906,f27247,f27213,f27744,f27855]) ).
fof(f27912,plain,
( sQ626_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27215,f22139]) ).
fof(f27913,plain,
sQ626_spl,
inference(contradiction_clause,[status(thm)],[f27912]) ).
fof(f27915,plain,
! [X0] :
( ~ sQ695_spl
| m1_group_2(sK1499_skl,sK1498_skl)
| ~ m1_group_2(sK1498_skl,X0)
| ~ m1_group_2(sK1499_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f27895,f17852]) ).
fof(f27917,plain,
( ~ sQ695_spl
| sQ689_spl
| sQ688_spl ),
inference(split_clause,[status(thm)],[f27915,f27783,f27796,f27894]) ).
fof(f27918,plain,
( ~ sQ687_spl
| ~ sQ689_spl
| ~ v1_group_3(sK1498_skl,sK1498_skl)
| ~ l1_group_1(sK1498_skl)
| ~ v4_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl) ),
inference(resolution,[status(thm)],[f27797,f27772]) ).
fof(f27931,plain,
( ~ sQ687_spl
| ~ sQ689_spl
| ~ sQ644_spl
| ~ sQ619_spl
| ~ sQ622_spl
| ~ sQ617_spl
| sQ615_spl ),
inference(split_clause,[status(thm)],[f27918,f27144,f27165,f27195,f27176,f27374,f27796,f27771]) ).
fof(f27949,plain,
( sQ695_spl
| ~ m1_group_2(sK1499_skl,sK1498_skl)
| ~ l1_group_1(sK1499_skl)
| ~ v3_group_1(sK1499_skl)
| ~ l1_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl) ),
inference(resolution,[status(thm)],[f27896,f27227]) ).
fof(f27950,plain,
( sQ695_spl
| ~ sQ689_spl
| ~ sQ618_spl
| ~ sQ616_spl
| ~ sQ619_spl
| ~ sQ617_spl
| sQ615_spl ),
inference(split_clause,[status(thm)],[f27949,f27144,f27165,f27176,f27161,f27172,f27796,f27894]) ).
fof(f27960,plain,
( r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1498_skl)
| ~ m1_group_2(sK1498_skl,sK1495_skl)
| ~ l1_group_1(sK1495_skl)
| ~ v4_group_1(sK1495_skl)
| ~ v3_group_1(sK1495_skl)
| v3_struct_0(sK1495_skl) ),
inference(resolution,[status(thm)],[f27864,f22138]) ).
fof(f27962,plain,
( sQ696_spl
| ~ sQ632_spl
| ~ sQ613_spl
| ~ sQ620_spl
| ~ sQ612_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f27960,f27131,f27134,f27188,f27137,f27252,f27898]) ).
fof(f27963,plain,
! [X0] :
( ~ sQ693_spl
| ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| v3_struct_0(sK1498_skl)
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1498_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ),
inference(resolution,[status(thm)],[f27860,f27227]) ).
fof(f27965,definition,
! [X0] :
( sQ701_spl
<=> ( ~ m1_group_2(X0,sK1498_skl)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| r3_lattices(k11_group_4(sK1495_skl),X0,sK1498_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK1495_skl)))
| ~ m1_group_2(X0,sK1495_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ701_spl])],[split_symbol_definition]) ).
fof(f27968,plain,
( ~ sQ693_spl
| ~ sQ619_spl
| ~ sQ617_spl
| sQ615_spl
| sQ701_spl ),
inference(split_clause,[status(thm)],[f27963,f27965,f27144,f27165,f27176,f27859]) ).
fof(f27971,plain,
( ~ sQ698_spl
| ~ m1_group_2(sK1498_skl,sK1499_skl)
| ~ l1_group_1(sK1498_skl)
| ~ v3_group_1(sK1498_skl)
| r3_lattices(k11_group_4(sK1495_skl),sK1498_skl,sK1499_skl)
| ~ m1_group_2(sK1498_skl,sK1495_skl) ),
inference(resolution,[status(thm)],[f27908,f22138]) ).
fof(f27973,plain,
( ~ sQ698_spl
| ~ sQ633_spl
| ~ sQ619_spl
| ~ sQ617_spl
| sQ450_spl
| ~ sQ632_spl ),
inference(split_clause,[status(thm)],[f27971,f27252,f25241,f27165,f27176,f27259,f27907]) ).
fof(f27974,plain,
$false,
inference(sat_refutation,[status(thm)],[f23600,f23604,f25247,f25248,f27143,f27147,f27149,f27151,f27153,f27164,f27168,f27175,f27179,f27181,f27194,f27198,f27200,f27221,f27235,f27239,f27250,f27255,f27262,f27266,f27299,f27303,f27316,f27320,f27377,f27384,f27390,f27391,f27418,f27445,f27449,f27453,f27457,f27461,f27472,f27476,f27480,f27484,f27488,f27501,f27505,f27547,f27551,f27578,f27582,f27586,f27590,f27594,f27600,f27604,f27617,f27621,f27625,f27629,f27633,f27646,f27651,f27655,f27659,f27663,f27681,f27685,f27689,f27725,f27729,f27750,f27754,f27786,f27791,f27792,f27800,f27858,f27862,f27897,f27904,f27910,f27911,f27913,f27917,f27931,f27950,f27962,f27968,f27973]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP648+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n001.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sun Sep 20 20:32:15 UTC 2026
% 0.19/0.44 % CPUTime :
% 1.16/1.41 % Drodi V4.1.1
% 1.23/1.77 % Refutation found
% 1.23/1.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.23/1.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.27/2.00 % Elapsed time: 1.525237 seconds
% 1.27/2.00 % CPU time: 4.013659 seconds
% 1.27/2.00 % Total memory used: 993.846 MB
% 1.27/2.00 % Net memory used: 986.335 MB
%------------------------------------------------------------------------------