%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP648+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 11.84s 14.63s
% Output : CNFRefutation 11.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 109
% Syntax : Number of formulae : 418 ( 30 unt; 84 def)
% Number of atoms : 2609 ( 29 equ)
% Maximal formula atoms : 17 ( 6 avg)
% Number of connectives : 3882 (1691 ~;1896 |; 147 &)
% ( 92 <=>; 55 =>; 0 <=; 1 <~>)
% Maximal formula depth : 20 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 120 ( 118 usr; 85 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-3 aty)
% Number of variables : 479 ( 466 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [A,B] : r1_tarski(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
? [A] : ~ v1_xboole_0(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f558,axiom,
! [A,B] :
( ( ~ v1_xboole_0(B)
& ~ v1_xboole_0(A) )
=> ~ r1_subset_1(A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f561,axiom,
! [A,B] :
( ( ~ v1_xboole_0(B)
& ~ v1_xboole_0(A) )
=> ~ r2_subset_1(A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f680,axiom,
? [A] :
( v1_relat_1(A)
& v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1176,axiom,
? [A] :
( v3_ordinal1(A)
& v2_ordinal1(A)
& v1_ordinal1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1251,axiom,
! [A,B] :
( ( v3_ordinal1(B)
& v3_ordinal1(A) )
=> r1_ordinal1(A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4814,axiom,
! [A,B] :
( ( ~ v1_xboole_0(B)
& ~ v1_xboole_0(A) )
=> r2_zfrefle1(A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4815,axiom,
! [A,B] :
( ( ~ v1_xboole_0(B)
& ~ v1_xboole_0(A) )
=> r3_zfrefle1(A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4816,axiom,
! [A,B] :
( ( v3_ordinal1(B)
& v3_ordinal1(A) )
=> r4_zfrefle1(A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5990,axiom,
! [A,B] :
( ( v1_relat_1(B)
& v1_relat_1(A) )
=> r1_rfinseq(A,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8697,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/sandbox/benchmark/theBenchmark.p') ).
fof(f8746,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/sandbox/benchmark/theBenchmark.p') ).
fof(f8765,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/sandbox/benchmark/theBenchmark.p') ).
fof(f8767,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/sandbox/benchmark/theBenchmark.p') ).
fof(f8768,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/sandbox/benchmark/theBenchmark.p') ).
fof(f8898,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/sandbox/benchmark/theBenchmark.p') ).
fof(f9466,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/sandbox/benchmark/theBenchmark.p') ).
fof(f11106,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/sandbox/benchmark/theBenchmark.p') ).
fof(f11108,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/sandbox/benchmark/theBenchmark.p') ).
fof(f11205,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/sandbox/benchmark/theBenchmark.p') ).
fof(f11207,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/sandbox/benchmark/theBenchmark.p') ).
fof(f13994,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/sandbox/benchmark/theBenchmark.p') ).
fof(f13995,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/sandbox/benchmark/theBenchmark.p') ).
fof(f13996,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/sandbox/benchmark/theBenchmark.p') ).
fof(f13997,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)],[f13996]) ).
fof(f14073,plain,
! [A] : r1_tarski(A,A),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f14074,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[status(thm)],[f14073]) ).
fof(f14079,plain,
~ v1_xboole_0(sK21_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(A,sK21_skl)],[f26]) ).
fof(f14080,plain,
~ v1_xboole_0(sK21_skl),
inference(cnf_transformation,[status(thm)],[f14079]) ).
fof(f15185,plain,
! [A,B] :
( ~ r1_subset_1(A,A)
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f558]) ).
fof(f15186,plain,
! [A] :
( ~ r1_subset_1(A,A)
| ! [B] : v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(miniscoping,[status(thm)],[f15185]) ).
fof(f15187,plain,
! [X0,X1] :
( ~ r1_subset_1(X0,X0)
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f15186]) ).
fof(f15194,plain,
! [A,B] :
( ~ r2_subset_1(A,A)
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f561]) ).
fof(f15195,plain,
! [A] :
( ~ r2_subset_1(A,A)
| ! [B] : v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(miniscoping,[status(thm)],[f15194]) ).
fof(f15196,plain,
! [X0,X1] :
( ~ r2_subset_1(X0,X0)
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f15195]) ).
fof(f15474,plain,
( v1_relat_1(sK124_skl)
& v1_xboole_0(sK124_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK124_skl]),skolemize(A,sK124_skl)],[f680]) ).
fof(f15476,plain,
v1_relat_1(sK124_skl),
inference(cnf_transformation,[status(thm)],[f15474]) ).
fof(f16819,plain,
( v3_ordinal1(sK240_skl)
& v2_ordinal1(sK240_skl)
& v1_ordinal1(sK240_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK240_skl]),skolemize(A,sK240_skl)],[f1176]) ).
fof(f16822,plain,
v3_ordinal1(sK240_skl),
inference(cnf_transformation,[status(thm)],[f16819]) ).
fof(f17063,plain,
! [A,B] :
( r1_ordinal1(A,A)
| ~ v3_ordinal1(B)
| ~ v3_ordinal1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1251]) ).
fof(f17064,plain,
! [A] :
( r1_ordinal1(A,A)
| ! [B] : ~ v3_ordinal1(B)
| ~ v3_ordinal1(A) ),
inference(miniscoping,[status(thm)],[f17063]) ).
fof(f17065,plain,
! [X0,X1] :
( r1_ordinal1(X0,X0)
| ~ v3_ordinal1(X1)
| ~ v3_ordinal1(X0) ),
inference(cnf_transformation,[status(thm)],[f17064]) ).
fof(f28265,plain,
! [A,B] :
( r2_zfrefle1(A,A)
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4814]) ).
fof(f28266,plain,
! [A] :
( r2_zfrefle1(A,A)
| ! [B] : v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(miniscoping,[status(thm)],[f28265]) ).
fof(f28267,plain,
! [X0,X1] :
( r2_zfrefle1(X0,X0)
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f28266]) ).
fof(f28268,plain,
! [A,B] :
( r3_zfrefle1(A,A)
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4815]) ).
fof(f28269,plain,
! [A] :
( r3_zfrefle1(A,A)
| ! [B] : v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(miniscoping,[status(thm)],[f28268]) ).
fof(f28270,plain,
! [X0,X1] :
( r3_zfrefle1(X0,X0)
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f28269]) ).
fof(f28271,plain,
! [A,B] :
( r4_zfrefle1(A,A)
| ~ v3_ordinal1(B)
| ~ v3_ordinal1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4816]) ).
fof(f28272,plain,
! [A] :
( r4_zfrefle1(A,A)
| ! [B] : ~ v3_ordinal1(B)
| ~ v3_ordinal1(A) ),
inference(miniscoping,[status(thm)],[f28271]) ).
fof(f28273,plain,
! [X0,X1] :
( r4_zfrefle1(X0,X0)
| ~ v3_ordinal1(X1)
| ~ v3_ordinal1(X0) ),
inference(cnf_transformation,[status(thm)],[f28272]) ).
fof(f32058,plain,
! [A,B] :
( r1_rfinseq(A,A)
| ~ v1_relat_1(B)
| ~ v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5990]) ).
fof(f32059,plain,
! [A] :
( r1_rfinseq(A,A)
| ! [B] : ~ v1_relat_1(B)
| ~ v1_relat_1(A) ),
inference(miniscoping,[status(thm)],[f32058]) ).
fof(f32060,plain,
! [X0,X1] :
( r1_rfinseq(X0,X0)
| ~ v1_relat_1(X1)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f32059]) ).
fof(f40195,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)],[f8697]) ).
fof(f40196,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)],[f40195]) ).
fof(f40336,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)],[f8746]) ).
fof(f40337,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)],[f40336]) ).
fof(f40338,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)],[f40337]) ).
fof(f40378,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)],[f8765]) ).
fof(f40379,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)],[f40378]) ).
fof(f40382,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)],[f8767]) ).
fof(f40383,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)],[f40382]) ).
fof(f40384,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)],[f8768]) ).
fof(f40385,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)],[f40384]) ).
fof(f40743,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)],[f8898]) ).
fof(f40744,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)],[f40743]) ).
fof(f40745,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)],[f40743]) ).
fof(f40746,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)],[f40743]) ).
fof(f42533,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)],[f9466]) ).
fof(f42534,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)],[f42533]) ).
fof(f47724,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)],[f11106]) ).
fof(f47725,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)],[f47724]) ).
fof(f47729,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)],[f11108]) ).
fof(f47731,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)],[f47729]) ).
fof(f47733,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)],[f47729]) ).
fof(f48022,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)],[f11205]) ).
fof(f48023,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)],[f48022]) ).
fof(f48027,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)],[f11207]) ).
fof(f48028,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)],[f48027]) ).
fof(f48029,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)],[f48028]) ).
fof(f48030,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)],[f48029]) ).
fof(f48031,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)],[f48029]) ).
fof(f59613,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)],[f13994]) ).
fof(f59614,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)],[f59613]) ).
fof(f59616,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)],[f13995]) ).
fof(f59617,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)],[f59616]) ).
fof(f59618,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)],[f59617]) ).
fof(f59619,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)],[f59617]) ).
fof(f59620,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)],[f13997]) ).
fof(f59621,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)],[f59620]) ).
fof(f59622,plain,
( ( ~ m1_group_6(sK4180_skl,sK4179_skl,sK4181_skl)
| ~ r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4183_skl) )
& ( m1_group_6(sK4180_skl,sK4179_skl,sK4181_skl)
| r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4183_skl) )
& sK4183_skl = sK4181_skl
& sK4182_skl = sK4180_skl
& m1_subset_1(sK4183_skl,u1_struct_0(k11_group_4(sK4179_skl)))
& m1_subset_1(sK4182_skl,u1_struct_0(k11_group_4(sK4179_skl)))
& m1_group_2(sK4181_skl,sK4179_skl)
& m1_group_2(sK4180_skl,sK4179_skl)
& l1_group_1(sK4179_skl)
& v4_group_1(sK4179_skl)
& v3_group_1(sK4179_skl)
& ~ v3_struct_0(sK4179_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4179_skl,sK4180_skl,sK4181_skl,sK4182_skl,sK4183_skl]),skolemize(A,sK4179_skl),skolemize(B,sK4180_skl),skolemize(C,sK4181_skl),skolemize(D,sK4182_skl),skolemize(E,sK4183_skl)],[f59621]) ).
fof(f59623,plain,
~ v3_struct_0(sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59624,plain,
v3_group_1(sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59625,plain,
v4_group_1(sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59626,plain,
l1_group_1(sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59627,plain,
m1_group_2(sK4180_skl,sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59628,plain,
m1_group_2(sK4181_skl,sK4179_skl),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59629,plain,
m1_subset_1(sK4182_skl,u1_struct_0(k11_group_4(sK4179_skl))),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59630,plain,
m1_subset_1(sK4183_skl,u1_struct_0(k11_group_4(sK4179_skl))),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59631,plain,
sK4182_skl = sK4180_skl,
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59632,plain,
sK4183_skl = sK4181_skl,
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59633,plain,
( m1_group_6(sK4180_skl,sK4179_skl,sK4181_skl)
| r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4183_skl) ),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f59634,plain,
( ~ m1_group_6(sK4180_skl,sK4179_skl,sK4181_skl)
| ~ r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4183_skl) ),
inference(cnf_transformation,[status(thm)],[f59622]) ).
fof(f62972,definition,
! [X0] :
( sQ13_spl
<=> ( ~ r1_subset_1(X0,X0)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f62975,definition,
! [X1] :
( sQ14_spl
<=> v1_xboole_0(X1) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f62976,plain,
! [X0] :
( ~ sQ14_spl
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f62975]) ).
fof(f62978,plain,
( sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f15187,f62972,f62975]) ).
fof(f62979,definition,
! [X0] :
( sQ15_spl
<=> ( ~ r2_subset_1(X0,X0)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f62982,plain,
( sQ14_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f15196,f62979,f62975]) ).
fof(f63113,definition,
! [X0] :
( sQ51_spl
<=> ( r1_ordinal1(X0,X0)
| ~ v3_ordinal1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f63116,definition,
! [X1] :
( sQ52_spl
<=> ~ v3_ordinal1(X1) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f63117,plain,
! [X0] :
( ~ sQ52_spl
| ~ v3_ordinal1(X0) ),
inference(component_clause,[status(thm)],[f63116]) ).
fof(f63119,plain,
( sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f17065,f63113,f63116]) ).
fof(f64965,definition,
! [X0] :
( sQ539_spl
<=> ( r2_zfrefle1(X0,X0)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ539_spl])],[split_symbol_definition]) ).
fof(f64968,plain,
( sQ14_spl
| sQ539_spl ),
inference(split_clause,[status(thm)],[f28267,f64965,f62975]) ).
fof(f64969,definition,
! [X0] :
( sQ540_spl
<=> ( r3_zfrefle1(X0,X0)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ540_spl])],[split_symbol_definition]) ).
fof(f64972,plain,
( sQ14_spl
| sQ540_spl ),
inference(split_clause,[status(thm)],[f28270,f64969,f62975]) ).
fof(f64973,definition,
! [X0] :
( sQ541_spl
<=> ( r4_zfrefle1(X0,X0)
| ~ v3_ordinal1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ541_spl])],[split_symbol_definition]) ).
fof(f64976,plain,
( sQ52_spl
| sQ541_spl ),
inference(split_clause,[status(thm)],[f28273,f64973,f63116]) ).
fof(f65764,definition,
! [X0] :
( sQ748_spl
<=> ( r1_rfinseq(X0,X0)
| ~ v1_relat_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ748_spl])],[split_symbol_definition]) ).
fof(f65767,definition,
! [X1] :
( sQ749_spl
<=> ~ v1_relat_1(X1) ),
introduced(definition,[new_symbols(definition,[sQ749_spl])],[split_symbol_definition]) ).
fof(f65768,plain,
! [X0] :
( ~ sQ749_spl
| ~ v1_relat_1(X0) ),
inference(component_clause,[status(thm)],[f65767]) ).
fof(f65770,plain,
( sQ749_spl
| sQ748_spl ),
inference(split_clause,[status(thm)],[f32060,f65764,f65767]) ).
fof(f66628,definition,
( sQ977_spl
<=> r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ977_spl])],[split_symbol_definition]) ).
fof(f66631,definition,
( sQ978_spl
<=> m1_group_6(sK4180_skl,sK4179_skl,sK4181_skl) ),
introduced(definition,[new_symbols(definition,[sQ978_spl])],[split_symbol_definition]) ).
fof(f66632,plain,
( ~ sQ978_spl
| m1_group_6(sK4180_skl,sK4179_skl,sK4181_skl) ),
inference(component_clause,[status(thm)],[f66631]) ).
fof(f66633,plain,
( sQ978_spl
| ~ m1_group_6(sK4180_skl,sK4179_skl,sK4181_skl) ),
inference(component_clause,[status(thm)],[f66631]) ).
fof(f66634,plain,
( sQ978_spl
| sQ977_spl ),
inference(split_clause,[status(thm)],[f59633,f66628,f66631]) ).
fof(f66635,plain,
( ~ sQ978_spl
| ~ sQ977_spl ),
inference(split_clause,[status(thm)],[f59634,f66628,f66631]) ).
fof(f70520,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)],[f59614]) ).
fof(f70521,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)],[f59618]) ).
fof(f70522,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)],[f59619]) ).
fof(f70838,plain,
m1_group_2(sK4182_skl,sK4179_skl),
inference(forward_demodulation,[status(thm)],[f59631,f59627]) ).
fof(f70839,plain,
m1_group_2(sK4183_skl,sK4179_skl),
inference(forward_demodulation,[status(thm)],[f59632,f59628]) ).
fof(f70840,plain,
( ~ sQ978_spl
| m1_group_6(sK4182_skl,sK4179_skl,sK4181_skl) ),
inference(forward_demodulation,[status(thm)],[f59631,f66632]) ).
fof(f70841,plain,
( ~ sQ978_spl
| m1_group_6(sK4182_skl,sK4179_skl,sK4183_skl) ),
inference(forward_demodulation,[status(thm)],[f59632,f70840]) ).
fof(f70842,plain,
( ~ v3_struct_0(sK4183_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f40744,f70839]) ).
fof(f70843,plain,
( ~ v3_struct_0(sK4182_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f40744,f70838]) ).
fof(f70845,definition,
( sQ1248_spl
<=> v3_struct_0(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1248_spl])],[split_symbol_definition]) ).
fof(f70846,plain,
( ~ sQ1248_spl
| v3_struct_0(sK4179_skl) ),
inference(component_clause,[status(thm)],[f70845]) ).
fof(f70848,definition,
( sQ1249_spl
<=> v3_group_1(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1249_spl])],[split_symbol_definition]) ).
fof(f70850,plain,
( sQ1249_spl
| ~ v3_group_1(sK4179_skl) ),
inference(component_clause,[status(thm)],[f70848]) ).
fof(f70851,definition,
( sQ1250_spl
<=> l1_group_1(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1250_spl])],[split_symbol_definition]) ).
fof(f70853,plain,
( sQ1250_spl
| ~ l1_group_1(sK4179_skl) ),
inference(component_clause,[status(thm)],[f70851]) ).
fof(f70854,definition,
( sQ1251_spl
<=> v3_struct_0(sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ1251_spl])],[split_symbol_definition]) ).
fof(f70857,plain,
( ~ sQ1251_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70842,f70845,f70848,f70851,f70854]) ).
fof(f70858,definition,
( sQ1252_spl
<=> v3_struct_0(sK4182_skl) ),
introduced(definition,[new_symbols(definition,[sQ1252_spl])],[split_symbol_definition]) ).
fof(f70861,plain,
( ~ sQ1252_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70843,f70845,f70848,f70851,f70858]) ).
fof(f70862,plain,
( sQ1250_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f70853,f59626]) ).
fof(f70863,plain,
sQ1250_spl,
inference(contradiction_clause,[status(thm)],[f70862]) ).
fof(f70864,plain,
( sQ1249_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f70850,f59624]) ).
fof(f70865,plain,
sQ1249_spl,
inference(contradiction_clause,[status(thm)],[f70864]) ).
fof(f70866,plain,
( ~ sQ1248_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f70846,f59623]) ).
fof(f70867,plain,
~ sQ1248_spl,
inference(contradiction_clause,[status(thm)],[f70866]) ).
fof(f70868,plain,
( sQ978_spl
| ~ m1_group_6(sK4182_skl,sK4179_skl,sK4181_skl) ),
inference(forward_demodulation,[status(thm)],[f59631,f66633]) ).
fof(f70869,plain,
( sQ978_spl
| ~ m1_group_6(sK4182_skl,sK4179_skl,sK4183_skl) ),
inference(forward_demodulation,[status(thm)],[f59632,f70868]) ).
fof(f70870,plain,
( v4_group_1(sK4183_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f40196,f70839]) ).
fof(f70871,plain,
( v4_group_1(sK4182_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f40196,f70838]) ).
fof(f70873,definition,
( sQ1253_spl
<=> v4_group_1(sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1253_spl])],[split_symbol_definition]) ).
fof(f70875,plain,
( sQ1253_spl
| ~ v4_group_1(sK4179_skl) ),
inference(component_clause,[status(thm)],[f70873]) ).
fof(f70876,definition,
( sQ1254_spl
<=> v4_group_1(sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ1254_spl])],[split_symbol_definition]) ).
fof(f70879,plain,
( sQ1254_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70870,f70845,f70848,f70873,f70851,f70876]) ).
fof(f70880,definition,
( sQ1255_spl
<=> v4_group_1(sK4182_skl) ),
introduced(definition,[new_symbols(definition,[sQ1255_spl])],[split_symbol_definition]) ).
fof(f70883,plain,
( sQ1255_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70871,f70845,f70848,f70873,f70851,f70880]) ).
fof(f70884,plain,
( sQ1253_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f70875,f59625]) ).
fof(f70885,plain,
sQ1253_spl,
inference(contradiction_clause,[status(thm)],[f70884]) ).
fof(f70886,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)],[f40338,f40744]) ).
fof(f70889,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f70886,f40745]) ).
fof(f70890,plain,
( v3_group_1(sK4183_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f40745,f70839]) ).
fof(f70891,plain,
( v3_group_1(sK4182_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f40745,f70838]) ).
fof(f70893,definition,
( sQ1256_spl
<=> v3_group_1(sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ1256_spl])],[split_symbol_definition]) ).
fof(f70896,plain,
( sQ1256_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70890,f70845,f70848,f70851,f70893]) ).
fof(f70897,definition,
( sQ1257_spl
<=> v3_group_1(sK4182_skl) ),
introduced(definition,[new_symbols(definition,[sQ1257_spl])],[split_symbol_definition]) ).
fof(f70900,plain,
( sQ1257_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70891,f70845,f70848,f70851,f70897]) ).
fof(f70901,plain,
( l1_group_1(sK4183_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f40746,f70839]) ).
fof(f70902,plain,
( l1_group_1(sK4182_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f40746,f70838]) ).
fof(f70904,definition,
( sQ1258_spl
<=> l1_group_1(sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ1258_spl])],[split_symbol_definition]) ).
fof(f70907,plain,
( sQ1258_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70901,f70845,f70848,f70851,f70904]) ).
fof(f70908,definition,
( sQ1259_spl
<=> l1_group_1(sK4182_skl) ),
introduced(definition,[new_symbols(definition,[sQ1259_spl])],[split_symbol_definition]) ).
fof(f70911,plain,
( sQ1259_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70902,f70845,f70848,f70851,f70908]) ).
fof(f70914,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)],[f40383,f40744]) ).
fof(f70915,plain,
! [X0] :
( m1_group_2(X0,sK4179_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(resolution,[status(thm)],[f70914,f70839]) ).
fof(f70916,plain,
! [X0] :
( m1_group_2(X0,sK4179_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(sK4182_skl)
| ~ v4_group_1(sK4182_skl)
| ~ v3_group_1(sK4182_skl)
| v3_struct_0(sK4182_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(resolution,[status(thm)],[f70914,f70838]) ).
fof(f70918,definition,
! [X0] :
( sQ1260_spl
<=> ( m1_group_2(X0,sK4179_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1260_spl])],[split_symbol_definition]) ).
fof(f70919,plain,
! [X0] :
( ~ sQ1260_spl
| m1_group_2(X0,sK4179_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(component_clause,[status(thm)],[f70918]) ).
fof(f70921,plain,
( ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| ~ sQ1258_spl
| ~ sQ1254_spl
| ~ sQ1256_spl
| sQ1251_spl
| sQ1260_spl ),
inference(split_clause,[status(thm)],[f70915,f70918,f70854,f70893,f70876,f70904,f70845,f70848,f70873,f70851]) ).
fof(f70922,definition,
! [X0] :
( sQ1261_spl
<=> ( m1_group_2(X0,sK4179_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1261_spl])],[split_symbol_definition]) ).
fof(f70923,plain,
! [X0] :
( ~ sQ1261_spl
| m1_group_2(X0,sK4179_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(component_clause,[status(thm)],[f70922]) ).
fof(f70925,plain,
( ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| ~ sQ1259_spl
| ~ sQ1255_spl
| ~ sQ1257_spl
| sQ1252_spl
| sQ1261_spl ),
inference(split_clause,[status(thm)],[f70916,f70922,f70858,f70897,f70880,f70908,f70845,f70848,f70873,f70851]) ).
fof(f70929,plain,
( ~ sQ1260_spl
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl)
| m1_group_2(sK4183_skl,sK4179_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl) ),
inference(resolution,[status(thm)],[f70919,f40379]) ).
fof(f70930,definition,
( sQ1262_spl
<=> m1_group_2(sK4183_skl,sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1262_spl])],[split_symbol_definition]) ).
fof(f70933,plain,
( ~ sQ1260_spl
| sQ1251_spl
| sQ1262_spl
| ~ sQ1258_spl
| ~ sQ1254_spl
| ~ sQ1256_spl ),
inference(split_clause,[status(thm)],[f70929,f70893,f70876,f70904,f70930,f70854,f70918]) ).
fof(f70934,plain,
( ~ sQ1261_spl
| ~ l1_group_1(sK4182_skl)
| ~ v4_group_1(sK4182_skl)
| ~ v3_group_1(sK4182_skl)
| v3_struct_0(sK4182_skl)
| m1_group_2(sK4182_skl,sK4179_skl)
| ~ l1_group_1(sK4182_skl)
| ~ v4_group_1(sK4182_skl)
| ~ v3_group_1(sK4182_skl) ),
inference(resolution,[status(thm)],[f70923,f40379]) ).
fof(f70935,definition,
( sQ1263_spl
<=> m1_group_2(sK4182_skl,sK4179_skl) ),
introduced(definition,[new_symbols(definition,[sQ1263_spl])],[split_symbol_definition]) ).
fof(f70938,plain,
( ~ sQ1261_spl
| sQ1252_spl
| sQ1263_spl
| ~ sQ1259_spl
| ~ sQ1255_spl
| ~ sQ1257_spl ),
inference(split_clause,[status(thm)],[f70934,f70897,f70880,f70908,f70935,f70858,f70922]) ).
fof(f70940,definition,
( sQ1264_spl
<=> v3_struct_0(k11_group_4(sK4179_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1264_spl])],[split_symbol_definition]) ).
fof(f70941,plain,
( ~ sQ1264_spl
| v3_struct_0(k11_group_4(sK4179_skl)) ),
inference(component_clause,[status(thm)],[f70940]) ).
fof(f70949,definition,
( sQ1267_spl
<=> m1_subset_1(sK4183_skl,u1_struct_0(k11_group_4(sK4179_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1267_spl])],[split_symbol_definition]) ).
fof(f70951,plain,
( sQ1267_spl
| ~ m1_subset_1(sK4183_skl,u1_struct_0(k11_group_4(sK4179_skl))) ),
inference(component_clause,[status(thm)],[f70949]) ).
fof(f70957,definition,
( sQ1269_spl
<=> m1_subset_1(sK4182_skl,u1_struct_0(k11_group_4(sK4179_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1269_spl])],[split_symbol_definition]) ).
fof(f70959,plain,
( sQ1269_spl
| ~ m1_subset_1(sK4182_skl,u1_struct_0(k11_group_4(sK4179_skl))) ),
inference(component_clause,[status(thm)],[f70957]) ).
fof(f70961,plain,
( ~ sQ1264_spl
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70941,f42534]) ).
fof(f70962,plain,
( ~ sQ1264_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70961,f70845,f70848,f70873,f70851,f70940]) ).
fof(f70963,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)],[f14074,f40385]) ).
fof(f70964,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)],[f70963]) ).
fof(f70965,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14080,f62976]) ).
fof(f70966,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f70965]) ).
fof(f70973,plain,
( m1_group_2(sK4183_skl,sK4183_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70964,f70839]) ).
fof(f70974,plain,
( m1_group_2(sK4182_skl,sK4182_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70964,f70838]) ).
fof(f70976,definition,
( sQ1270_spl
<=> m1_group_2(sK4183_skl,sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ1270_spl])],[split_symbol_definition]) ).
fof(f70977,plain,
( ~ sQ1270_spl
| m1_group_2(sK4183_skl,sK4183_skl) ),
inference(component_clause,[status(thm)],[f70976]) ).
fof(f70979,plain,
( sQ1270_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70973,f70845,f70848,f70873,f70851,f70976]) ).
fof(f70980,definition,
( sQ1271_spl
<=> m1_group_2(sK4182_skl,sK4182_skl) ),
introduced(definition,[new_symbols(definition,[sQ1271_spl])],[split_symbol_definition]) ).
fof(f70981,plain,
( ~ sQ1271_spl
| m1_group_2(sK4182_skl,sK4182_skl) ),
inference(component_clause,[status(thm)],[f70980]) ).
fof(f70983,plain,
( sQ1271_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f70974,f70845,f70848,f70873,f70851,f70980]) ).
fof(f70987,plain,
! [X0] :
( ~ sQ1270_spl
| m1_group_2(X0,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(resolution,[status(thm)],[f70977,f70914]) ).
fof(f70994,definition,
! [X0] :
( sQ1272_spl
<=> ( m1_group_2(X0,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1272_spl])],[split_symbol_definition]) ).
fof(f70997,plain,
( ~ sQ1270_spl
| ~ sQ1258_spl
| ~ sQ1254_spl
| ~ sQ1256_spl
| sQ1251_spl
| sQ1272_spl ),
inference(split_clause,[status(thm)],[f70987,f70994,f70854,f70893,f70876,f70904,f70976]) ).
fof(f71004,plain,
! [X0] :
( ~ sQ1271_spl
| m1_group_2(X0,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(sK4182_skl)
| ~ v4_group_1(sK4182_skl)
| ~ v3_group_1(sK4182_skl)
| v3_struct_0(sK4182_skl)
| ~ l1_group_1(sK4182_skl)
| ~ v4_group_1(sK4182_skl)
| ~ v3_group_1(sK4182_skl)
| v3_struct_0(sK4182_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(resolution,[status(thm)],[f70981,f70914]) ).
fof(f71011,definition,
! [X0] :
( sQ1273_spl
<=> ( m1_group_2(X0,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1273_spl])],[split_symbol_definition]) ).
fof(f71014,plain,
( ~ sQ1271_spl
| ~ sQ1259_spl
| ~ sQ1255_spl
| ~ sQ1257_spl
| sQ1252_spl
| sQ1273_spl ),
inference(split_clause,[status(thm)],[f71004,f71011,f70858,f70897,f70880,f70908,f70980]) ).
fof(f71019,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f70889,f40746]) ).
fof(f71021,plain,
( sQ978_spl
| ~ m1_group_2(sK4182_skl,sK4183_skl)
| ~ m1_group_2(sK4183_skl,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f48031,f70869]) ).
fof(f71024,definition,
( sQ1274_spl
<=> m1_group_2(sK4182_skl,sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ1274_spl])],[split_symbol_definition]) ).
fof(f71027,plain,
( sQ978_spl
| ~ sQ1274_spl
| ~ sQ1262_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71021,f70845,f70848,f70873,f70851,f70930,f71024,f66631]) ).
fof(f71029,plain,
( ~ sQ978_spl
| m1_group_2(sK4182_skl,sK4183_skl)
| ~ m1_group_2(sK4183_skl,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70841,f48030]) ).
fof(f71031,plain,
( ~ sQ978_spl
| sQ1274_spl
| ~ sQ1262_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71029,f70845,f70848,f70873,f70851,f70930,f71024,f66631]) ).
fof(f71054,plain,
( ~ sQ749_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15476,f65768]) ).
fof(f71055,plain,
~ sQ749_spl,
inference(contradiction_clause,[status(thm)],[f71054]) ).
fof(f71096,plain,
( v1_group_1(sK4183_skl)
| ~ m1_group_2(sK4183_skl,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70520,f59630]) ).
fof(f71097,plain,
( v1_group_1(sK4182_skl)
| ~ m1_group_2(sK4182_skl,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70520,f59629]) ).
fof(f71098,definition,
( sQ1276_spl
<=> v1_group_1(sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ1276_spl])],[split_symbol_definition]) ).
fof(f71101,plain,
( sQ1276_spl
| ~ sQ1262_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71096,f70845,f70848,f70873,f70851,f70930,f71098]) ).
fof(f71102,definition,
( sQ1277_spl
<=> v1_group_1(sK4182_skl) ),
introduced(definition,[new_symbols(definition,[sQ1277_spl])],[split_symbol_definition]) ).
fof(f71105,plain,
( sQ1277_spl
| ~ sQ1263_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71097,f70845,f70848,f70873,f70851,f70935,f71102]) ).
fof(f71106,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)],[f47725,f48023]) ).
fof(f71108,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)],[f71106,f48031]) ).
fof(f71116,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)],[f71108]) ).
fof(f71118,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)],[f47731,f48030]) ).
fof(f71119,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)],[f47731,f48023]) ).
fof(f71121,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)],[f71118]) ).
fof(f71122,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)],[f71119]) ).
fof(f71125,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)],[f47733,f48023]) ).
fof(f71128,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)],[f71125]) ).
fof(f71147,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)],[f71116,f40379]) ).
fof(f71177,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)],[f71147,f40744]) ).
fof(f71211,plain,
! [X0,X1] :
( ~ sQ1261_spl
| m1_group_2(k9_group_2(X0,sK4182_skl,X1),sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71121,f70923]) ).
fof(f71212,plain,
! [X0,X1] :
( ~ sQ1260_spl
| m1_group_2(k9_group_2(X0,sK4183_skl,X1),sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71121,f70919]) ).
fof(f71227,plain,
( ~ sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16822,f63117]) ).
fof(f71228,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f71227]) ).
fof(f71246,definition,
! [X0,X1] :
( sQ1288_spl
<=> ( m1_group_2(k9_group_2(X0,sK4182_skl,X1),k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1288_spl])],[split_symbol_definition]) ).
fof(f71250,definition,
! [X0,X1] :
( sQ1289_spl
<=> ( l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1289_spl])],[split_symbol_definition]) ).
fof(f71254,definition,
! [X0,X1] :
( sQ1290_spl
<=> ( v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1290_spl])],[split_symbol_definition]) ).
fof(f71258,definition,
! [X0,X1] :
( sQ1291_spl
<=> ( v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1291_spl])],[split_symbol_definition]) ).
fof(f71262,definition,
! [X0,X1] :
( sQ1292_spl
<=> ( ~ v3_struct_0(k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1292_spl])],[split_symbol_definition]) ).
fof(f71268,plain,
! [X0,X1] :
( ~ sQ1261_spl
| m1_group_2(k9_group_2(X0,sK4182_skl,X1),k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71211,f70964]) ).
fof(f71269,plain,
! [X0,X1] :
( ~ sQ1261_spl
| l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71211,f40746]) ).
fof(f71270,plain,
! [X0,X1] :
( ~ sQ1261_spl
| v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71211,f40745]) ).
fof(f71271,plain,
! [X0,X1] :
( ~ sQ1261_spl
| v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71211,f40196]) ).
fof(f71272,plain,
! [X0,X1] :
( ~ sQ1261_spl
| ~ v3_struct_0(k9_group_2(X0,sK4182_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4182_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71211,f40744]) ).
fof(f71273,plain,
( ~ sQ1261_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1288_spl ),
inference(split_clause,[status(thm)],[f71268,f71246,f70845,f70848,f70873,f70851,f70922]) ).
fof(f71274,plain,
( ~ sQ1261_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1289_spl ),
inference(split_clause,[status(thm)],[f71269,f71250,f70845,f70848,f70851,f70922]) ).
fof(f71275,plain,
( ~ sQ1261_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1290_spl ),
inference(split_clause,[status(thm)],[f71270,f71254,f70845,f70848,f70851,f70922]) ).
fof(f71276,plain,
( ~ sQ1261_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1291_spl ),
inference(split_clause,[status(thm)],[f71271,f71258,f70845,f70848,f70873,f70851,f70922]) ).
fof(f71277,plain,
( ~ sQ1261_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1292_spl ),
inference(split_clause,[status(thm)],[f71272,f71262,f70845,f70848,f70851,f70922]) ).
fof(f71280,plain,
! [X0,X1] :
( ~ sQ1260_spl
| m1_group_2(k9_group_2(X0,sK4183_skl,X1),k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71212,f70964]) ).
fof(f71281,plain,
! [X0,X1] :
( ~ sQ1260_spl
| l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71212,f40746]) ).
fof(f71282,plain,
! [X0,X1] :
( ~ sQ1260_spl
| v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71212,f40745]) ).
fof(f71283,plain,
! [X0,X1] :
( ~ sQ1260_spl
| v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71212,f40196]) ).
fof(f71284,plain,
! [X0,X1] :
( ~ sQ1260_spl
| ~ v3_struct_0(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71212,f40744]) ).
fof(f71285,definition,
! [X0,X1] :
( sQ1293_spl
<=> ( m1_group_2(k9_group_2(X0,sK4183_skl,X1),k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1293_spl])],[split_symbol_definition]) ).
fof(f71288,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1293_spl ),
inference(split_clause,[status(thm)],[f71280,f71285,f70845,f70848,f70873,f70851,f70918]) ).
fof(f71289,definition,
! [X0,X1] :
( sQ1294_spl
<=> ( l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1294_spl])],[split_symbol_definition]) ).
fof(f71292,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1294_spl ),
inference(split_clause,[status(thm)],[f71281,f71289,f70845,f70848,f70851,f70918]) ).
fof(f71293,definition,
! [X0,X1] :
( sQ1295_spl
<=> ( v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1295_spl])],[split_symbol_definition]) ).
fof(f71296,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1295_spl ),
inference(split_clause,[status(thm)],[f71282,f71293,f70845,f70848,f70851,f70918]) ).
fof(f71297,definition,
! [X0,X1] :
( sQ1296_spl
<=> ( v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1296_spl])],[split_symbol_definition]) ).
fof(f71300,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1296_spl ),
inference(split_clause,[status(thm)],[f71283,f71297,f70845,f70848,f70873,f70851,f70918]) ).
fof(f71301,definition,
! [X0,X1] :
( sQ1297_spl
<=> ( ~ v3_struct_0(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1297_spl])],[split_symbol_definition]) ).
fof(f71304,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1297_spl ),
inference(split_clause,[status(thm)],[f71284,f71301,f70845,f70848,f70851,f70918]) ).
fof(f71306,plain,
! [X0,X1] :
( ~ sQ1261_spl
| m1_group_2(k9_group_2(sK4182_skl,X0,X1),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(sK4182_skl)
| ~ v4_group_1(sK4182_skl)
| ~ v3_group_1(sK4182_skl)
| v3_struct_0(sK4182_skl) ),
inference(resolution,[status(thm)],[f71122,f70923]) ).
fof(f71307,plain,
! [X0,X1] :
( ~ sQ1260_spl
| m1_group_2(k9_group_2(sK4183_skl,X0,X1),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl) ),
inference(resolution,[status(thm)],[f71122,f70919]) ).
fof(f71311,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)],[f71122,f40746]) ).
fof(f71312,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)],[f71122,f40745]) ).
fof(f71319,definition,
! [X0,X1] :
( sQ1299_spl
<=> ( m1_group_2(k9_group_2(sK4182_skl,X0,X1),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1299_spl])],[split_symbol_definition]) ).
fof(f71320,plain,
! [X0,X1] :
( ~ sQ1299_spl
| m1_group_2(k9_group_2(sK4182_skl,X0,X1),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ),
inference(component_clause,[status(thm)],[f71319]) ).
fof(f71322,plain,
( ~ sQ1261_spl
| sQ1299_spl
| ~ sQ1259_spl
| ~ sQ1255_spl
| ~ sQ1257_spl
| sQ1252_spl ),
inference(split_clause,[status(thm)],[f71306,f70858,f70897,f70880,f70908,f71319,f70922]) ).
fof(f71323,definition,
! [X0,X1] :
( sQ1300_spl
<=> ( m1_group_2(k9_group_2(sK4183_skl,X0,X1),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1300_spl])],[split_symbol_definition]) ).
fof(f71324,plain,
! [X0,X1] :
( ~ sQ1300_spl
| m1_group_2(k9_group_2(sK4183_skl,X0,X1),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(component_clause,[status(thm)],[f71323]) ).
fof(f71326,plain,
( ~ sQ1260_spl
| sQ1300_spl
| ~ sQ1258_spl
| ~ sQ1254_spl
| ~ sQ1256_spl
| sQ1251_spl ),
inference(split_clause,[status(thm)],[f71307,f70854,f70893,f70876,f70904,f71323,f70918]) ).
fof(f71330,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)],[f71311]) ).
fof(f71331,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)],[f71312]) ).
fof(f71334,plain,
! [X0,X1] :
( ~ sQ1260_spl
| m1_group_2(k9_group_2(X0,sK4183_skl,X1),sK4179_skl)
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f71212,f71330]) ).
fof(f71356,plain,
! [X0,X1] :
( ~ sQ1261_spl
| m1_group_2(k9_group_2(sK4182_skl,X1,X0),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X1,X0))
| ~ v4_group_1(k9_group_2(sK4182_skl,X1,X0))
| ~ v3_group_1(k9_group_2(sK4182_skl,X1,X0))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(sK4182_skl)
| ~ v4_group_1(sK4182_skl)
| ~ v3_group_1(sK4182_skl)
| v3_struct_0(sK4182_skl) ),
inference(resolution,[status(thm)],[f71128,f70923]) ).
fof(f71357,plain,
! [X0,X1] :
( ~ sQ1260_spl
| m1_group_2(k9_group_2(sK4183_skl,X1,X0),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X1,X0))
| ~ v4_group_1(k9_group_2(sK4183_skl,X1,X0))
| ~ v3_group_1(k9_group_2(sK4183_skl,X1,X0))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl) ),
inference(resolution,[status(thm)],[f71128,f70919]) ).
fof(f71361,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)],[f71128,f40746]) ).
fof(f71369,definition,
! [X0,X1] :
( sQ1302_spl
<=> ( m1_group_2(k9_group_2(sK4182_skl,X1,X0),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X1,X0))
| ~ v4_group_1(k9_group_2(sK4182_skl,X1,X0))
| ~ v3_group_1(k9_group_2(sK4182_skl,X1,X0))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1302_spl])],[split_symbol_definition]) ).
fof(f71372,plain,
( ~ sQ1261_spl
| sQ1302_spl
| ~ sQ1259_spl
| ~ sQ1255_spl
| ~ sQ1257_spl
| sQ1252_spl ),
inference(split_clause,[status(thm)],[f71356,f70858,f70897,f70880,f70908,f71369,f70922]) ).
fof(f71373,definition,
! [X0,X1] :
( sQ1303_spl
<=> ( m1_group_2(k9_group_2(sK4183_skl,X1,X0),sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X1,X0))
| ~ v4_group_1(k9_group_2(sK4183_skl,X1,X0))
| ~ v3_group_1(k9_group_2(sK4183_skl,X1,X0))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1303_spl])],[split_symbol_definition]) ).
fof(f71376,plain,
( ~ sQ1260_spl
| sQ1303_spl
| ~ sQ1258_spl
| ~ sQ1254_spl
| ~ sQ1256_spl
| sQ1251_spl ),
inference(split_clause,[status(thm)],[f71357,f70854,f70893,f70876,f70904,f71373,f70918]) ).
fof(f71380,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)],[f71361]) ).
fof(f71398,plain,
! [X0,X1] :
( ~ sQ1300_spl
| m1_group_2(k9_group_2(sK4183_skl,X0,X1),k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(resolution,[status(thm)],[f71324,f70964]) ).
fof(f71399,plain,
! [X0,X1] :
( ~ sQ1300_spl
| l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(resolution,[status(thm)],[f71324,f40746]) ).
fof(f71400,plain,
! [X0,X1] :
( ~ sQ1300_spl
| v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(resolution,[status(thm)],[f71324,f40745]) ).
fof(f71401,plain,
! [X0,X1] :
( ~ sQ1300_spl
| v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(resolution,[status(thm)],[f71324,f40196]) ).
fof(f71402,plain,
! [X0,X1] :
( ~ sQ1300_spl
| ~ v3_struct_0(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(resolution,[status(thm)],[f71324,f40744]) ).
fof(f71403,definition,
! [X0,X1] :
( sQ1304_spl
<=> ( m1_group_2(k9_group_2(sK4183_skl,X0,X1),k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1304_spl])],[split_symbol_definition]) ).
fof(f71406,plain,
( ~ sQ1300_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1304_spl ),
inference(split_clause,[status(thm)],[f71398,f71403,f70845,f70848,f70873,f70851,f71323]) ).
fof(f71407,definition,
! [X0,X1] :
( sQ1305_spl
<=> ( l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1305_spl])],[split_symbol_definition]) ).
fof(f71410,plain,
( ~ sQ1300_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1305_spl ),
inference(split_clause,[status(thm)],[f71399,f71407,f70845,f70848,f70851,f71323]) ).
fof(f71411,definition,
! [X0,X1] :
( sQ1306_spl
<=> ( v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1306_spl])],[split_symbol_definition]) ).
fof(f71414,plain,
( ~ sQ1300_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1306_spl ),
inference(split_clause,[status(thm)],[f71400,f71411,f70845,f70848,f70851,f71323]) ).
fof(f71415,definition,
! [X0,X1] :
( sQ1307_spl
<=> ( v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1307_spl])],[split_symbol_definition]) ).
fof(f71418,plain,
( ~ sQ1300_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1307_spl ),
inference(split_clause,[status(thm)],[f71401,f71415,f70845,f70848,f70873,f70851,f71323]) ).
fof(f71419,definition,
! [X0,X1] :
( sQ1308_spl
<=> ( ~ v3_struct_0(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1308_spl])],[split_symbol_definition]) ).
fof(f71420,plain,
! [X0,X1] :
( ~ sQ1308_spl
| ~ v3_struct_0(k9_group_2(sK4183_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(component_clause,[status(thm)],[f71419]) ).
fof(f71422,plain,
( ~ sQ1300_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1308_spl ),
inference(split_clause,[status(thm)],[f71402,f71419,f70845,f70848,f70851,f71323]) ).
fof(f71423,plain,
! [X0,X1] :
( ~ sQ1308_spl
| ~ m1_group_2(X0,sK4183_skl)
| ~ v1_group_3(X0,sK4183_skl)
| ~ m1_group_2(X1,sK4183_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl)
| ~ v3_struct_0(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(resolution,[status(thm)],[f71420,f71380]) ).
fof(f71424,plain,
! [X0,X1] :
( ~ sQ1308_spl
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v4_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl)
| ~ v3_struct_0(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ),
inference(resolution,[status(thm)],[f71420,f71330]) ).
fof(f71425,definition,
! [X0,X1] :
( sQ1309_spl
<=> ( ~ m1_group_2(X0,sK4183_skl)
| ~ v1_group_3(X0,sK4183_skl)
| ~ m1_group_2(X1,sK4183_skl)
| ~ v3_struct_0(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1309_spl])],[split_symbol_definition]) ).
fof(f71428,plain,
( ~ sQ1308_spl
| ~ sQ1258_spl
| ~ sQ1254_spl
| ~ sQ1256_spl
| sQ1251_spl
| sQ1309_spl ),
inference(split_clause,[status(thm)],[f71423,f71425,f70854,f70893,f70876,f70904,f71419]) ).
fof(f71429,definition,
! [X0,X1] :
( sQ1310_spl
<=> ( ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ v3_struct_0(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1310_spl])],[split_symbol_definition]) ).
fof(f71432,plain,
( ~ sQ1308_spl
| ~ sQ1258_spl
| ~ sQ1254_spl
| ~ sQ1256_spl
| sQ1251_spl
| sQ1310_spl ),
inference(split_clause,[status(thm)],[f71424,f71429,f70854,f70893,f70876,f70904,f71419]) ).
fof(f71437,plain,
! [X0,X1] :
( ~ sQ1299_spl
| m1_group_2(k9_group_2(sK4182_skl,X0,X1),k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ),
inference(resolution,[status(thm)],[f71320,f70964]) ).
fof(f71438,plain,
! [X0,X1] :
( ~ sQ1299_spl
| l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ),
inference(resolution,[status(thm)],[f71320,f40746]) ).
fof(f71439,plain,
! [X0,X1] :
( ~ sQ1299_spl
| v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ),
inference(resolution,[status(thm)],[f71320,f40745]) ).
fof(f71440,plain,
! [X0,X1] :
( ~ sQ1299_spl
| v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ),
inference(resolution,[status(thm)],[f71320,f40196]) ).
fof(f71441,plain,
! [X0,X1] :
( ~ sQ1299_spl
| ~ v3_struct_0(k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ),
inference(resolution,[status(thm)],[f71320,f40744]) ).
fof(f71442,definition,
! [X0,X1] :
( sQ1311_spl
<=> ( m1_group_2(k9_group_2(sK4182_skl,X0,X1),k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1311_spl])],[split_symbol_definition]) ).
fof(f71445,plain,
( ~ sQ1299_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1311_spl ),
inference(split_clause,[status(thm)],[f71437,f71442,f70845,f70848,f70873,f70851,f71319]) ).
fof(f71446,definition,
! [X0,X1] :
( sQ1312_spl
<=> ( l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1312_spl])],[split_symbol_definition]) ).
fof(f71449,plain,
( ~ sQ1299_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1312_spl ),
inference(split_clause,[status(thm)],[f71438,f71446,f70845,f70848,f70851,f71319]) ).
fof(f71450,definition,
! [X0,X1] :
( sQ1313_spl
<=> ( v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1313_spl])],[split_symbol_definition]) ).
fof(f71453,plain,
( ~ sQ1299_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1313_spl ),
inference(split_clause,[status(thm)],[f71439,f71450,f70845,f70848,f70851,f71319]) ).
fof(f71454,definition,
! [X0,X1] :
( sQ1314_spl
<=> ( v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1314_spl])],[split_symbol_definition]) ).
fof(f71457,plain,
( ~ sQ1299_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1314_spl ),
inference(split_clause,[status(thm)],[f71440,f71454,f70845,f70848,f70873,f70851,f71319]) ).
fof(f71458,definition,
! [X0,X1] :
( sQ1315_spl
<=> ( ~ v3_struct_0(k9_group_2(sK4182_skl,X0,X1))
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1315_spl])],[split_symbol_definition]) ).
fof(f71461,plain,
( ~ sQ1299_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1315_spl ),
inference(split_clause,[status(thm)],[f71441,f71458,f70845,f70848,f70851,f71319]) ).
fof(f71462,plain,
! [X0,X1] :
( ~ sQ1260_spl
| m1_group_2(k9_group_2(X0,sK4183_skl,X1),sK4179_skl)
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f71334,f71331]) ).
fof(f71465,plain,
! [X0,X1] :
( ~ sQ1260_spl
| m1_group_2(k9_group_2(X0,sK4183_skl,X1),k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71462,f70964]) ).
fof(f71466,plain,
! [X0,X1] :
( ~ sQ1260_spl
| l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71462,f40746]) ).
fof(f71467,plain,
! [X0,X1] :
( ~ sQ1260_spl
| v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71462,f40745]) ).
fof(f71468,plain,
! [X0,X1] :
( ~ sQ1260_spl
| v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71462,f40196]) ).
fof(f71469,plain,
! [X0,X1] :
( ~ sQ1260_spl
| ~ v3_struct_0(k9_group_2(X0,sK4183_skl,X1))
| ~ l1_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl)
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71462,f40744]) ).
fof(f71472,definition,
! [X0,X1] :
( sQ1316_spl
<=> ( m1_group_2(k9_group_2(X0,sK4183_skl,X1),k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1316_spl])],[split_symbol_definition]) ).
fof(f71475,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1316_spl ),
inference(split_clause,[status(thm)],[f71465,f71472,f70845,f70848,f70873,f70851,f70918]) ).
fof(f71476,definition,
! [X0,X1] :
( sQ1317_spl
<=> ( l1_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1317_spl])],[split_symbol_definition]) ).
fof(f71479,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1317_spl ),
inference(split_clause,[status(thm)],[f71466,f71476,f70845,f70848,f70851,f70918]) ).
fof(f71480,definition,
! [X0,X1] :
( sQ1318_spl
<=> ( v3_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1318_spl])],[split_symbol_definition]) ).
fof(f71483,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1318_spl ),
inference(split_clause,[status(thm)],[f71467,f71480,f70845,f70848,f70851,f70918]) ).
fof(f71484,definition,
! [X0,X1] :
( sQ1319_spl
<=> ( v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1319_spl])],[split_symbol_definition]) ).
fof(f71487,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1319_spl ),
inference(split_clause,[status(thm)],[f71468,f71484,f70845,f70848,f70873,f70851,f70918]) ).
fof(f71488,definition,
! [X0,X1] :
( sQ1320_spl
<=> ( ~ v3_struct_0(k9_group_2(X0,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1320_spl])],[split_symbol_definition]) ).
fof(f71491,plain,
( ~ sQ1260_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| sQ1248_spl
| sQ1320_spl ),
inference(split_clause,[status(thm)],[f71469,f71488,f70845,f70848,f70851,f70918]) ).
fof(f71493,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)],[f71177,f40745]) ).
fof(f71494,plain,
! [X0,X1] :
( ~ sQ1299_spl
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| v1_group_3(k9_group_2(sK4182_skl,X0,X1),k9_group_2(sK4182_skl,X0,X1))
| ~ v1_group_3(k9_group_2(sK4182_skl,X0,X1),sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f71493,f71320]) ).
fof(f71495,plain,
! [X0,X1] :
( ~ sQ1300_spl
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| v1_group_3(k9_group_2(sK4183_skl,X0,X1),k9_group_2(sK4183_skl,X0,X1))
| ~ v1_group_3(k9_group_2(sK4183_skl,X0,X1),sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f71493,f71324]) ).
fof(f71496,plain,
! [X0,X1] :
( ~ sQ1260_spl
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_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,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| v1_group_3(k9_group_2(X0,sK4183_skl,X1),k9_group_2(X0,sK4183_skl,X1))
| ~ v1_group_3(k9_group_2(X0,sK4183_skl,X1),sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f71493,f71462]) ).
fof(f71507,definition,
! [X0,X1] :
( sQ1321_spl
<=> ( ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ m1_group_2(X1,sK4182_skl)
| ~ v1_group_3(X1,sK4182_skl)
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(k9_group_2(sK4182_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4182_skl,X0,X1))
| v1_group_3(k9_group_2(sK4182_skl,X0,X1),k9_group_2(sK4182_skl,X0,X1))
| ~ v1_group_3(k9_group_2(sK4182_skl,X0,X1),sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1321_spl])],[split_symbol_definition]) ).
fof(f71510,plain,
( ~ sQ1299_spl
| sQ1321_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71494,f70845,f70848,f70873,f70851,f71507,f71319]) ).
fof(f71511,definition,
! [X0,X1] :
( sQ1322_spl
<=> ( ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v3_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ m1_group_2(X1,sK4183_skl)
| ~ v1_group_3(X1,sK4183_skl)
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(k9_group_2(sK4183_skl,X0,X1))
| ~ v4_group_1(k9_group_2(sK4183_skl,X0,X1))
| v1_group_3(k9_group_2(sK4183_skl,X0,X1),k9_group_2(sK4183_skl,X0,X1))
| ~ v1_group_3(k9_group_2(sK4183_skl,X0,X1),sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1322_spl])],[split_symbol_definition]) ).
fof(f71514,plain,
( ~ sQ1300_spl
| sQ1322_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71495,f70845,f70848,f70873,f70851,f71511,f71323]) ).
fof(f71515,definition,
! [X0,X1] :
( sQ1323_spl
<=> ( ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| ~ m1_group_2(X1,X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(sK4183_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,sK4183_skl,X1))
| ~ v4_group_1(k9_group_2(X0,sK4183_skl,X1))
| v1_group_3(k9_group_2(X0,sK4183_skl,X1),k9_group_2(X0,sK4183_skl,X1))
| ~ v1_group_3(k9_group_2(X0,sK4183_skl,X1),sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1323_spl])],[split_symbol_definition]) ).
fof(f71518,plain,
( ~ sQ1260_spl
| sQ1323_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71496,f70845,f70848,f70873,f70851,f71515,f70918]) ).
fof(f71550,plain,
! [X0] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(sK4183_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(sK4183_skl,sK4179_skl)
| ~ m1_group_2(X0,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70521,f59630]) ).
fof(f71551,plain,
! [X0] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(sK4182_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),X0,sK4182_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(sK4182_skl,sK4179_skl)
| ~ m1_group_2(X0,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70521,f59629]) ).
fof(f71552,definition,
! [X0] :
( sQ1324_spl
<=> ( r1_tarski(u1_struct_0(X0),u1_struct_0(sK4183_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1324_spl])],[split_symbol_definition]) ).
fof(f71553,plain,
! [X0] :
( ~ sQ1324_spl
| r1_tarski(u1_struct_0(X0),u1_struct_0(sK4183_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ),
inference(component_clause,[status(thm)],[f71552]) ).
fof(f71555,plain,
( ~ sQ1262_spl
| sQ1324_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71550,f70845,f70848,f70873,f70851,f71552,f70930]) ).
fof(f71556,definition,
! [X0] :
( sQ1325_spl
<=> ( r1_tarski(u1_struct_0(X0),u1_struct_0(sK4182_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),X0,sK4182_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1325_spl])],[split_symbol_definition]) ).
fof(f71557,plain,
! [X0] :
( ~ sQ1325_spl
| r1_tarski(u1_struct_0(X0),u1_struct_0(sK4182_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),X0,sK4182_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ),
inference(component_clause,[status(thm)],[f71556]) ).
fof(f71559,plain,
( ~ sQ1263_spl
| sQ1325_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71551,f70845,f70848,f70873,f70851,f71556,f70935]) ).
fof(f71560,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK4183_skl))
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(sK4183_skl,sK4179_skl)
| ~ m1_group_2(X0,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70522,f59630]) ).
fof(f71561,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK4182_skl))
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4182_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(sK4182_skl,sK4179_skl)
| ~ m1_group_2(X0,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f70522,f59629]) ).
fof(f71564,definition,
! [X0] :
( sQ1326_spl
<=> ( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK4183_skl))
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1326_spl])],[split_symbol_definition]) ).
fof(f71565,plain,
! [X0] :
( ~ sQ1326_spl
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK4183_skl))
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ),
inference(component_clause,[status(thm)],[f71564]) ).
fof(f71567,plain,
( ~ sQ1262_spl
| sQ1326_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71560,f70845,f70848,f70873,f70851,f71564,f70930]) ).
fof(f71568,definition,
! [X0] :
( sQ1327_spl
<=> ( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK4182_skl))
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4182_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1327_spl])],[split_symbol_definition]) ).
fof(f71569,plain,
! [X0] :
( ~ sQ1327_spl
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(sK4182_skl))
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4182_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ),
inference(component_clause,[status(thm)],[f71568]) ).
fof(f71571,plain,
( ~ sQ1263_spl
| sQ1327_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71561,f70845,f70848,f70873,f70851,f71568,f70935]) ).
fof(f71592,plain,
( ~ sQ1324_spl
| r1_tarski(u1_struct_0(sK4183_skl),u1_struct_0(sK4183_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),sK4183_skl,sK4183_skl)
| ~ m1_group_2(sK4183_skl,sK4179_skl) ),
inference(resolution,[status(thm)],[f71553,f59630]) ).
fof(f71593,plain,
( ~ sQ1324_spl
| r1_tarski(u1_struct_0(sK4182_skl),u1_struct_0(sK4183_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4183_skl)
| ~ m1_group_2(sK4182_skl,sK4179_skl) ),
inference(resolution,[status(thm)],[f71553,f59629]) ).
fof(f71594,definition,
( sQ1328_spl
<=> r3_lattices(k11_group_4(sK4179_skl),sK4183_skl,sK4183_skl) ),
introduced(definition,[new_symbols(definition,[sQ1328_spl])],[split_symbol_definition]) ).
fof(f71597,definition,
( sQ1329_spl
<=> r1_tarski(u1_struct_0(sK4183_skl),u1_struct_0(sK4183_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1329_spl])],[split_symbol_definition]) ).
fof(f71600,plain,
( ~ sQ1324_spl
| sQ1329_spl
| ~ sQ1328_spl
| ~ sQ1262_spl ),
inference(split_clause,[status(thm)],[f71592,f70930,f71594,f71597,f71552]) ).
fof(f71601,definition,
( sQ1330_spl
<=> r1_tarski(u1_struct_0(sK4182_skl),u1_struct_0(sK4183_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1330_spl])],[split_symbol_definition]) ).
fof(f71602,plain,
( ~ sQ1330_spl
| r1_tarski(u1_struct_0(sK4182_skl),u1_struct_0(sK4183_skl)) ),
inference(component_clause,[status(thm)],[f71601]) ).
fof(f71604,plain,
( ~ sQ1324_spl
| sQ1330_spl
| ~ sQ977_spl
| ~ sQ1263_spl ),
inference(split_clause,[status(thm)],[f71593,f70935,f66628,f71601,f71552]) ).
fof(f71606,plain,
! [X0] :
( ~ sQ1330_spl
| m1_group_2(sK4182_skl,sK4183_skl)
| ~ m1_group_2(sK4183_skl,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f71602,f40385]) ).
fof(f71608,definition,
! [X0] :
( sQ1331_spl
<=> ( ~ m1_group_2(sK4183_skl,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1331_spl])],[split_symbol_definition]) ).
fof(f71609,plain,
! [X0] :
( ~ sQ1331_spl
| ~ m1_group_2(sK4183_skl,X0)
| ~ m1_group_2(sK4182_skl,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f71608]) ).
fof(f71611,plain,
( ~ sQ1330_spl
| sQ1274_spl
| sQ1331_spl ),
inference(split_clause,[status(thm)],[f71606,f71608,f71024,f71601]) ).
fof(f71628,plain,
( ~ sQ1325_spl
| r1_tarski(u1_struct_0(sK4182_skl),u1_struct_0(sK4182_skl))
| ~ r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4182_skl)
| ~ m1_group_2(sK4182_skl,sK4179_skl) ),
inference(resolution,[status(thm)],[f71557,f59629]) ).
fof(f71636,definition,
( sQ1334_spl
<=> r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4182_skl) ),
introduced(definition,[new_symbols(definition,[sQ1334_spl])],[split_symbol_definition]) ).
fof(f71639,definition,
( sQ1335_spl
<=> r1_tarski(u1_struct_0(sK4182_skl),u1_struct_0(sK4182_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1335_spl])],[split_symbol_definition]) ).
fof(f71642,plain,
( ~ sQ1325_spl
| sQ1335_spl
| ~ sQ1334_spl
| ~ sQ1263_spl ),
inference(split_clause,[status(thm)],[f71628,f70935,f71636,f71639,f71556]) ).
fof(f71714,plain,
! [X0] :
( ~ sQ1326_spl
| ~ m1_group_2(X0,sK4183_skl)
| ~ l1_group_1(sK4183_skl)
| ~ v3_group_1(sK4183_skl)
| v3_struct_0(sK4183_skl)
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ),
inference(resolution,[status(thm)],[f71565,f71019]) ).
fof(f71715,plain,
( ~ sQ1326_spl
| r3_lattices(k11_group_4(sK4179_skl),sK4183_skl,sK4183_skl)
| ~ m1_subset_1(sK4183_skl,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(sK4183_skl,sK4179_skl) ),
inference(resolution,[status(thm)],[f71565,f14074]) ).
fof(f71716,definition,
! [X0] :
( sQ1339_spl
<=> ( ~ m1_group_2(X0,sK4183_skl)
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1339_spl])],[split_symbol_definition]) ).
fof(f71717,plain,
! [X0] :
( ~ sQ1339_spl
| ~ m1_group_2(X0,sK4183_skl)
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4183_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ),
inference(component_clause,[status(thm)],[f71716]) ).
fof(f71719,plain,
( ~ sQ1326_spl
| ~ sQ1258_spl
| ~ sQ1256_spl
| sQ1251_spl
| sQ1339_spl ),
inference(split_clause,[status(thm)],[f71714,f71716,f70854,f70893,f70904,f71564]) ).
fof(f71720,plain,
( ~ sQ1326_spl
| sQ1328_spl
| ~ sQ1267_spl
| ~ sQ1262_spl ),
inference(split_clause,[status(thm)],[f71715,f70930,f70949,f71594,f71564]) ).
fof(f71721,plain,
( sQ1267_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f70951,f59630]) ).
fof(f71722,plain,
sQ1267_spl,
inference(contradiction_clause,[status(thm)],[f71721]) ).
fof(f71723,plain,
! [X0] :
( ~ sQ1327_spl
| ~ m1_group_2(X0,sK4182_skl)
| ~ l1_group_1(sK4182_skl)
| ~ v3_group_1(sK4182_skl)
| v3_struct_0(sK4182_skl)
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4182_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ),
inference(resolution,[status(thm)],[f71569,f71019]) ).
fof(f71724,plain,
( ~ sQ1327_spl
| r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4182_skl)
| ~ m1_subset_1(sK4182_skl,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(sK4182_skl,sK4179_skl) ),
inference(resolution,[status(thm)],[f71569,f14074]) ).
fof(f71725,definition,
! [X0] :
( sQ1340_spl
<=> ( ~ m1_group_2(X0,sK4182_skl)
| r3_lattices(k11_group_4(sK4179_skl),X0,sK4182_skl)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK4179_skl)))
| ~ m1_group_2(X0,sK4179_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1340_spl])],[split_symbol_definition]) ).
fof(f71728,plain,
( ~ sQ1327_spl
| ~ sQ1259_spl
| ~ sQ1257_spl
| sQ1252_spl
| sQ1340_spl ),
inference(split_clause,[status(thm)],[f71723,f71725,f70858,f70897,f70908,f71568]) ).
fof(f71729,plain,
( ~ sQ1327_spl
| sQ1334_spl
| ~ sQ1269_spl
| ~ sQ1263_spl ),
inference(split_clause,[status(thm)],[f71724,f70935,f70957,f71636,f71568]) ).
fof(f71730,plain,
( sQ1269_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f70959,f59629]) ).
fof(f71731,plain,
sQ1269_spl,
inference(contradiction_clause,[status(thm)],[f71730]) ).
fof(f71733,plain,
( ~ sQ1339_spl
| ~ m1_group_2(sK4182_skl,sK4183_skl)
| r3_lattices(k11_group_4(sK4179_skl),sK4182_skl,sK4183_skl)
| ~ m1_group_2(sK4182_skl,sK4179_skl) ),
inference(resolution,[status(thm)],[f71717,f59629]) ).
fof(f71735,plain,
( ~ sQ1339_spl
| ~ sQ1274_spl
| sQ977_spl
| ~ sQ1263_spl ),
inference(split_clause,[status(thm)],[f71733,f70935,f66628,f71024,f71716]) ).
fof(f71744,plain,
( ~ sQ1331_spl
| ~ m1_group_2(sK4183_skl,sK4179_skl)
| ~ l1_group_1(sK4179_skl)
| ~ v4_group_1(sK4179_skl)
| ~ v3_group_1(sK4179_skl)
| v3_struct_0(sK4179_skl) ),
inference(resolution,[status(thm)],[f71609,f70838]) ).
fof(f71747,plain,
( ~ sQ1331_spl
| ~ sQ1262_spl
| ~ sQ1250_spl
| ~ sQ1253_spl
| ~ sQ1249_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f71744,f70845,f70848,f70873,f70851,f70930,f71608]) ).
fof(f71749,plain,
$false,
inference(sat_refutation,[status(thm)],[f62978,f62982,f63119,f64968,f64972,f64976,f65770,f66634,f66635,f70857,f70861,f70863,f70865,f70867,f70879,f70883,f70885,f70896,f70900,f70907,f70911,f70921,f70925,f70933,f70938,f70962,f70966,f70979,f70983,f70997,f71014,f71027,f71031,f71055,f71101,f71105,f71228,f71273,f71274,f71275,f71276,f71277,f71288,f71292,f71296,f71300,f71304,f71322,f71326,f71372,f71376,f71406,f71410,f71414,f71418,f71422,f71428,f71432,f71445,f71449,f71453,f71457,f71461,f71475,f71479,f71483,f71487,f71491,f71510,f71514,f71518,f71555,f71559,f71567,f71571,f71600,f71604,f71611,f71642,f71719,f71720,f71722,f71728,f71729,f71731,f71735,f71747]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP648+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/10.41 % Computer : n008.cluster.edu
% 0.15/10.41 % Model : x86_64 x86_64
% 0.15/10.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/10.41 % Memory : 8046.5625MB
% 0.15/10.41 % OS : Linux 6.8.0-71-generic
% 0.15/10.41 % CPULimit : 300
% 0.15/10.41 % WCLimit : 300
% 0.15/10.41 % DateTime : Sun Sep 20 20:27:42 UTC 2026
% 0.15/10.42 % CPUTime :
% 3.04/13.35 % Drodi V4.1.1
% 11.84/14.63 % Refutation found
% 11.84/14.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.84/14.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.77/15.05 % Elapsed time: 4.593216 seconds
% 3.77/15.05 % CPU time: 13.388723 seconds
% 3.77/15.05 % Total memory used: 3.921 GB
% 3.77/15.05 % Net memory used: 3.897 GB
%------------------------------------------------------------------------------