%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG219+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 11:48:59 AM UTC 2026
% Result : Theorem 267.25s 34.77s
% Output : CNFRefutation 213.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 179
% Syntax : Number of formulae : 822 ( 311 unt; 152 def)
% Number of atoms : 2030 ( 41 equ)
% Maximal formula atoms : 26 ( 2 avg)
% Number of connectives : 1725 ( 517 ~; 554 |; 487 &)
% ( 152 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 190 ( 188 usr; 153 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 25 con; 0-3 aty)
% Number of variables : 64 ( 43 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f482,axiom,
! [A] : k2_subset_1(A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f486,axiom,
! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f564,axiom,
! [A] : m1_subset_1(k2_subset_1(A),k1_zfmisc_1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1776,axiom,
? [A] :
( v1_int_1(A)
& v1_xreal_0(A)
& v1_xcmplx_0(A)
& m1_subset_1(A,k1_numbers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2203,axiom,
? [A] :
( v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& v1_rlvect_1(A)
& ~ v3_struct_0(A)
& l1_rlvect_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2204,axiom,
? [A] :
( v7_rlvect_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& v2_rlvect_1(A)
& ~ v3_struct_0(A)
& l2_rlvect_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2458,axiom,
? [A] :
( v4_group_1(A)
& v3_group_1(A)
& v2_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A)
& l1_group_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2459,axiom,
? [A] :
( v7_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v2_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A)
& l1_group_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2592,axiom,
( v1_rlvect_1(k1_vectsp_1)
& ~ v3_struct_0(k1_vectsp_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2593,axiom,
( v6_rlvect_1(k1_vectsp_1)
& v5_rlvect_1(k1_vectsp_1)
& v4_rlvect_1(k1_vectsp_1)
& v3_rlvect_1(k1_vectsp_1)
& v1_rlvect_1(k1_vectsp_1)
& ~ v3_struct_0(k1_vectsp_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2594,axiom,
? [A] :
( v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& v1_rlvect_1(A)
& ~ v3_struct_0(A)
& l1_rlvect_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2600,axiom,
? [A] :
( v3_vectsp_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2603,axiom,
( ~ v10_vectsp_1(k3_vectsp_1)
& v9_vectsp_1(k3_vectsp_1)
& v8_vectsp_1(k3_vectsp_1)
& v7_vectsp_1(k3_vectsp_1)
& v6_vectsp_1(k3_vectsp_1)
& v3_vectsp_1(k3_vectsp_1)
& v7_group_1(k3_vectsp_1)
& v4_group_1(k3_vectsp_1)
& v2_group_1(k3_vectsp_1)
& v6_rlvect_1(k3_vectsp_1)
& v5_rlvect_1(k3_vectsp_1)
& v4_rlvect_1(k3_vectsp_1)
& v3_rlvect_1(k3_vectsp_1)
& ~ v3_struct_0(k3_vectsp_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2608,axiom,
? [A] :
( v7_group_1(A)
& v4_group_1(A)
& ~ v3_struct_0(A)
& l1_group_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2609,axiom,
? [A] :
( v8_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& ~ v3_struct_0(A)
& l1_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2610,axiom,
? [A] :
( ~ v10_vectsp_1(A)
& v9_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v3_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2617,axiom,
? [A] :
( v13_vectsp_1(A)
& ~ v10_vectsp_1(A)
& v9_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v3_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2942,axiom,
? [A] :
( v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v3_vectsp_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2943,axiom,
? [A] :
( v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v3_vectsp_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2944,axiom,
? [A] :
( v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2945,axiom,
? [A] :
( v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v3_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2946,axiom,
? [A] :
( v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v3_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2947,axiom,
? [A] :
( ~ v10_vectsp_1(A)
& v9_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2948,axiom,
? [A] :
( ~ v10_vectsp_1(A)
& v9_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v5_vectsp_1(A)
& v4_vectsp_1(A)
& v3_vectsp_1(A)
& v4_group_1(A)
& v2_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A)
& l3_vectsp_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3171,axiom,
! [A] :
( ( l3_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> m1_rmod_2(B,A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3457,axiom,
! [A] :
( ( l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( ( m1_rmod_2(D,A,B)
& v3_vectsp_2(D,A) )
=> ( C = u1_struct_0(D)
=> ( k1_rmod_5(A,B,C) = D
| k1_rlvect_1(A) = k2_group_1(A) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3458,conjecture,
! [A] :
( ( l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v3_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ( C = u1_struct_0(B)
=> ( k1_rmod_5(A,B,C) = B
| k1_rlvect_1(A) = k2_group_1(A) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3459,negated_conjecture,
~ ! [A] :
( ( l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v3_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ( C = u1_struct_0(B)
=> ( k1_rmod_5(A,B,C) = B
| k1_rlvect_1(A) = k2_group_1(A) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3458]) ).
fof(f4451,plain,
! [X0] : k2_subset_1(X0) = X0,
inference(cnf_transformation,[status(thm)],[f482]) ).
fof(f4452,plain,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f486]) ).
fof(f4666,plain,
! [X0] : m1_subset_1(k2_subset_1(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f564]) ).
fof(f8608,plain,
( v1_int_1(sK513_skl)
& v1_xreal_0(sK513_skl)
& v1_xcmplx_0(sK513_skl)
& m1_subset_1(sK513_skl,k1_numbers) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK513_skl]),skolemize(A,sK513_skl)],[f1776]) ).
fof(f8609,plain,
m1_subset_1(sK513_skl,k1_numbers),
inference(cnf_transformation,[status(thm)],[f8608]) ).
fof(f9846,plain,
( v6_rlvect_1(sK602_skl)
& v5_rlvect_1(sK602_skl)
& v4_rlvect_1(sK602_skl)
& v3_rlvect_1(sK602_skl)
& v1_rlvect_1(sK602_skl)
& ~ v3_struct_0(sK602_skl)
& l1_rlvect_1(sK602_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK602_skl]),skolemize(A,sK602_skl)],[f2203]) ).
fof(f9848,plain,
~ v3_struct_0(sK602_skl),
inference(cnf_transformation,[status(thm)],[f9846]) ).
fof(f9850,plain,
v3_rlvect_1(sK602_skl),
inference(cnf_transformation,[status(thm)],[f9846]) ).
fof(f9851,plain,
v4_rlvect_1(sK602_skl),
inference(cnf_transformation,[status(thm)],[f9846]) ).
fof(f9852,plain,
v5_rlvect_1(sK602_skl),
inference(cnf_transformation,[status(thm)],[f9846]) ).
fof(f9853,plain,
v6_rlvect_1(sK602_skl),
inference(cnf_transformation,[status(thm)],[f9846]) ).
fof(f9854,plain,
( v7_rlvect_1(sK603_skl)
& v6_rlvect_1(sK603_skl)
& v5_rlvect_1(sK603_skl)
& v4_rlvect_1(sK603_skl)
& v3_rlvect_1(sK603_skl)
& v2_rlvect_1(sK603_skl)
& ~ v3_struct_0(sK603_skl)
& l2_rlvect_1(sK603_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK603_skl]),skolemize(A,sK603_skl)],[f2204]) ).
fof(f9856,plain,
~ v3_struct_0(sK603_skl),
inference(cnf_transformation,[status(thm)],[f9854]) ).
fof(f9858,plain,
v3_rlvect_1(sK603_skl),
inference(cnf_transformation,[status(thm)],[f9854]) ).
fof(f9859,plain,
v4_rlvect_1(sK603_skl),
inference(cnf_transformation,[status(thm)],[f9854]) ).
fof(f9860,plain,
v5_rlvect_1(sK603_skl),
inference(cnf_transformation,[status(thm)],[f9854]) ).
fof(f9861,plain,
v6_rlvect_1(sK603_skl),
inference(cnf_transformation,[status(thm)],[f9854]) ).
fof(f10537,plain,
( v4_group_1(sK650_skl)
& v3_group_1(sK650_skl)
& v2_group_1(sK650_skl)
& v1_group_1(sK650_skl)
& ~ v3_struct_0(sK650_skl)
& l1_group_1(sK650_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK650_skl]),skolemize(A,sK650_skl)],[f2458]) ).
fof(f10539,plain,
~ v3_struct_0(sK650_skl),
inference(cnf_transformation,[status(thm)],[f10537]) ).
fof(f10544,plain,
( v7_group_1(sK651_skl)
& v4_group_1(sK651_skl)
& v3_group_1(sK651_skl)
& v2_group_1(sK651_skl)
& v1_group_1(sK651_skl)
& ~ v3_struct_0(sK651_skl)
& l1_group_1(sK651_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK651_skl]),skolemize(A,sK651_skl)],[f2459]) ).
fof(f10546,plain,
~ v3_struct_0(sK651_skl),
inference(cnf_transformation,[status(thm)],[f10544]) ).
fof(f10550,plain,
v4_group_1(sK651_skl),
inference(cnf_transformation,[status(thm)],[f10544]) ).
fof(f10551,plain,
v7_group_1(sK651_skl),
inference(cnf_transformation,[status(thm)],[f10544]) ).
fof(f10881,plain,
~ v3_struct_0(k1_vectsp_1),
inference(cnf_transformation,[status(thm)],[f2592]) ).
fof(f10885,plain,
v3_rlvect_1(k1_vectsp_1),
inference(cnf_transformation,[status(thm)],[f2593]) ).
fof(f10886,plain,
v4_rlvect_1(k1_vectsp_1),
inference(cnf_transformation,[status(thm)],[f2593]) ).
fof(f10887,plain,
v5_rlvect_1(k1_vectsp_1),
inference(cnf_transformation,[status(thm)],[f2593]) ).
fof(f10888,plain,
v6_rlvect_1(k1_vectsp_1),
inference(cnf_transformation,[status(thm)],[f2593]) ).
fof(f10889,plain,
( v6_rlvect_1(sK677_skl)
& v5_rlvect_1(sK677_skl)
& v4_rlvect_1(sK677_skl)
& v3_rlvect_1(sK677_skl)
& v1_rlvect_1(sK677_skl)
& ~ v3_struct_0(sK677_skl)
& l1_rlvect_1(sK677_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK677_skl]),skolemize(A,sK677_skl)],[f2594]) ).
fof(f10891,plain,
~ v3_struct_0(sK677_skl),
inference(cnf_transformation,[status(thm)],[f10889]) ).
fof(f10893,plain,
v3_rlvect_1(sK677_skl),
inference(cnf_transformation,[status(thm)],[f10889]) ).
fof(f10894,plain,
v4_rlvect_1(sK677_skl),
inference(cnf_transformation,[status(thm)],[f10889]) ).
fof(f10895,plain,
v5_rlvect_1(sK677_skl),
inference(cnf_transformation,[status(thm)],[f10889]) ).
fof(f10896,plain,
v6_rlvect_1(sK677_skl),
inference(cnf_transformation,[status(thm)],[f10889]) ).
fof(f10914,plain,
( v3_vectsp_1(sK683_skl)
& ~ v3_struct_0(sK683_skl)
& l3_vectsp_1(sK683_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK683_skl]),skolemize(A,sK683_skl)],[f2600]) ).
fof(f10916,plain,
~ v3_struct_0(sK683_skl),
inference(cnf_transformation,[status(thm)],[f10914]) ).
fof(f10930,plain,
v7_group_1(k3_vectsp_1),
inference(cnf_transformation,[status(thm)],[f2603]) ).
fof(f10951,plain,
( v7_group_1(sK684_skl)
& v4_group_1(sK684_skl)
& ~ v3_struct_0(sK684_skl)
& l1_group_1(sK684_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK684_skl]),skolemize(A,sK684_skl)],[f2608]) ).
fof(f10953,plain,
~ v3_struct_0(sK684_skl),
inference(cnf_transformation,[status(thm)],[f10951]) ).
fof(f10954,plain,
v4_group_1(sK684_skl),
inference(cnf_transformation,[status(thm)],[f10951]) ).
fof(f10955,plain,
v7_group_1(sK684_skl),
inference(cnf_transformation,[status(thm)],[f10951]) ).
fof(f10956,plain,
( v8_vectsp_1(sK685_skl)
& v6_vectsp_1(sK685_skl)
& v7_group_1(sK685_skl)
& v4_group_1(sK685_skl)
& v2_group_1(sK685_skl)
& ~ v3_struct_0(sK685_skl)
& l1_vectsp_1(sK685_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK685_skl]),skolemize(A,sK685_skl)],[f2609]) ).
fof(f10958,plain,
~ v3_struct_0(sK685_skl),
inference(cnf_transformation,[status(thm)],[f10956]) ).
fof(f10960,plain,
v4_group_1(sK685_skl),
inference(cnf_transformation,[status(thm)],[f10956]) ).
fof(f10961,plain,
v7_group_1(sK685_skl),
inference(cnf_transformation,[status(thm)],[f10956]) ).
fof(f10963,plain,
v8_vectsp_1(sK685_skl),
inference(cnf_transformation,[status(thm)],[f10956]) ).
fof(f10964,plain,
( ~ v10_vectsp_1(sK686_skl)
& v9_vectsp_1(sK686_skl)
& v8_vectsp_1(sK686_skl)
& v7_vectsp_1(sK686_skl)
& v6_vectsp_1(sK686_skl)
& v5_vectsp_1(sK686_skl)
& v4_vectsp_1(sK686_skl)
& v3_vectsp_1(sK686_skl)
& v7_group_1(sK686_skl)
& v4_group_1(sK686_skl)
& v2_group_1(sK686_skl)
& v6_rlvect_1(sK686_skl)
& v5_rlvect_1(sK686_skl)
& v4_rlvect_1(sK686_skl)
& v3_rlvect_1(sK686_skl)
& ~ v3_struct_0(sK686_skl)
& l3_vectsp_1(sK686_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK686_skl]),skolemize(A,sK686_skl)],[f2610]) ).
fof(f10965,plain,
l3_vectsp_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10966,plain,
~ v3_struct_0(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10967,plain,
v3_rlvect_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10968,plain,
v4_rlvect_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10969,plain,
v5_rlvect_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10970,plain,
v6_rlvect_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10972,plain,
v4_group_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10973,plain,
v7_group_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10978,plain,
v7_vectsp_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10979,plain,
v8_vectsp_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10980,plain,
v9_vectsp_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f10981,plain,
~ v10_vectsp_1(sK686_skl),
inference(cnf_transformation,[status(thm)],[f10964]) ).
fof(f11011,plain,
( v13_vectsp_1(sK691_skl)
& ~ v10_vectsp_1(sK691_skl)
& v9_vectsp_1(sK691_skl)
& v8_vectsp_1(sK691_skl)
& v7_vectsp_1(sK691_skl)
& v6_vectsp_1(sK691_skl)
& v5_vectsp_1(sK691_skl)
& v4_vectsp_1(sK691_skl)
& v3_vectsp_1(sK691_skl)
& v7_group_1(sK691_skl)
& v4_group_1(sK691_skl)
& v2_group_1(sK691_skl)
& v6_rlvect_1(sK691_skl)
& v5_rlvect_1(sK691_skl)
& v4_rlvect_1(sK691_skl)
& v3_rlvect_1(sK691_skl)
& ~ v3_struct_0(sK691_skl)
& l3_vectsp_1(sK691_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK691_skl]),skolemize(A,sK691_skl)],[f2617]) ).
fof(f11012,plain,
l3_vectsp_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11013,plain,
~ v3_struct_0(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11014,plain,
v3_rlvect_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11015,plain,
v4_rlvect_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11016,plain,
v5_rlvect_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11017,plain,
v6_rlvect_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11019,plain,
v4_group_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11020,plain,
v7_group_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11025,plain,
v7_vectsp_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11026,plain,
v8_vectsp_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11027,plain,
v9_vectsp_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11028,plain,
~ v10_vectsp_1(sK691_skl),
inference(cnf_transformation,[status(thm)],[f11011]) ).
fof(f11743,plain,
( v8_vectsp_1(sK743_skl)
& v7_vectsp_1(sK743_skl)
& v6_vectsp_1(sK743_skl)
& v5_vectsp_1(sK743_skl)
& v4_vectsp_1(sK743_skl)
& v3_vectsp_1(sK743_skl)
& v2_group_1(sK743_skl)
& v6_rlvect_1(sK743_skl)
& v5_rlvect_1(sK743_skl)
& v4_rlvect_1(sK743_skl)
& v3_rlvect_1(sK743_skl)
& ~ v3_struct_0(sK743_skl)
& l3_vectsp_1(sK743_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK743_skl]),skolemize(A,sK743_skl)],[f2942]) ).
fof(f11744,plain,
l3_vectsp_1(sK743_skl),
inference(cnf_transformation,[status(thm)],[f11743]) ).
fof(f11745,plain,
~ v3_struct_0(sK743_skl),
inference(cnf_transformation,[status(thm)],[f11743]) ).
fof(f11746,plain,
v3_rlvect_1(sK743_skl),
inference(cnf_transformation,[status(thm)],[f11743]) ).
fof(f11747,plain,
v4_rlvect_1(sK743_skl),
inference(cnf_transformation,[status(thm)],[f11743]) ).
fof(f11748,plain,
v5_rlvect_1(sK743_skl),
inference(cnf_transformation,[status(thm)],[f11743]) ).
fof(f11749,plain,
v6_rlvect_1(sK743_skl),
inference(cnf_transformation,[status(thm)],[f11743]) ).
fof(f11755,plain,
v7_vectsp_1(sK743_skl),
inference(cnf_transformation,[status(thm)],[f11743]) ).
fof(f11756,plain,
v8_vectsp_1(sK743_skl),
inference(cnf_transformation,[status(thm)],[f11743]) ).
fof(f11757,plain,
( v8_vectsp_1(sK744_skl)
& v7_vectsp_1(sK744_skl)
& v6_vectsp_1(sK744_skl)
& v5_vectsp_1(sK744_skl)
& v4_vectsp_1(sK744_skl)
& v3_vectsp_1(sK744_skl)
& v4_group_1(sK744_skl)
& v2_group_1(sK744_skl)
& v6_rlvect_1(sK744_skl)
& v5_rlvect_1(sK744_skl)
& v4_rlvect_1(sK744_skl)
& v3_rlvect_1(sK744_skl)
& ~ v3_struct_0(sK744_skl)
& l3_vectsp_1(sK744_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK744_skl]),skolemize(A,sK744_skl)],[f2943]) ).
fof(f11758,plain,
l3_vectsp_1(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11759,plain,
~ v3_struct_0(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11760,plain,
v3_rlvect_1(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11761,plain,
v4_rlvect_1(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11762,plain,
v5_rlvect_1(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11763,plain,
v6_rlvect_1(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11765,plain,
v4_group_1(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11770,plain,
v7_vectsp_1(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11771,plain,
v8_vectsp_1(sK744_skl),
inference(cnf_transformation,[status(thm)],[f11757]) ).
fof(f11772,plain,
( v8_vectsp_1(sK745_skl)
& v7_vectsp_1(sK745_skl)
& v6_vectsp_1(sK745_skl)
& v5_vectsp_1(sK745_skl)
& v4_vectsp_1(sK745_skl)
& v7_group_1(sK745_skl)
& v4_group_1(sK745_skl)
& v2_group_1(sK745_skl)
& v6_rlvect_1(sK745_skl)
& v5_rlvect_1(sK745_skl)
& v4_rlvect_1(sK745_skl)
& v3_rlvect_1(sK745_skl)
& ~ v3_struct_0(sK745_skl)
& l3_vectsp_1(sK745_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK745_skl]),skolemize(A,sK745_skl)],[f2944]) ).
fof(f11773,plain,
l3_vectsp_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11774,plain,
~ v3_struct_0(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11775,plain,
v3_rlvect_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11776,plain,
v4_rlvect_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11777,plain,
v5_rlvect_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11778,plain,
v6_rlvect_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11780,plain,
v4_group_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11781,plain,
v7_group_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11785,plain,
v7_vectsp_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11786,plain,
v8_vectsp_1(sK745_skl),
inference(cnf_transformation,[status(thm)],[f11772]) ).
fof(f11787,plain,
( v8_vectsp_1(sK746_skl)
& v7_vectsp_1(sK746_skl)
& v6_vectsp_1(sK746_skl)
& v5_vectsp_1(sK746_skl)
& v4_vectsp_1(sK746_skl)
& v3_vectsp_1(sK746_skl)
& v7_group_1(sK746_skl)
& v4_group_1(sK746_skl)
& v2_group_1(sK746_skl)
& v6_rlvect_1(sK746_skl)
& v5_rlvect_1(sK746_skl)
& v4_rlvect_1(sK746_skl)
& v3_rlvect_1(sK746_skl)
& ~ v3_struct_0(sK746_skl)
& l3_vectsp_1(sK746_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK746_skl]),skolemize(A,sK746_skl)],[f2945]) ).
fof(f11788,plain,
l3_vectsp_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11789,plain,
~ v3_struct_0(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11790,plain,
v3_rlvect_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11791,plain,
v4_rlvect_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11792,plain,
v5_rlvect_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11793,plain,
v6_rlvect_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11795,plain,
v4_group_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11796,plain,
v7_group_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11801,plain,
v7_vectsp_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11802,plain,
v8_vectsp_1(sK746_skl),
inference(cnf_transformation,[status(thm)],[f11787]) ).
fof(f11803,plain,
( v2_vectsp_2(sK747_skl)
& ~ v10_vectsp_1(sK747_skl)
& v8_vectsp_1(sK747_skl)
& v7_vectsp_1(sK747_skl)
& v6_vectsp_1(sK747_skl)
& v5_vectsp_1(sK747_skl)
& v4_vectsp_1(sK747_skl)
& v3_vectsp_1(sK747_skl)
& v7_group_1(sK747_skl)
& v4_group_1(sK747_skl)
& v2_group_1(sK747_skl)
& v6_rlvect_1(sK747_skl)
& v5_rlvect_1(sK747_skl)
& v4_rlvect_1(sK747_skl)
& v3_rlvect_1(sK747_skl)
& ~ v3_struct_0(sK747_skl)
& l3_vectsp_1(sK747_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK747_skl]),skolemize(A,sK747_skl)],[f2946]) ).
fof(f11804,plain,
l3_vectsp_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11805,plain,
~ v3_struct_0(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11806,plain,
v3_rlvect_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11807,plain,
v4_rlvect_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11808,plain,
v5_rlvect_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11809,plain,
v6_rlvect_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11811,plain,
v4_group_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11812,plain,
v7_group_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11817,plain,
v7_vectsp_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11818,plain,
v8_vectsp_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11819,plain,
~ v10_vectsp_1(sK747_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11821,plain,
( ~ v10_vectsp_1(sK748_skl)
& v9_vectsp_1(sK748_skl)
& v8_vectsp_1(sK748_skl)
& v7_vectsp_1(sK748_skl)
& v6_vectsp_1(sK748_skl)
& v5_vectsp_1(sK748_skl)
& v4_vectsp_1(sK748_skl)
& v4_group_1(sK748_skl)
& v2_group_1(sK748_skl)
& v6_rlvect_1(sK748_skl)
& v5_rlvect_1(sK748_skl)
& v4_rlvect_1(sK748_skl)
& v3_rlvect_1(sK748_skl)
& ~ v3_struct_0(sK748_skl)
& l3_vectsp_1(sK748_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK748_skl]),skolemize(A,sK748_skl)],[f2947]) ).
fof(f11822,plain,
l3_vectsp_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11823,plain,
~ v3_struct_0(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11824,plain,
v3_rlvect_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11825,plain,
v4_rlvect_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11826,plain,
v5_rlvect_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11827,plain,
v6_rlvect_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11829,plain,
v4_group_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11833,plain,
v7_vectsp_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11834,plain,
v8_vectsp_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11835,plain,
v9_vectsp_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11836,plain,
~ v10_vectsp_1(sK748_skl),
inference(cnf_transformation,[status(thm)],[f11821]) ).
fof(f11837,plain,
( ~ v10_vectsp_1(sK749_skl)
& v9_vectsp_1(sK749_skl)
& v8_vectsp_1(sK749_skl)
& v7_vectsp_1(sK749_skl)
& v6_vectsp_1(sK749_skl)
& v5_vectsp_1(sK749_skl)
& v4_vectsp_1(sK749_skl)
& v3_vectsp_1(sK749_skl)
& v4_group_1(sK749_skl)
& v2_group_1(sK749_skl)
& v6_rlvect_1(sK749_skl)
& v5_rlvect_1(sK749_skl)
& v4_rlvect_1(sK749_skl)
& v3_rlvect_1(sK749_skl)
& ~ v3_struct_0(sK749_skl)
& l3_vectsp_1(sK749_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK749_skl]),skolemize(A,sK749_skl)],[f2948]) ).
fof(f11838,plain,
l3_vectsp_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11839,plain,
~ v3_struct_0(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11840,plain,
v3_rlvect_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11841,plain,
v4_rlvect_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11842,plain,
v5_rlvect_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11843,plain,
v6_rlvect_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11845,plain,
v4_group_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11850,plain,
v7_vectsp_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11851,plain,
v8_vectsp_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11852,plain,
v9_vectsp_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f11853,plain,
~ v10_vectsp_1(sK749_skl),
inference(cnf_transformation,[status(thm)],[f11837]) ).
fof(f12355,plain,
! [A] :
( ! [B] :
( m1_rmod_2(B,A,B)
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B) )
| ~ l3_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3171]) ).
fof(f12356,plain,
! [X0,X1] :
( m1_rmod_2(X1,X0,X1)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ l3_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f12355]) ).
fof(f13146,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( k1_rmod_5(A,B,C) = D
| k1_rlvect_1(A) = k2_group_1(A)
| C != u1_struct_0(D)
| ~ m1_rmod_2(D,A,B)
| ~ v3_vectsp_2(D,A) )
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
| ~ l1_vectsp_2(B,A)
| ~ v5_vectsp_2(B,A)
| ~ v6_rlvect_1(B)
| ~ v5_rlvect_1(B)
| ~ v4_rlvect_1(B)
| ~ v3_rlvect_1(B)
| v3_struct_0(B) )
| ~ l3_vectsp_1(A)
| ~ v2_vectsp_2(A)
| v10_vectsp_1(A)
| ~ v8_vectsp_1(A)
| ~ v7_vectsp_1(A)
| ~ v6_vectsp_1(A)
| ~ v7_group_1(A)
| ~ v4_group_1(A)
| ~ v6_rlvect_1(A)
| ~ v5_rlvect_1(A)
| ~ v4_rlvect_1(A)
| ~ v3_rlvect_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3457]) ).
fof(f13147,plain,
! [X0,X1,X2,X3] :
( k1_rmod_5(X0,X1,X2) = X3
| k1_rlvect_1(X0) = k2_group_1(X0)
| X2 != u1_struct_0(X3)
| ~ m1_rmod_2(X3,X0,X1)
| ~ v3_vectsp_2(X3,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ l3_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| v10_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f13146]) ).
fof(f13148,plain,
? [A] :
( ? [B] :
( ? [C] :
( k1_rmod_5(A,B,C) != B
& k1_rlvect_1(A) != k2_group_1(A)
& C = u1_struct_0(B)
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
& l1_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& v3_vectsp_2(B,A)
& v6_rlvect_1(B)
& v5_rlvect_1(B)
& v4_rlvect_1(B)
& v3_rlvect_1(B)
& ~ v3_struct_0(B) )
& l3_vectsp_1(A)
& v2_vectsp_2(A)
& ~ v10_vectsp_1(A)
& v8_vectsp_1(A)
& v7_vectsp_1(A)
& v6_vectsp_1(A)
& v7_group_1(A)
& v4_group_1(A)
& v6_rlvect_1(A)
& v5_rlvect_1(A)
& v4_rlvect_1(A)
& v3_rlvect_1(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3459]) ).
fof(f13149,plain,
( k1_rmod_5(sK845_skl,sK846_skl,sK847_skl) != sK846_skl
& k1_rlvect_1(sK845_skl) != k2_group_1(sK845_skl)
& sK847_skl = u1_struct_0(sK846_skl)
& m1_subset_1(sK847_skl,k1_zfmisc_1(u1_struct_0(sK846_skl)))
& l1_vectsp_2(sK846_skl,sK845_skl)
& v5_vectsp_2(sK846_skl,sK845_skl)
& v3_vectsp_2(sK846_skl,sK845_skl)
& v6_rlvect_1(sK846_skl)
& v5_rlvect_1(sK846_skl)
& v4_rlvect_1(sK846_skl)
& v3_rlvect_1(sK846_skl)
& ~ v3_struct_0(sK846_skl)
& l3_vectsp_1(sK845_skl)
& v2_vectsp_2(sK845_skl)
& ~ v10_vectsp_1(sK845_skl)
& v8_vectsp_1(sK845_skl)
& v7_vectsp_1(sK845_skl)
& v6_vectsp_1(sK845_skl)
& v7_group_1(sK845_skl)
& v4_group_1(sK845_skl)
& v6_rlvect_1(sK845_skl)
& v5_rlvect_1(sK845_skl)
& v4_rlvect_1(sK845_skl)
& v3_rlvect_1(sK845_skl)
& ~ v3_struct_0(sK845_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK845_skl,sK846_skl,sK847_skl]),skolemize(A,sK845_skl),skolemize(B,sK846_skl),skolemize(C,sK847_skl)],[f13148]) ).
fof(f13150,plain,
~ v3_struct_0(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13151,plain,
v3_rlvect_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13152,plain,
v4_rlvect_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13153,plain,
v5_rlvect_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13154,plain,
v6_rlvect_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13155,plain,
v4_group_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13156,plain,
v7_group_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13157,plain,
v6_vectsp_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13158,plain,
v7_vectsp_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13159,plain,
v8_vectsp_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13160,plain,
~ v10_vectsp_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13161,plain,
v2_vectsp_2(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13162,plain,
l3_vectsp_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13163,plain,
~ v3_struct_0(sK846_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13164,plain,
v3_rlvect_1(sK846_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13165,plain,
v4_rlvect_1(sK846_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13166,plain,
v5_rlvect_1(sK846_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13167,plain,
v6_rlvect_1(sK846_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13168,plain,
v3_vectsp_2(sK846_skl,sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13169,plain,
v5_vectsp_2(sK846_skl,sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13170,plain,
l1_vectsp_2(sK846_skl,sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13172,plain,
sK847_skl = u1_struct_0(sK846_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13173,plain,
k1_rlvect_1(sK845_skl) != k2_group_1(sK845_skl),
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f13174,plain,
k1_rmod_5(sK845_skl,sK846_skl,sK847_skl) != sK846_skl,
inference(cnf_transformation,[status(thm)],[f13149]) ).
fof(f16311,plain,
! [X0] : m1_subset_1(X0,k1_zfmisc_1(X0)),
inference(forward_demodulation,[status(thm)],[f4451,f4666]) ).
fof(f17853,plain,
! [X0,X1,X2] :
( k1_rmod_5(X0,X1,u1_struct_0(X2)) = X2
| k1_rlvect_1(X0) = k2_group_1(X0)
| ~ m1_rmod_2(X2,X0,X1)
| ~ v3_vectsp_2(X2,X0)
| ~ m1_subset_1(u1_struct_0(X2),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ l3_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| v10_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f13147]) ).
fof(f18632,definition,
( sQ523_spl
<=> v3_struct_0(sK846_skl) ),
introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition]) ).
fof(f18633,plain,
( ~ sQ523_spl
| v3_struct_0(sK846_skl) ),
inference(component_clause,[status(thm)],[f18632]) ).
fof(f18642,plain,
( ~ sQ523_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18633,f13163]) ).
fof(f18643,plain,
~ sQ523_spl,
inference(contradiction_clause,[status(thm)],[f18642]) ).
fof(f18656,definition,
( sQ526_spl
<=> v3_rlvect_1(sK846_skl) ),
introduced(definition,[new_symbols(definition,[sQ526_spl])],[split_symbol_definition]) ).
fof(f18658,plain,
( sQ526_spl
| ~ v3_rlvect_1(sK846_skl) ),
inference(component_clause,[status(thm)],[f18656]) ).
fof(f18659,definition,
( sQ527_spl
<=> v5_rlvect_1(sK846_skl) ),
introduced(definition,[new_symbols(definition,[sQ527_spl])],[split_symbol_definition]) ).
fof(f18661,plain,
( sQ527_spl
| ~ v5_rlvect_1(sK846_skl) ),
inference(component_clause,[status(thm)],[f18659]) ).
fof(f18662,definition,
( sQ528_spl
<=> v6_rlvect_1(sK846_skl) ),
introduced(definition,[new_symbols(definition,[sQ528_spl])],[split_symbol_definition]) ).
fof(f18664,plain,
( sQ528_spl
| ~ v6_rlvect_1(sK846_skl) ),
inference(component_clause,[status(thm)],[f18662]) ).
fof(f18690,definition,
( sQ537_spl
<=> v3_struct_0(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ537_spl])],[split_symbol_definition]) ).
fof(f18691,plain,
( ~ sQ537_spl
| v3_struct_0(sK845_skl) ),
inference(component_clause,[status(thm)],[f18690]) ).
fof(f18693,definition,
( sQ538_spl
<=> v3_rlvect_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ538_spl])],[split_symbol_definition]) ).
fof(f18695,plain,
( sQ538_spl
| ~ v3_rlvect_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18693]) ).
fof(f18696,definition,
( sQ539_spl
<=> v5_rlvect_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ539_spl])],[split_symbol_definition]) ).
fof(f18698,plain,
( sQ539_spl
| ~ v5_rlvect_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18696]) ).
fof(f18699,definition,
( sQ540_spl
<=> v6_rlvect_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ540_spl])],[split_symbol_definition]) ).
fof(f18701,plain,
( sQ540_spl
| ~ v6_rlvect_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18699]) ).
fof(f18702,definition,
( sQ541_spl
<=> v4_group_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ541_spl])],[split_symbol_definition]) ).
fof(f18704,plain,
( sQ541_spl
| ~ v4_group_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18702]) ).
fof(f18705,definition,
( sQ542_spl
<=> v7_group_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ542_spl])],[split_symbol_definition]) ).
fof(f18707,plain,
( sQ542_spl
| ~ v7_group_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18705]) ).
fof(f18708,definition,
( sQ543_spl
<=> v7_vectsp_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ543_spl])],[split_symbol_definition]) ).
fof(f18710,plain,
( sQ543_spl
| ~ v7_vectsp_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18708]) ).
fof(f18711,definition,
( sQ544_spl
<=> v8_vectsp_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ544_spl])],[split_symbol_definition]) ).
fof(f18713,plain,
( sQ544_spl
| ~ v8_vectsp_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18711]) ).
fof(f18717,definition,
( sQ546_spl
<=> v10_vectsp_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ546_spl])],[split_symbol_definition]) ).
fof(f18718,plain,
( ~ sQ546_spl
| v10_vectsp_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18717]) ).
fof(f18720,definition,
( sQ547_spl
<=> l3_vectsp_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ547_spl])],[split_symbol_definition]) ).
fof(f18722,plain,
( sQ547_spl
| ~ l3_vectsp_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18720]) ).
fof(f18723,definition,
( sQ548_spl
<=> v2_vectsp_2(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ548_spl])],[split_symbol_definition]) ).
fof(f18725,plain,
( sQ548_spl
| ~ v2_vectsp_2(sK845_skl) ),
inference(component_clause,[status(thm)],[f18723]) ).
fof(f18727,definition,
( sQ549_spl
<=> v4_rlvect_1(sK846_skl) ),
introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition]) ).
fof(f18729,plain,
( sQ549_spl
| ~ v4_rlvect_1(sK846_skl) ),
inference(component_clause,[status(thm)],[f18727]) ).
fof(f18731,definition,
( sQ550_spl
<=> v4_rlvect_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition]) ).
fof(f18733,plain,
( sQ550_spl
| ~ v4_rlvect_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18731]) ).
fof(f18779,plain,
( ~ sQ546_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18718,f13160]) ).
fof(f18780,plain,
~ sQ546_spl,
inference(contradiction_clause,[status(thm)],[f18779]) ).
fof(f18781,plain,
( sQ538_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18695,f13151]) ).
fof(f18782,plain,
sQ538_spl,
inference(contradiction_clause,[status(thm)],[f18781]) ).
fof(f18783,plain,
( ~ sQ537_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18691,f13150]) ).
fof(f18784,plain,
~ sQ537_spl,
inference(contradiction_clause,[status(thm)],[f18783]) ).
fof(f18785,plain,
( sQ544_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18713,f13159]) ).
fof(f18786,plain,
sQ544_spl,
inference(contradiction_clause,[status(thm)],[f18785]) ).
fof(f18787,plain,
( sQ543_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18710,f13158]) ).
fof(f18788,plain,
sQ543_spl,
inference(contradiction_clause,[status(thm)],[f18787]) ).
fof(f18789,plain,
( sQ542_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18707,f13156]) ).
fof(f18790,plain,
sQ542_spl,
inference(contradiction_clause,[status(thm)],[f18789]) ).
fof(f18791,plain,
( sQ541_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18704,f13155]) ).
fof(f18792,plain,
sQ541_spl,
inference(contradiction_clause,[status(thm)],[f18791]) ).
fof(f18793,plain,
( sQ540_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18701,f13154]) ).
fof(f18794,plain,
sQ540_spl,
inference(contradiction_clause,[status(thm)],[f18793]) ).
fof(f18795,plain,
( sQ539_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18698,f13153]) ).
fof(f18796,plain,
sQ539_spl,
inference(contradiction_clause,[status(thm)],[f18795]) ).
fof(f18797,plain,
( sQ550_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18733,f13152]) ).
fof(f18798,plain,
sQ550_spl,
inference(contradiction_clause,[status(thm)],[f18797]) ).
fof(f18799,plain,
( sQ547_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18722,f13162]) ).
fof(f18800,plain,
sQ547_spl,
inference(contradiction_clause,[status(thm)],[f18799]) ).
fof(f18801,plain,
( sQ526_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18658,f13164]) ).
fof(f18802,plain,
sQ526_spl,
inference(contradiction_clause,[status(thm)],[f18801]) ).
fof(f18803,plain,
( sQ527_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18661,f13166]) ).
fof(f18804,plain,
sQ527_spl,
inference(contradiction_clause,[status(thm)],[f18803]) ).
fof(f18805,plain,
( sQ549_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18729,f13165]) ).
fof(f18806,plain,
sQ549_spl,
inference(contradiction_clause,[status(thm)],[f18805]) ).
fof(f18807,plain,
( sQ528_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18664,f13167]) ).
fof(f18808,plain,
sQ528_spl,
inference(contradiction_clause,[status(thm)],[f18807]) ).
fof(f18880,definition,
( sQ569_spl
<=> v6_vectsp_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ569_spl])],[split_symbol_definition]) ).
fof(f18882,plain,
( sQ569_spl
| ~ v6_vectsp_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18880]) ).
fof(f18883,definition,
( sQ570_spl
<=> v5_vectsp_2(sK846_skl,sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ570_spl])],[split_symbol_definition]) ).
fof(f18885,plain,
( sQ570_spl
| ~ v5_vectsp_2(sK846_skl,sK845_skl) ),
inference(component_clause,[status(thm)],[f18883]) ).
fof(f18886,definition,
( sQ571_spl
<=> l1_vectsp_2(sK846_skl,sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ571_spl])],[split_symbol_definition]) ).
fof(f18888,plain,
( sQ571_spl
| ~ l1_vectsp_2(sK846_skl,sK845_skl) ),
inference(component_clause,[status(thm)],[f18886]) ).
fof(f18889,definition,
( sQ572_spl
<=> v3_vectsp_2(sK846_skl,sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ572_spl])],[split_symbol_definition]) ).
fof(f18891,plain,
( sQ572_spl
| ~ v3_vectsp_2(sK846_skl,sK845_skl) ),
inference(component_clause,[status(thm)],[f18889]) ).
fof(f18895,definition,
( sQ574_spl
<=> k1_rlvect_1(sK845_skl) = k2_group_1(sK845_skl) ),
introduced(definition,[new_symbols(definition,[sQ574_spl])],[split_symbol_definition]) ).
fof(f18896,plain,
( ~ sQ574_spl
| k1_rlvect_1(sK845_skl) = k2_group_1(sK845_skl) ),
inference(component_clause,[status(thm)],[f18895]) ).
fof(f18899,plain,
( ~ sQ574_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18896,f13173]) ).
fof(f18900,plain,
~ sQ574_spl,
inference(contradiction_clause,[status(thm)],[f18899]) ).
fof(f18901,plain,
( sQ572_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18891,f13168]) ).
fof(f18902,plain,
sQ572_spl,
inference(contradiction_clause,[status(thm)],[f18901]) ).
fof(f18903,plain,
( sQ571_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18888,f13170]) ).
fof(f18904,plain,
sQ571_spl,
inference(contradiction_clause,[status(thm)],[f18903]) ).
fof(f18905,plain,
( sQ570_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18885,f13169]) ).
fof(f18906,plain,
sQ570_spl,
inference(contradiction_clause,[status(thm)],[f18905]) ).
fof(f18907,plain,
( sQ569_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18882,f13157]) ).
fof(f18908,plain,
sQ569_spl,
inference(contradiction_clause,[status(thm)],[f18907]) ).
fof(f18909,plain,
( sQ548_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18725,f13161]) ).
fof(f18910,plain,
sQ548_spl,
inference(contradiction_clause,[status(thm)],[f18909]) ).
fof(f18923,definition,
( sQ575_spl
<=> v3_struct_0(sK602_skl) ),
introduced(definition,[new_symbols(definition,[sQ575_spl])],[split_symbol_definition]) ).
fof(f18924,plain,
( ~ sQ575_spl
| v3_struct_0(sK602_skl) ),
inference(component_clause,[status(thm)],[f18923]) ).
fof(f18926,definition,
( sQ576_spl
<=> v3_rlvect_1(sK602_skl) ),
introduced(definition,[new_symbols(definition,[sQ576_spl])],[split_symbol_definition]) ).
fof(f18928,plain,
( sQ576_spl
| ~ v3_rlvect_1(sK602_skl) ),
inference(component_clause,[status(thm)],[f18926]) ).
fof(f18929,definition,
( sQ577_spl
<=> v5_rlvect_1(sK602_skl) ),
introduced(definition,[new_symbols(definition,[sQ577_spl])],[split_symbol_definition]) ).
fof(f18931,plain,
( sQ577_spl
| ~ v5_rlvect_1(sK602_skl) ),
inference(component_clause,[status(thm)],[f18929]) ).
fof(f18932,definition,
( sQ578_spl
<=> v6_rlvect_1(sK602_skl) ),
introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition]) ).
fof(f18934,plain,
( sQ578_spl
| ~ v6_rlvect_1(sK602_skl) ),
inference(component_clause,[status(thm)],[f18932]) ).
fof(f18960,plain,
( sQ578_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18934,f9853]) ).
fof(f18961,plain,
sQ578_spl,
inference(contradiction_clause,[status(thm)],[f18960]) ).
fof(f18962,plain,
( sQ577_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18931,f9852]) ).
fof(f18963,plain,
sQ577_spl,
inference(contradiction_clause,[status(thm)],[f18962]) ).
fof(f18964,plain,
( sQ576_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18928,f9850]) ).
fof(f18965,plain,
sQ576_spl,
inference(contradiction_clause,[status(thm)],[f18964]) ).
fof(f18966,plain,
( ~ sQ575_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18924,f9848]) ).
fof(f18967,plain,
~ sQ575_spl,
inference(contradiction_clause,[status(thm)],[f18966]) ).
fof(f18969,definition,
( sQ587_spl
<=> v4_rlvect_1(sK602_skl) ),
introduced(definition,[new_symbols(definition,[sQ587_spl])],[split_symbol_definition]) ).
fof(f18971,plain,
( sQ587_spl
| ~ v4_rlvect_1(sK602_skl) ),
inference(component_clause,[status(thm)],[f18969]) ).
fof(f18973,plain,
( sQ587_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18971,f9851]) ).
fof(f18974,plain,
sQ587_spl,
inference(contradiction_clause,[status(thm)],[f18973]) ).
fof(f19000,definition,
( sQ588_spl
<=> v3_struct_0(sK603_skl) ),
introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition]) ).
fof(f19001,plain,
( ~ sQ588_spl
| v3_struct_0(sK603_skl) ),
inference(component_clause,[status(thm)],[f19000]) ).
fof(f19003,definition,
( sQ589_spl
<=> v3_rlvect_1(sK603_skl) ),
introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition]) ).
fof(f19005,plain,
( sQ589_spl
| ~ v3_rlvect_1(sK603_skl) ),
inference(component_clause,[status(thm)],[f19003]) ).
fof(f19006,definition,
( sQ590_spl
<=> v5_rlvect_1(sK603_skl) ),
introduced(definition,[new_symbols(definition,[sQ590_spl])],[split_symbol_definition]) ).
fof(f19008,plain,
( sQ590_spl
| ~ v5_rlvect_1(sK603_skl) ),
inference(component_clause,[status(thm)],[f19006]) ).
fof(f19009,definition,
( sQ591_spl
<=> v6_rlvect_1(sK603_skl) ),
introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition]) ).
fof(f19011,plain,
( sQ591_spl
| ~ v6_rlvect_1(sK603_skl) ),
inference(component_clause,[status(thm)],[f19009]) ).
fof(f19037,plain,
( sQ591_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19011,f9861]) ).
fof(f19038,plain,
sQ591_spl,
inference(contradiction_clause,[status(thm)],[f19037]) ).
fof(f19039,plain,
( sQ590_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19008,f9860]) ).
fof(f19040,plain,
sQ590_spl,
inference(contradiction_clause,[status(thm)],[f19039]) ).
fof(f19041,plain,
( sQ589_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19005,f9858]) ).
fof(f19042,plain,
sQ589_spl,
inference(contradiction_clause,[status(thm)],[f19041]) ).
fof(f19043,plain,
( ~ sQ588_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19001,f9856]) ).
fof(f19044,plain,
~ sQ588_spl,
inference(contradiction_clause,[status(thm)],[f19043]) ).
fof(f19046,definition,
( sQ600_spl
<=> v4_rlvect_1(sK603_skl) ),
introduced(definition,[new_symbols(definition,[sQ600_spl])],[split_symbol_definition]) ).
fof(f19048,plain,
( sQ600_spl
| ~ v4_rlvect_1(sK603_skl) ),
inference(component_clause,[status(thm)],[f19046]) ).
fof(f19050,plain,
( sQ600_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19048,f9859]) ).
fof(f19051,plain,
sQ600_spl,
inference(contradiction_clause,[status(thm)],[f19050]) ).
fof(f19055,definition,
( sQ601_spl
<=> v3_struct_0(sK650_skl) ),
introduced(definition,[new_symbols(definition,[sQ601_spl])],[split_symbol_definition]) ).
fof(f19056,plain,
( ~ sQ601_spl
| v3_struct_0(sK650_skl) ),
inference(component_clause,[status(thm)],[f19055]) ).
fof(f19092,plain,
( ~ sQ601_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19056,f10539]) ).
fof(f19093,plain,
~ sQ601_spl,
inference(contradiction_clause,[status(thm)],[f19092]) ).
fof(f19095,definition,
( sQ613_spl
<=> v3_struct_0(sK651_skl) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f19096,plain,
( ~ sQ613_spl
| v3_struct_0(sK651_skl) ),
inference(component_clause,[status(thm)],[f19095]) ).
fof(f19110,definition,
( sQ618_spl
<=> v7_group_1(sK651_skl) ),
introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition]) ).
fof(f19112,plain,
( sQ618_spl
| ~ v7_group_1(sK651_skl) ),
inference(component_clause,[status(thm)],[f19110]) ).
fof(f19132,plain,
( sQ618_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19112,f10551]) ).
fof(f19133,plain,
sQ618_spl,
inference(contradiction_clause,[status(thm)],[f19132]) ).
fof(f19134,plain,
( ~ sQ613_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19096,f10546]) ).
fof(f19135,plain,
~ sQ613_spl,
inference(contradiction_clause,[status(thm)],[f19134]) ).
fof(f19137,definition,
( sQ625_spl
<=> v4_group_1(sK651_skl) ),
introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition]) ).
fof(f19139,plain,
( sQ625_spl
| ~ v4_group_1(sK651_skl) ),
inference(component_clause,[status(thm)],[f19137]) ).
fof(f19141,plain,
( sQ625_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19139,f10550]) ).
fof(f19142,plain,
sQ625_spl,
inference(contradiction_clause,[status(thm)],[f19141]) ).
fof(f19177,definition,
( sQ626_spl
<=> v3_struct_0(k1_vectsp_1) ),
introduced(definition,[new_symbols(definition,[sQ626_spl])],[split_symbol_definition]) ).
fof(f19178,plain,
( ~ sQ626_spl
| v3_struct_0(k1_vectsp_1) ),
inference(component_clause,[status(thm)],[f19177]) ).
fof(f19180,definition,
( sQ627_spl
<=> v3_rlvect_1(k1_vectsp_1) ),
introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition]) ).
fof(f19182,plain,
( sQ627_spl
| ~ v3_rlvect_1(k1_vectsp_1) ),
inference(component_clause,[status(thm)],[f19180]) ).
fof(f19183,definition,
( sQ628_spl
<=> v5_rlvect_1(k1_vectsp_1) ),
introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition]) ).
fof(f19185,plain,
( sQ628_spl
| ~ v5_rlvect_1(k1_vectsp_1) ),
inference(component_clause,[status(thm)],[f19183]) ).
fof(f19186,definition,
( sQ629_spl
<=> v6_rlvect_1(k1_vectsp_1) ),
introduced(definition,[new_symbols(definition,[sQ629_spl])],[split_symbol_definition]) ).
fof(f19188,plain,
( sQ629_spl
| ~ v6_rlvect_1(k1_vectsp_1) ),
inference(component_clause,[status(thm)],[f19186]) ).
fof(f19214,plain,
( sQ629_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19188,f10888]) ).
fof(f19215,plain,
sQ629_spl,
inference(contradiction_clause,[status(thm)],[f19214]) ).
fof(f19216,plain,
( sQ628_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19185,f10887]) ).
fof(f19217,plain,
sQ628_spl,
inference(contradiction_clause,[status(thm)],[f19216]) ).
fof(f19218,plain,
( sQ627_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19182,f10885]) ).
fof(f19219,plain,
sQ627_spl,
inference(contradiction_clause,[status(thm)],[f19218]) ).
fof(f19220,plain,
( ~ sQ626_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19178,f10881]) ).
fof(f19221,plain,
~ sQ626_spl,
inference(contradiction_clause,[status(thm)],[f19220]) ).
fof(f19223,definition,
( sQ638_spl
<=> v4_rlvect_1(k1_vectsp_1) ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f19225,plain,
( sQ638_spl
| ~ v4_rlvect_1(k1_vectsp_1) ),
inference(component_clause,[status(thm)],[f19223]) ).
fof(f19227,plain,
( sQ638_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19225,f10886]) ).
fof(f19228,plain,
sQ638_spl,
inference(contradiction_clause,[status(thm)],[f19227]) ).
fof(f19232,definition,
( sQ639_spl
<=> v3_struct_0(sK677_skl) ),
introduced(definition,[new_symbols(definition,[sQ639_spl])],[split_symbol_definition]) ).
fof(f19233,plain,
( ~ sQ639_spl
| v3_struct_0(sK677_skl) ),
inference(component_clause,[status(thm)],[f19232]) ).
fof(f19235,definition,
( sQ640_spl
<=> v3_rlvect_1(sK677_skl) ),
introduced(definition,[new_symbols(definition,[sQ640_spl])],[split_symbol_definition]) ).
fof(f19237,plain,
( sQ640_spl
| ~ v3_rlvect_1(sK677_skl) ),
inference(component_clause,[status(thm)],[f19235]) ).
fof(f19238,definition,
( sQ641_spl
<=> v5_rlvect_1(sK677_skl) ),
introduced(definition,[new_symbols(definition,[sQ641_spl])],[split_symbol_definition]) ).
fof(f19240,plain,
( sQ641_spl
| ~ v5_rlvect_1(sK677_skl) ),
inference(component_clause,[status(thm)],[f19238]) ).
fof(f19241,definition,
( sQ642_spl
<=> v6_rlvect_1(sK677_skl) ),
introduced(definition,[new_symbols(definition,[sQ642_spl])],[split_symbol_definition]) ).
fof(f19243,plain,
( sQ642_spl
| ~ v6_rlvect_1(sK677_skl) ),
inference(component_clause,[status(thm)],[f19241]) ).
fof(f19269,plain,
( sQ642_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19243,f10896]) ).
fof(f19270,plain,
sQ642_spl,
inference(contradiction_clause,[status(thm)],[f19269]) ).
fof(f19271,plain,
( sQ641_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19240,f10895]) ).
fof(f19272,plain,
sQ641_spl,
inference(contradiction_clause,[status(thm)],[f19271]) ).
fof(f19273,plain,
( sQ640_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19237,f10893]) ).
fof(f19274,plain,
sQ640_spl,
inference(contradiction_clause,[status(thm)],[f19273]) ).
fof(f19275,plain,
( ~ sQ639_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19233,f10891]) ).
fof(f19276,plain,
~ sQ639_spl,
inference(contradiction_clause,[status(thm)],[f19275]) ).
fof(f19278,definition,
( sQ651_spl
<=> v4_rlvect_1(sK677_skl) ),
introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition]) ).
fof(f19280,plain,
( sQ651_spl
| ~ v4_rlvect_1(sK677_skl) ),
inference(component_clause,[status(thm)],[f19278]) ).
fof(f19282,plain,
( sQ651_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19280,f10894]) ).
fof(f19283,plain,
sQ651_spl,
inference(contradiction_clause,[status(thm)],[f19282]) ).
fof(f19325,definition,
( sQ664_spl
<=> v3_struct_0(sK683_skl) ),
introduced(definition,[new_symbols(definition,[sQ664_spl])],[split_symbol_definition]) ).
fof(f19326,plain,
( ~ sQ664_spl
| v3_struct_0(sK683_skl) ),
inference(component_clause,[status(thm)],[f19325]) ).
fof(f19362,plain,
( ~ sQ664_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19326,f10916]) ).
fof(f19363,plain,
~ sQ664_spl,
inference(contradiction_clause,[status(thm)],[f19362]) ).
fof(f19407,definition,
( sQ679_spl
<=> v7_group_1(k3_vectsp_1) ),
introduced(definition,[new_symbols(definition,[sQ679_spl])],[split_symbol_definition]) ).
fof(f19409,plain,
( sQ679_spl
| ~ v7_group_1(k3_vectsp_1) ),
inference(component_clause,[status(thm)],[f19407]) ).
fof(f19411,plain,
( sQ679_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19409,f10930]) ).
fof(f19412,plain,
sQ679_spl,
inference(contradiction_clause,[status(thm)],[f19411]) ).
fof(f19426,definition,
( sQ680_spl
<=> v3_struct_0(sK684_skl) ),
introduced(definition,[new_symbols(definition,[sQ680_spl])],[split_symbol_definition]) ).
fof(f19427,plain,
( ~ sQ680_spl
| v3_struct_0(sK684_skl) ),
inference(component_clause,[status(thm)],[f19426]) ).
fof(f19441,definition,
( sQ685_spl
<=> v7_group_1(sK684_skl) ),
introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition]) ).
fof(f19443,plain,
( sQ685_spl
| ~ v7_group_1(sK684_skl) ),
inference(component_clause,[status(thm)],[f19441]) ).
fof(f19463,plain,
( sQ685_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19443,f10955]) ).
fof(f19464,plain,
sQ685_spl,
inference(contradiction_clause,[status(thm)],[f19463]) ).
fof(f19465,plain,
( ~ sQ680_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19427,f10953]) ).
fof(f19466,plain,
~ sQ680_spl,
inference(contradiction_clause,[status(thm)],[f19465]) ).
fof(f19468,definition,
( sQ692_spl
<=> v4_group_1(sK684_skl) ),
introduced(definition,[new_symbols(definition,[sQ692_spl])],[split_symbol_definition]) ).
fof(f19470,plain,
( sQ692_spl
| ~ v4_group_1(sK684_skl) ),
inference(component_clause,[status(thm)],[f19468]) ).
fof(f19472,plain,
( sQ692_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19470,f10954]) ).
fof(f19473,plain,
sQ692_spl,
inference(contradiction_clause,[status(thm)],[f19472]) ).
fof(f19531,definition,
( sQ693_spl
<=> v3_struct_0(sK685_skl) ),
introduced(definition,[new_symbols(definition,[sQ693_spl])],[split_symbol_definition]) ).
fof(f19532,plain,
( ~ sQ693_spl
| v3_struct_0(sK685_skl) ),
inference(component_clause,[status(thm)],[f19531]) ).
fof(f19546,definition,
( sQ698_spl
<=> v7_group_1(sK685_skl) ),
introduced(definition,[new_symbols(definition,[sQ698_spl])],[split_symbol_definition]) ).
fof(f19548,plain,
( sQ698_spl
| ~ v7_group_1(sK685_skl) ),
inference(component_clause,[status(thm)],[f19546]) ).
fof(f19552,definition,
( sQ700_spl
<=> v8_vectsp_1(sK685_skl) ),
introduced(definition,[new_symbols(definition,[sQ700_spl])],[split_symbol_definition]) ).
fof(f19554,plain,
( sQ700_spl
| ~ v8_vectsp_1(sK685_skl) ),
inference(component_clause,[status(thm)],[f19552]) ).
fof(f19568,plain,
( sQ700_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19554,f10963]) ).
fof(f19569,plain,
sQ700_spl,
inference(contradiction_clause,[status(thm)],[f19568]) ).
fof(f19570,plain,
( sQ698_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19548,f10961]) ).
fof(f19571,plain,
sQ698_spl,
inference(contradiction_clause,[status(thm)],[f19570]) ).
fof(f19572,plain,
( ~ sQ693_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19532,f10958]) ).
fof(f19573,plain,
~ sQ693_spl,
inference(contradiction_clause,[status(thm)],[f19572]) ).
fof(f19575,definition,
( sQ705_spl
<=> v4_group_1(sK685_skl) ),
introduced(definition,[new_symbols(definition,[sQ705_spl])],[split_symbol_definition]) ).
fof(f19577,plain,
( sQ705_spl
| ~ v4_group_1(sK685_skl) ),
inference(component_clause,[status(thm)],[f19575]) ).
fof(f19579,plain,
( sQ705_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19577,f10960]) ).
fof(f19580,plain,
sQ705_spl,
inference(contradiction_clause,[status(thm)],[f19579]) ).
fof(f19584,definition,
( sQ706_spl
<=> v3_struct_0(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ706_spl])],[split_symbol_definition]) ).
fof(f19585,plain,
( ~ sQ706_spl
| v3_struct_0(sK686_skl) ),
inference(component_clause,[status(thm)],[f19584]) ).
fof(f19587,definition,
( sQ707_spl
<=> v3_rlvect_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ707_spl])],[split_symbol_definition]) ).
fof(f19589,plain,
( sQ707_spl
| ~ v3_rlvect_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19587]) ).
fof(f19590,definition,
( sQ708_spl
<=> v4_rlvect_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ708_spl])],[split_symbol_definition]) ).
fof(f19592,plain,
( sQ708_spl
| ~ v4_rlvect_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19590]) ).
fof(f19593,definition,
( sQ709_spl
<=> v5_rlvect_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ709_spl])],[split_symbol_definition]) ).
fof(f19595,plain,
( sQ709_spl
| ~ v5_rlvect_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19593]) ).
fof(f19596,definition,
( sQ710_spl
<=> v6_rlvect_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ710_spl])],[split_symbol_definition]) ).
fof(f19598,plain,
( sQ710_spl
| ~ v6_rlvect_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19596]) ).
fof(f19599,definition,
( sQ711_spl
<=> v4_group_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ711_spl])],[split_symbol_definition]) ).
fof(f19601,plain,
( sQ711_spl
| ~ v4_group_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19599]) ).
fof(f19602,definition,
( sQ712_spl
<=> v7_group_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ712_spl])],[split_symbol_definition]) ).
fof(f19604,plain,
( sQ712_spl
| ~ v7_group_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19602]) ).
fof(f19605,definition,
( sQ713_spl
<=> v7_vectsp_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition]) ).
fof(f19607,plain,
( sQ713_spl
| ~ v7_vectsp_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19605]) ).
fof(f19608,definition,
( sQ714_spl
<=> v8_vectsp_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition]) ).
fof(f19610,plain,
( sQ714_spl
| ~ v8_vectsp_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19608]) ).
fof(f19611,definition,
( sQ715_spl
<=> v9_vectsp_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ715_spl])],[split_symbol_definition]) ).
fof(f19613,plain,
( sQ715_spl
| ~ v9_vectsp_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19611]) ).
fof(f19614,definition,
( sQ716_spl
<=> v10_vectsp_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ716_spl])],[split_symbol_definition]) ).
fof(f19615,plain,
( ~ sQ716_spl
| v10_vectsp_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19614]) ).
fof(f19621,plain,
( ~ sQ716_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19615,f10981]) ).
fof(f19622,plain,
~ sQ716_spl,
inference(contradiction_clause,[status(thm)],[f19621]) ).
fof(f19623,plain,
( sQ715_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19613,f10980]) ).
fof(f19624,plain,
sQ715_spl,
inference(contradiction_clause,[status(thm)],[f19623]) ).
fof(f19625,plain,
( sQ714_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19610,f10979]) ).
fof(f19626,plain,
sQ714_spl,
inference(contradiction_clause,[status(thm)],[f19625]) ).
fof(f19627,plain,
( sQ713_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19607,f10978]) ).
fof(f19628,plain,
sQ713_spl,
inference(contradiction_clause,[status(thm)],[f19627]) ).
fof(f19629,plain,
( sQ712_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19604,f10973]) ).
fof(f19630,plain,
sQ712_spl,
inference(contradiction_clause,[status(thm)],[f19629]) ).
fof(f19631,plain,
( sQ711_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19601,f10972]) ).
fof(f19632,plain,
sQ711_spl,
inference(contradiction_clause,[status(thm)],[f19631]) ).
fof(f19633,plain,
( sQ710_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19598,f10970]) ).
fof(f19634,plain,
sQ710_spl,
inference(contradiction_clause,[status(thm)],[f19633]) ).
fof(f19635,plain,
( sQ709_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19595,f10969]) ).
fof(f19636,plain,
sQ709_spl,
inference(contradiction_clause,[status(thm)],[f19635]) ).
fof(f19637,plain,
( sQ708_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19592,f10968]) ).
fof(f19638,plain,
sQ708_spl,
inference(contradiction_clause,[status(thm)],[f19637]) ).
fof(f19639,plain,
( sQ707_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19589,f10967]) ).
fof(f19640,plain,
sQ707_spl,
inference(contradiction_clause,[status(thm)],[f19639]) ).
fof(f19641,plain,
( ~ sQ706_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19585,f10966]) ).
fof(f19642,plain,
~ sQ706_spl,
inference(contradiction_clause,[status(thm)],[f19641]) ).
fof(f19644,definition,
( sQ718_spl
<=> l3_vectsp_1(sK686_skl) ),
introduced(definition,[new_symbols(definition,[sQ718_spl])],[split_symbol_definition]) ).
fof(f19646,plain,
( sQ718_spl
| ~ l3_vectsp_1(sK686_skl) ),
inference(component_clause,[status(thm)],[f19644]) ).
fof(f19648,plain,
( sQ718_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19646,f10965]) ).
fof(f19649,plain,
sQ718_spl,
inference(contradiction_clause,[status(thm)],[f19648]) ).
fof(f19693,definition,
( sQ722_spl
<=> v3_struct_0(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition]) ).
fof(f19694,plain,
( ~ sQ722_spl
| v3_struct_0(sK691_skl) ),
inference(component_clause,[status(thm)],[f19693]) ).
fof(f19696,definition,
( sQ723_spl
<=> v3_rlvect_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ723_spl])],[split_symbol_definition]) ).
fof(f19698,plain,
( sQ723_spl
| ~ v3_rlvect_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19696]) ).
fof(f19699,definition,
( sQ724_spl
<=> v4_rlvect_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ724_spl])],[split_symbol_definition]) ).
fof(f19701,plain,
( sQ724_spl
| ~ v4_rlvect_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19699]) ).
fof(f19702,definition,
( sQ725_spl
<=> v5_rlvect_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ725_spl])],[split_symbol_definition]) ).
fof(f19704,plain,
( sQ725_spl
| ~ v5_rlvect_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19702]) ).
fof(f19705,definition,
( sQ726_spl
<=> v6_rlvect_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition]) ).
fof(f19707,plain,
( sQ726_spl
| ~ v6_rlvect_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19705]) ).
fof(f19708,definition,
( sQ727_spl
<=> v4_group_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ727_spl])],[split_symbol_definition]) ).
fof(f19710,plain,
( sQ727_spl
| ~ v4_group_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19708]) ).
fof(f19711,definition,
( sQ728_spl
<=> v7_group_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ728_spl])],[split_symbol_definition]) ).
fof(f19713,plain,
( sQ728_spl
| ~ v7_group_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19711]) ).
fof(f19714,definition,
( sQ729_spl
<=> v7_vectsp_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ729_spl])],[split_symbol_definition]) ).
fof(f19716,plain,
( sQ729_spl
| ~ v7_vectsp_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19714]) ).
fof(f19717,definition,
( sQ730_spl
<=> v8_vectsp_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ730_spl])],[split_symbol_definition]) ).
fof(f19719,plain,
( sQ730_spl
| ~ v8_vectsp_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19717]) ).
fof(f19720,definition,
( sQ731_spl
<=> v9_vectsp_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition]) ).
fof(f19722,plain,
( sQ731_spl
| ~ v9_vectsp_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19720]) ).
fof(f19723,definition,
( sQ732_spl
<=> v10_vectsp_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ732_spl])],[split_symbol_definition]) ).
fof(f19724,plain,
( ~ sQ732_spl
| v10_vectsp_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19723]) ).
fof(f19730,plain,
( ~ sQ732_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19724,f11028]) ).
fof(f19731,plain,
~ sQ732_spl,
inference(contradiction_clause,[status(thm)],[f19730]) ).
fof(f19732,plain,
( sQ731_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19722,f11027]) ).
fof(f19733,plain,
sQ731_spl,
inference(contradiction_clause,[status(thm)],[f19732]) ).
fof(f19734,plain,
( sQ730_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19719,f11026]) ).
fof(f19735,plain,
sQ730_spl,
inference(contradiction_clause,[status(thm)],[f19734]) ).
fof(f19736,plain,
( sQ729_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19716,f11025]) ).
fof(f19737,plain,
sQ729_spl,
inference(contradiction_clause,[status(thm)],[f19736]) ).
fof(f19738,plain,
( sQ728_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19713,f11020]) ).
fof(f19739,plain,
sQ728_spl,
inference(contradiction_clause,[status(thm)],[f19738]) ).
fof(f19740,plain,
( sQ727_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19710,f11019]) ).
fof(f19741,plain,
sQ727_spl,
inference(contradiction_clause,[status(thm)],[f19740]) ).
fof(f19742,plain,
( sQ726_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19707,f11017]) ).
fof(f19743,plain,
sQ726_spl,
inference(contradiction_clause,[status(thm)],[f19742]) ).
fof(f19744,plain,
( sQ725_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19704,f11016]) ).
fof(f19745,plain,
sQ725_spl,
inference(contradiction_clause,[status(thm)],[f19744]) ).
fof(f19746,plain,
( sQ724_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19701,f11015]) ).
fof(f19747,plain,
sQ724_spl,
inference(contradiction_clause,[status(thm)],[f19746]) ).
fof(f19748,plain,
( sQ723_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19698,f11014]) ).
fof(f19749,plain,
sQ723_spl,
inference(contradiction_clause,[status(thm)],[f19748]) ).
fof(f19750,plain,
( ~ sQ722_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19694,f11013]) ).
fof(f19751,plain,
~ sQ722_spl,
inference(contradiction_clause,[status(thm)],[f19750]) ).
fof(f19753,definition,
( sQ734_spl
<=> l3_vectsp_1(sK691_skl) ),
introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition]) ).
fof(f19755,plain,
( sQ734_spl
| ~ l3_vectsp_1(sK691_skl) ),
inference(component_clause,[status(thm)],[f19753]) ).
fof(f19757,plain,
( sQ734_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19755,f11012]) ).
fof(f19758,plain,
sQ734_spl,
inference(contradiction_clause,[status(thm)],[f19757]) ).
fof(f19875,definition,
! [X1] :
( sQ744_spl
<=> ~ m1_subset_1(X1,k1_numbers) ),
introduced(definition,[new_symbols(definition,[sQ744_spl])],[split_symbol_definition]) ).
fof(f19876,plain,
! [X0] :
( ~ sQ744_spl
| ~ m1_subset_1(X0,k1_numbers) ),
inference(component_clause,[status(thm)],[f19875]) ).
fof(f19924,definition,
( sQ757_spl
<=> v3_struct_0(sK743_skl) ),
introduced(definition,[new_symbols(definition,[sQ757_spl])],[split_symbol_definition]) ).
fof(f19925,plain,
( ~ sQ757_spl
| v3_struct_0(sK743_skl) ),
inference(component_clause,[status(thm)],[f19924]) ).
fof(f19927,definition,
( sQ758_spl
<=> v3_rlvect_1(sK743_skl) ),
introduced(definition,[new_symbols(definition,[sQ758_spl])],[split_symbol_definition]) ).
fof(f19929,plain,
( sQ758_spl
| ~ v3_rlvect_1(sK743_skl) ),
inference(component_clause,[status(thm)],[f19927]) ).
fof(f19930,definition,
( sQ759_spl
<=> v4_rlvect_1(sK743_skl) ),
introduced(definition,[new_symbols(definition,[sQ759_spl])],[split_symbol_definition]) ).
fof(f19932,plain,
( sQ759_spl
| ~ v4_rlvect_1(sK743_skl) ),
inference(component_clause,[status(thm)],[f19930]) ).
fof(f19933,definition,
( sQ760_spl
<=> v5_rlvect_1(sK743_skl) ),
introduced(definition,[new_symbols(definition,[sQ760_spl])],[split_symbol_definition]) ).
fof(f19935,plain,
( sQ760_spl
| ~ v5_rlvect_1(sK743_skl) ),
inference(component_clause,[status(thm)],[f19933]) ).
fof(f19936,definition,
( sQ761_spl
<=> v6_rlvect_1(sK743_skl) ),
introduced(definition,[new_symbols(definition,[sQ761_spl])],[split_symbol_definition]) ).
fof(f19938,plain,
( sQ761_spl
| ~ v6_rlvect_1(sK743_skl) ),
inference(component_clause,[status(thm)],[f19936]) ).
fof(f19945,definition,
( sQ764_spl
<=> v7_vectsp_1(sK743_skl) ),
introduced(definition,[new_symbols(definition,[sQ764_spl])],[split_symbol_definition]) ).
fof(f19947,plain,
( sQ764_spl
| ~ v7_vectsp_1(sK743_skl) ),
inference(component_clause,[status(thm)],[f19945]) ).
fof(f19948,definition,
( sQ765_spl
<=> v8_vectsp_1(sK743_skl) ),
introduced(definition,[new_symbols(definition,[sQ765_spl])],[split_symbol_definition]) ).
fof(f19950,plain,
( sQ765_spl
| ~ v8_vectsp_1(sK743_skl) ),
inference(component_clause,[status(thm)],[f19948]) ).
fof(f19961,plain,
( sQ765_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19950,f11756]) ).
fof(f19962,plain,
sQ765_spl,
inference(contradiction_clause,[status(thm)],[f19961]) ).
fof(f19963,plain,
( sQ764_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19947,f11755]) ).
fof(f19964,plain,
sQ764_spl,
inference(contradiction_clause,[status(thm)],[f19963]) ).
fof(f19965,plain,
( sQ761_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19938,f11749]) ).
fof(f19966,plain,
sQ761_spl,
inference(contradiction_clause,[status(thm)],[f19965]) ).
fof(f19967,plain,
( sQ760_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19935,f11748]) ).
fof(f19968,plain,
sQ760_spl,
inference(contradiction_clause,[status(thm)],[f19967]) ).
fof(f19969,plain,
( sQ759_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19932,f11747]) ).
fof(f19970,plain,
sQ759_spl,
inference(contradiction_clause,[status(thm)],[f19969]) ).
fof(f19971,plain,
( sQ758_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19929,f11746]) ).
fof(f19972,plain,
sQ758_spl,
inference(contradiction_clause,[status(thm)],[f19971]) ).
fof(f19973,plain,
( ~ sQ757_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19925,f11745]) ).
fof(f19974,plain,
~ sQ757_spl,
inference(contradiction_clause,[status(thm)],[f19973]) ).
fof(f19976,definition,
( sQ769_spl
<=> l3_vectsp_1(sK743_skl) ),
introduced(definition,[new_symbols(definition,[sQ769_spl])],[split_symbol_definition]) ).
fof(f19978,plain,
( sQ769_spl
| ~ l3_vectsp_1(sK743_skl) ),
inference(component_clause,[status(thm)],[f19976]) ).
fof(f19980,plain,
( sQ769_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19978,f11744]) ).
fof(f19981,plain,
sQ769_spl,
inference(contradiction_clause,[status(thm)],[f19980]) ).
fof(f20072,plain,
( ~ sQ744_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8609,f19876]) ).
fof(f20080,plain,
~ sQ744_spl,
inference(contradiction_clause,[status(thm)],[f20072]) ).
fof(f20095,definition,
( sQ776_spl
<=> v3_struct_0(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ776_spl])],[split_symbol_definition]) ).
fof(f20096,plain,
( ~ sQ776_spl
| v3_struct_0(sK744_skl) ),
inference(component_clause,[status(thm)],[f20095]) ).
fof(f20098,definition,
( sQ777_spl
<=> v3_rlvect_1(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ777_spl])],[split_symbol_definition]) ).
fof(f20100,plain,
( sQ777_spl
| ~ v3_rlvect_1(sK744_skl) ),
inference(component_clause,[status(thm)],[f20098]) ).
fof(f20101,definition,
( sQ778_spl
<=> v4_rlvect_1(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ778_spl])],[split_symbol_definition]) ).
fof(f20103,plain,
( sQ778_spl
| ~ v4_rlvect_1(sK744_skl) ),
inference(component_clause,[status(thm)],[f20101]) ).
fof(f20104,definition,
( sQ779_spl
<=> v5_rlvect_1(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ779_spl])],[split_symbol_definition]) ).
fof(f20106,plain,
( sQ779_spl
| ~ v5_rlvect_1(sK744_skl) ),
inference(component_clause,[status(thm)],[f20104]) ).
fof(f20107,definition,
( sQ780_spl
<=> v6_rlvect_1(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ780_spl])],[split_symbol_definition]) ).
fof(f20109,plain,
( sQ780_spl
| ~ v6_rlvect_1(sK744_skl) ),
inference(component_clause,[status(thm)],[f20107]) ).
fof(f20110,definition,
( sQ781_spl
<=> v4_group_1(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ781_spl])],[split_symbol_definition]) ).
fof(f20112,plain,
( sQ781_spl
| ~ v4_group_1(sK744_skl) ),
inference(component_clause,[status(thm)],[f20110]) ).
fof(f20116,definition,
( sQ783_spl
<=> v7_vectsp_1(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ783_spl])],[split_symbol_definition]) ).
fof(f20118,plain,
( sQ783_spl
| ~ v7_vectsp_1(sK744_skl) ),
inference(component_clause,[status(thm)],[f20116]) ).
fof(f20119,definition,
( sQ784_spl
<=> v8_vectsp_1(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ784_spl])],[split_symbol_definition]) ).
fof(f20121,plain,
( sQ784_spl
| ~ v8_vectsp_1(sK744_skl) ),
inference(component_clause,[status(thm)],[f20119]) ).
fof(f20132,plain,
( sQ784_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20121,f11771]) ).
fof(f20133,plain,
sQ784_spl,
inference(contradiction_clause,[status(thm)],[f20132]) ).
fof(f20134,plain,
( sQ783_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20118,f11770]) ).
fof(f20135,plain,
sQ783_spl,
inference(contradiction_clause,[status(thm)],[f20134]) ).
fof(f20136,plain,
( sQ781_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20112,f11765]) ).
fof(f20137,plain,
sQ781_spl,
inference(contradiction_clause,[status(thm)],[f20136]) ).
fof(f20138,plain,
( sQ780_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20109,f11763]) ).
fof(f20139,plain,
sQ780_spl,
inference(contradiction_clause,[status(thm)],[f20138]) ).
fof(f20140,plain,
( sQ779_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20106,f11762]) ).
fof(f20141,plain,
sQ779_spl,
inference(contradiction_clause,[status(thm)],[f20140]) ).
fof(f20142,plain,
( sQ778_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20103,f11761]) ).
fof(f20143,plain,
sQ778_spl,
inference(contradiction_clause,[status(thm)],[f20142]) ).
fof(f20144,plain,
( sQ777_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20100,f11760]) ).
fof(f20145,plain,
sQ777_spl,
inference(contradiction_clause,[status(thm)],[f20144]) ).
fof(f20146,plain,
( ~ sQ776_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20096,f11759]) ).
fof(f20147,plain,
~ sQ776_spl,
inference(contradiction_clause,[status(thm)],[f20146]) ).
fof(f20149,definition,
( sQ788_spl
<=> l3_vectsp_1(sK744_skl) ),
introduced(definition,[new_symbols(definition,[sQ788_spl])],[split_symbol_definition]) ).
fof(f20151,plain,
( sQ788_spl
| ~ l3_vectsp_1(sK744_skl) ),
inference(component_clause,[status(thm)],[f20149]) ).
fof(f20153,plain,
( sQ788_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20151,f11758]) ).
fof(f20154,plain,
sQ788_spl,
inference(contradiction_clause,[status(thm)],[f20153]) ).
fof(f20166,definition,
( sQ789_spl
<=> v3_struct_0(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ789_spl])],[split_symbol_definition]) ).
fof(f20167,plain,
( ~ sQ789_spl
| v3_struct_0(sK745_skl) ),
inference(component_clause,[status(thm)],[f20166]) ).
fof(f20169,definition,
( sQ790_spl
<=> v3_rlvect_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ790_spl])],[split_symbol_definition]) ).
fof(f20171,plain,
( sQ790_spl
| ~ v3_rlvect_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20169]) ).
fof(f20172,definition,
( sQ791_spl
<=> v4_rlvect_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ791_spl])],[split_symbol_definition]) ).
fof(f20174,plain,
( sQ791_spl
| ~ v4_rlvect_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20172]) ).
fof(f20175,definition,
( sQ792_spl
<=> v5_rlvect_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ792_spl])],[split_symbol_definition]) ).
fof(f20177,plain,
( sQ792_spl
| ~ v5_rlvect_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20175]) ).
fof(f20178,definition,
( sQ793_spl
<=> v6_rlvect_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ793_spl])],[split_symbol_definition]) ).
fof(f20180,plain,
( sQ793_spl
| ~ v6_rlvect_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20178]) ).
fof(f20181,definition,
( sQ794_spl
<=> v4_group_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ794_spl])],[split_symbol_definition]) ).
fof(f20183,plain,
( sQ794_spl
| ~ v4_group_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20181]) ).
fof(f20184,definition,
( sQ795_spl
<=> v7_group_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ795_spl])],[split_symbol_definition]) ).
fof(f20186,plain,
( sQ795_spl
| ~ v7_group_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20184]) ).
fof(f20187,definition,
( sQ796_spl
<=> v7_vectsp_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ796_spl])],[split_symbol_definition]) ).
fof(f20189,plain,
( sQ796_spl
| ~ v7_vectsp_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20187]) ).
fof(f20190,definition,
( sQ797_spl
<=> v8_vectsp_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ797_spl])],[split_symbol_definition]) ).
fof(f20192,plain,
( sQ797_spl
| ~ v8_vectsp_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20190]) ).
fof(f20203,plain,
( sQ797_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20192,f11786]) ).
fof(f20204,plain,
sQ797_spl,
inference(contradiction_clause,[status(thm)],[f20203]) ).
fof(f20205,plain,
( sQ796_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20189,f11785]) ).
fof(f20206,plain,
sQ796_spl,
inference(contradiction_clause,[status(thm)],[f20205]) ).
fof(f20207,plain,
( sQ795_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20186,f11781]) ).
fof(f20208,plain,
sQ795_spl,
inference(contradiction_clause,[status(thm)],[f20207]) ).
fof(f20209,plain,
( sQ794_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20183,f11780]) ).
fof(f20210,plain,
sQ794_spl,
inference(contradiction_clause,[status(thm)],[f20209]) ).
fof(f20211,plain,
( sQ793_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20180,f11778]) ).
fof(f20212,plain,
sQ793_spl,
inference(contradiction_clause,[status(thm)],[f20211]) ).
fof(f20213,plain,
( sQ792_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20177,f11777]) ).
fof(f20214,plain,
sQ792_spl,
inference(contradiction_clause,[status(thm)],[f20213]) ).
fof(f20215,plain,
( sQ791_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20174,f11776]) ).
fof(f20216,plain,
sQ791_spl,
inference(contradiction_clause,[status(thm)],[f20215]) ).
fof(f20217,plain,
( sQ790_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20171,f11775]) ).
fof(f20218,plain,
sQ790_spl,
inference(contradiction_clause,[status(thm)],[f20217]) ).
fof(f20219,plain,
( ~ sQ789_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20167,f11774]) ).
fof(f20220,plain,
~ sQ789_spl,
inference(contradiction_clause,[status(thm)],[f20219]) ).
fof(f20222,definition,
( sQ801_spl
<=> l3_vectsp_1(sK745_skl) ),
introduced(definition,[new_symbols(definition,[sQ801_spl])],[split_symbol_definition]) ).
fof(f20224,plain,
( sQ801_spl
| ~ l3_vectsp_1(sK745_skl) ),
inference(component_clause,[status(thm)],[f20222]) ).
fof(f20226,plain,
( sQ801_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20224,f11773]) ).
fof(f20227,plain,
sQ801_spl,
inference(contradiction_clause,[status(thm)],[f20226]) ).
fof(f20309,definition,
( sQ805_spl
<=> v3_struct_0(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ805_spl])],[split_symbol_definition]) ).
fof(f20310,plain,
( ~ sQ805_spl
| v3_struct_0(sK746_skl) ),
inference(component_clause,[status(thm)],[f20309]) ).
fof(f20312,definition,
( sQ806_spl
<=> v3_rlvect_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ806_spl])],[split_symbol_definition]) ).
fof(f20314,plain,
( sQ806_spl
| ~ v3_rlvect_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20312]) ).
fof(f20315,definition,
( sQ807_spl
<=> v4_rlvect_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ807_spl])],[split_symbol_definition]) ).
fof(f20317,plain,
( sQ807_spl
| ~ v4_rlvect_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20315]) ).
fof(f20318,definition,
( sQ808_spl
<=> v5_rlvect_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ808_spl])],[split_symbol_definition]) ).
fof(f20320,plain,
( sQ808_spl
| ~ v5_rlvect_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20318]) ).
fof(f20321,definition,
( sQ809_spl
<=> v6_rlvect_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ809_spl])],[split_symbol_definition]) ).
fof(f20323,plain,
( sQ809_spl
| ~ v6_rlvect_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20321]) ).
fof(f20324,definition,
( sQ810_spl
<=> v4_group_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ810_spl])],[split_symbol_definition]) ).
fof(f20326,plain,
( sQ810_spl
| ~ v4_group_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20324]) ).
fof(f20327,definition,
( sQ811_spl
<=> v7_group_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ811_spl])],[split_symbol_definition]) ).
fof(f20329,plain,
( sQ811_spl
| ~ v7_group_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20327]) ).
fof(f20330,definition,
( sQ812_spl
<=> v7_vectsp_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ812_spl])],[split_symbol_definition]) ).
fof(f20332,plain,
( sQ812_spl
| ~ v7_vectsp_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20330]) ).
fof(f20333,definition,
( sQ813_spl
<=> v8_vectsp_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ813_spl])],[split_symbol_definition]) ).
fof(f20335,plain,
( sQ813_spl
| ~ v8_vectsp_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20333]) ).
fof(f20346,plain,
( sQ813_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20335,f11802]) ).
fof(f20347,plain,
sQ813_spl,
inference(contradiction_clause,[status(thm)],[f20346]) ).
fof(f20348,plain,
( sQ812_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20332,f11801]) ).
fof(f20349,plain,
sQ812_spl,
inference(contradiction_clause,[status(thm)],[f20348]) ).
fof(f20350,plain,
( sQ811_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20329,f11796]) ).
fof(f20351,plain,
sQ811_spl,
inference(contradiction_clause,[status(thm)],[f20350]) ).
fof(f20352,plain,
( sQ810_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20326,f11795]) ).
fof(f20353,plain,
sQ810_spl,
inference(contradiction_clause,[status(thm)],[f20352]) ).
fof(f20354,plain,
( sQ809_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20323,f11793]) ).
fof(f20355,plain,
sQ809_spl,
inference(contradiction_clause,[status(thm)],[f20354]) ).
fof(f20356,plain,
( sQ808_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20320,f11792]) ).
fof(f20357,plain,
sQ808_spl,
inference(contradiction_clause,[status(thm)],[f20356]) ).
fof(f20358,plain,
( sQ807_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20317,f11791]) ).
fof(f20359,plain,
sQ807_spl,
inference(contradiction_clause,[status(thm)],[f20358]) ).
fof(f20360,plain,
( sQ806_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20314,f11790]) ).
fof(f20361,plain,
sQ806_spl,
inference(contradiction_clause,[status(thm)],[f20360]) ).
fof(f20362,plain,
( ~ sQ805_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20310,f11789]) ).
fof(f20363,plain,
~ sQ805_spl,
inference(contradiction_clause,[status(thm)],[f20362]) ).
fof(f20365,definition,
( sQ817_spl
<=> l3_vectsp_1(sK746_skl) ),
introduced(definition,[new_symbols(definition,[sQ817_spl])],[split_symbol_definition]) ).
fof(f20367,plain,
( sQ817_spl
| ~ l3_vectsp_1(sK746_skl) ),
inference(component_clause,[status(thm)],[f20365]) ).
fof(f20369,plain,
( sQ817_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20367,f11788]) ).
fof(f20370,plain,
sQ817_spl,
inference(contradiction_clause,[status(thm)],[f20369]) ).
fof(f20419,definition,
( sQ822_spl
<=> m1_subset_1(k1_xboole_0,k1_zfmisc_1(sK847_skl)) ),
introduced(definition,[new_symbols(definition,[sQ822_spl])],[split_symbol_definition]) ).
fof(f20421,plain,
( sQ822_spl
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(sK847_skl)) ),
inference(component_clause,[status(thm)],[f20419]) ).
fof(f20432,plain,
( sQ822_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20421,f4452]) ).
fof(f20433,plain,
sQ822_spl,
inference(contradiction_clause,[status(thm)],[f20432]) ).
fof(f20553,definition,
( sQ829_spl
<=> v3_struct_0(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ829_spl])],[split_symbol_definition]) ).
fof(f20554,plain,
( ~ sQ829_spl
| v3_struct_0(sK747_skl) ),
inference(component_clause,[status(thm)],[f20553]) ).
fof(f20556,definition,
( sQ830_spl
<=> v3_rlvect_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ830_spl])],[split_symbol_definition]) ).
fof(f20558,plain,
( sQ830_spl
| ~ v3_rlvect_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20556]) ).
fof(f20559,definition,
( sQ831_spl
<=> v4_rlvect_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ831_spl])],[split_symbol_definition]) ).
fof(f20561,plain,
( sQ831_spl
| ~ v4_rlvect_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20559]) ).
fof(f20562,definition,
( sQ832_spl
<=> v5_rlvect_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ832_spl])],[split_symbol_definition]) ).
fof(f20564,plain,
( sQ832_spl
| ~ v5_rlvect_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20562]) ).
fof(f20565,definition,
( sQ833_spl
<=> v6_rlvect_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ833_spl])],[split_symbol_definition]) ).
fof(f20567,plain,
( sQ833_spl
| ~ v6_rlvect_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20565]) ).
fof(f20568,definition,
( sQ834_spl
<=> v4_group_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ834_spl])],[split_symbol_definition]) ).
fof(f20570,plain,
( sQ834_spl
| ~ v4_group_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20568]) ).
fof(f20571,definition,
( sQ835_spl
<=> v7_group_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ835_spl])],[split_symbol_definition]) ).
fof(f20573,plain,
( sQ835_spl
| ~ v7_group_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20571]) ).
fof(f20574,definition,
( sQ836_spl
<=> v7_vectsp_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ836_spl])],[split_symbol_definition]) ).
fof(f20576,plain,
( sQ836_spl
| ~ v7_vectsp_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20574]) ).
fof(f20577,definition,
( sQ837_spl
<=> v8_vectsp_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ837_spl])],[split_symbol_definition]) ).
fof(f20579,plain,
( sQ837_spl
| ~ v8_vectsp_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20577]) ).
fof(f20583,definition,
( sQ839_spl
<=> v10_vectsp_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ839_spl])],[split_symbol_definition]) ).
fof(f20584,plain,
( ~ sQ839_spl
| v10_vectsp_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20583]) ).
fof(f20590,plain,
( ~ sQ839_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20584,f11819]) ).
fof(f20591,plain,
~ sQ839_spl,
inference(contradiction_clause,[status(thm)],[f20590]) ).
fof(f20592,plain,
( sQ837_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20579,f11818]) ).
fof(f20593,plain,
sQ837_spl,
inference(contradiction_clause,[status(thm)],[f20592]) ).
fof(f20594,plain,
( sQ836_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20576,f11817]) ).
fof(f20595,plain,
sQ836_spl,
inference(contradiction_clause,[status(thm)],[f20594]) ).
fof(f20596,plain,
( sQ835_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20573,f11812]) ).
fof(f20597,plain,
sQ835_spl,
inference(contradiction_clause,[status(thm)],[f20596]) ).
fof(f20598,plain,
( sQ834_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20570,f11811]) ).
fof(f20599,plain,
sQ834_spl,
inference(contradiction_clause,[status(thm)],[f20598]) ).
fof(f20600,plain,
( sQ833_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20567,f11809]) ).
fof(f20601,plain,
sQ833_spl,
inference(contradiction_clause,[status(thm)],[f20600]) ).
fof(f20602,plain,
( sQ832_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20564,f11808]) ).
fof(f20603,plain,
sQ832_spl,
inference(contradiction_clause,[status(thm)],[f20602]) ).
fof(f20604,plain,
( sQ831_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20561,f11807]) ).
fof(f20605,plain,
sQ831_spl,
inference(contradiction_clause,[status(thm)],[f20604]) ).
fof(f20606,plain,
( sQ830_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20558,f11806]) ).
fof(f20607,plain,
sQ830_spl,
inference(contradiction_clause,[status(thm)],[f20606]) ).
fof(f20608,plain,
( ~ sQ829_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20554,f11805]) ).
fof(f20609,plain,
~ sQ829_spl,
inference(contradiction_clause,[status(thm)],[f20608]) ).
fof(f20611,definition,
( sQ841_spl
<=> l3_vectsp_1(sK747_skl) ),
introduced(definition,[new_symbols(definition,[sQ841_spl])],[split_symbol_definition]) ).
fof(f20613,plain,
( sQ841_spl
| ~ l3_vectsp_1(sK747_skl) ),
inference(component_clause,[status(thm)],[f20611]) ).
fof(f20615,plain,
( sQ841_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20613,f11804]) ).
fof(f20616,plain,
sQ841_spl,
inference(contradiction_clause,[status(thm)],[f20615]) ).
fof(f20743,definition,
( sQ848_spl
<=> v3_struct_0(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ848_spl])],[split_symbol_definition]) ).
fof(f20744,plain,
( ~ sQ848_spl
| v3_struct_0(sK748_skl) ),
inference(component_clause,[status(thm)],[f20743]) ).
fof(f20746,definition,
( sQ849_spl
<=> v3_rlvect_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ849_spl])],[split_symbol_definition]) ).
fof(f20748,plain,
( sQ849_spl
| ~ v3_rlvect_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20746]) ).
fof(f20749,definition,
( sQ850_spl
<=> v4_rlvect_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ850_spl])],[split_symbol_definition]) ).
fof(f20751,plain,
( sQ850_spl
| ~ v4_rlvect_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20749]) ).
fof(f20752,definition,
( sQ851_spl
<=> v5_rlvect_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ851_spl])],[split_symbol_definition]) ).
fof(f20754,plain,
( sQ851_spl
| ~ v5_rlvect_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20752]) ).
fof(f20755,definition,
( sQ852_spl
<=> v6_rlvect_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ852_spl])],[split_symbol_definition]) ).
fof(f20757,plain,
( sQ852_spl
| ~ v6_rlvect_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20755]) ).
fof(f20758,definition,
( sQ853_spl
<=> v4_group_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ853_spl])],[split_symbol_definition]) ).
fof(f20760,plain,
( sQ853_spl
| ~ v4_group_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20758]) ).
fof(f20764,definition,
( sQ855_spl
<=> v7_vectsp_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ855_spl])],[split_symbol_definition]) ).
fof(f20766,plain,
( sQ855_spl
| ~ v7_vectsp_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20764]) ).
fof(f20767,definition,
( sQ856_spl
<=> v8_vectsp_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ856_spl])],[split_symbol_definition]) ).
fof(f20769,plain,
( sQ856_spl
| ~ v8_vectsp_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20767]) ).
fof(f20770,definition,
( sQ857_spl
<=> v9_vectsp_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ857_spl])],[split_symbol_definition]) ).
fof(f20772,plain,
( sQ857_spl
| ~ v9_vectsp_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20770]) ).
fof(f20773,definition,
( sQ858_spl
<=> v10_vectsp_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ858_spl])],[split_symbol_definition]) ).
fof(f20774,plain,
( ~ sQ858_spl
| v10_vectsp_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20773]) ).
fof(f20780,plain,
( ~ sQ858_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20774,f11836]) ).
fof(f20781,plain,
~ sQ858_spl,
inference(contradiction_clause,[status(thm)],[f20780]) ).
fof(f20782,plain,
( sQ857_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20772,f11835]) ).
fof(f20783,plain,
sQ857_spl,
inference(contradiction_clause,[status(thm)],[f20782]) ).
fof(f20784,plain,
( sQ856_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20769,f11834]) ).
fof(f20785,plain,
sQ856_spl,
inference(contradiction_clause,[status(thm)],[f20784]) ).
fof(f20786,plain,
( sQ855_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20766,f11833]) ).
fof(f20787,plain,
sQ855_spl,
inference(contradiction_clause,[status(thm)],[f20786]) ).
fof(f20788,plain,
( sQ853_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20760,f11829]) ).
fof(f20789,plain,
sQ853_spl,
inference(contradiction_clause,[status(thm)],[f20788]) ).
fof(f20790,plain,
( sQ852_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20757,f11827]) ).
fof(f20791,plain,
sQ852_spl,
inference(contradiction_clause,[status(thm)],[f20790]) ).
fof(f20792,plain,
( sQ851_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20754,f11826]) ).
fof(f20793,plain,
sQ851_spl,
inference(contradiction_clause,[status(thm)],[f20792]) ).
fof(f20794,plain,
( sQ850_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20751,f11825]) ).
fof(f20795,plain,
sQ850_spl,
inference(contradiction_clause,[status(thm)],[f20794]) ).
fof(f20796,plain,
( sQ849_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20748,f11824]) ).
fof(f20797,plain,
sQ849_spl,
inference(contradiction_clause,[status(thm)],[f20796]) ).
fof(f20798,plain,
( ~ sQ848_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20744,f11823]) ).
fof(f20799,plain,
~ sQ848_spl,
inference(contradiction_clause,[status(thm)],[f20798]) ).
fof(f20801,definition,
( sQ860_spl
<=> l3_vectsp_1(sK748_skl) ),
introduced(definition,[new_symbols(definition,[sQ860_spl])],[split_symbol_definition]) ).
fof(f20803,plain,
( sQ860_spl
| ~ l3_vectsp_1(sK748_skl) ),
inference(component_clause,[status(thm)],[f20801]) ).
fof(f20805,plain,
( sQ860_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20803,f11822]) ).
fof(f20806,plain,
sQ860_spl,
inference(contradiction_clause,[status(thm)],[f20805]) ).
fof(f20978,definition,
( sQ867_spl
<=> v3_struct_0(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ867_spl])],[split_symbol_definition]) ).
fof(f20979,plain,
( ~ sQ867_spl
| v3_struct_0(sK749_skl) ),
inference(component_clause,[status(thm)],[f20978]) ).
fof(f20981,definition,
( sQ868_spl
<=> v3_rlvect_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ868_spl])],[split_symbol_definition]) ).
fof(f20983,plain,
( sQ868_spl
| ~ v3_rlvect_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f20981]) ).
fof(f20984,definition,
( sQ869_spl
<=> v4_rlvect_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ869_spl])],[split_symbol_definition]) ).
fof(f20986,plain,
( sQ869_spl
| ~ v4_rlvect_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f20984]) ).
fof(f20987,definition,
( sQ870_spl
<=> v5_rlvect_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ870_spl])],[split_symbol_definition]) ).
fof(f20989,plain,
( sQ870_spl
| ~ v5_rlvect_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f20987]) ).
fof(f20990,definition,
( sQ871_spl
<=> v6_rlvect_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ871_spl])],[split_symbol_definition]) ).
fof(f20992,plain,
( sQ871_spl
| ~ v6_rlvect_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f20990]) ).
fof(f20993,definition,
( sQ872_spl
<=> v4_group_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ872_spl])],[split_symbol_definition]) ).
fof(f20995,plain,
( sQ872_spl
| ~ v4_group_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f20993]) ).
fof(f20999,definition,
( sQ874_spl
<=> v7_vectsp_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ874_spl])],[split_symbol_definition]) ).
fof(f21001,plain,
( sQ874_spl
| ~ v7_vectsp_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f20999]) ).
fof(f21002,definition,
( sQ875_spl
<=> v8_vectsp_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ875_spl])],[split_symbol_definition]) ).
fof(f21004,plain,
( sQ875_spl
| ~ v8_vectsp_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f21002]) ).
fof(f21005,definition,
( sQ876_spl
<=> v9_vectsp_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ876_spl])],[split_symbol_definition]) ).
fof(f21007,plain,
( sQ876_spl
| ~ v9_vectsp_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f21005]) ).
fof(f21008,definition,
( sQ877_spl
<=> v10_vectsp_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ877_spl])],[split_symbol_definition]) ).
fof(f21009,plain,
( ~ sQ877_spl
| v10_vectsp_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f21008]) ).
fof(f21015,plain,
( ~ sQ877_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21009,f11853]) ).
fof(f21016,plain,
~ sQ877_spl,
inference(contradiction_clause,[status(thm)],[f21015]) ).
fof(f21017,plain,
( sQ876_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21007,f11852]) ).
fof(f21018,plain,
sQ876_spl,
inference(contradiction_clause,[status(thm)],[f21017]) ).
fof(f21019,plain,
( sQ875_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21004,f11851]) ).
fof(f21020,plain,
sQ875_spl,
inference(contradiction_clause,[status(thm)],[f21019]) ).
fof(f21021,plain,
( sQ874_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21001,f11850]) ).
fof(f21022,plain,
sQ874_spl,
inference(contradiction_clause,[status(thm)],[f21021]) ).
fof(f21023,plain,
( sQ872_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20995,f11845]) ).
fof(f21024,plain,
sQ872_spl,
inference(contradiction_clause,[status(thm)],[f21023]) ).
fof(f21025,plain,
( sQ871_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20992,f11843]) ).
fof(f21026,plain,
sQ871_spl,
inference(contradiction_clause,[status(thm)],[f21025]) ).
fof(f21027,plain,
( sQ870_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20989,f11842]) ).
fof(f21028,plain,
sQ870_spl,
inference(contradiction_clause,[status(thm)],[f21027]) ).
fof(f21029,plain,
( sQ869_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20986,f11841]) ).
fof(f21030,plain,
sQ869_spl,
inference(contradiction_clause,[status(thm)],[f21029]) ).
fof(f21031,plain,
( sQ868_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20983,f11840]) ).
fof(f21032,plain,
sQ868_spl,
inference(contradiction_clause,[status(thm)],[f21031]) ).
fof(f21033,plain,
( ~ sQ867_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20979,f11839]) ).
fof(f21034,plain,
~ sQ867_spl,
inference(contradiction_clause,[status(thm)],[f21033]) ).
fof(f21036,definition,
( sQ879_spl
<=> l3_vectsp_1(sK749_skl) ),
introduced(definition,[new_symbols(definition,[sQ879_spl])],[split_symbol_definition]) ).
fof(f21038,plain,
( sQ879_spl
| ~ l3_vectsp_1(sK749_skl) ),
inference(component_clause,[status(thm)],[f21036]) ).
fof(f21040,plain,
( sQ879_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21038,f11838]) ).
fof(f21041,plain,
sQ879_spl,
inference(contradiction_clause,[status(thm)],[f21040]) ).
fof(f22019,plain,
! [X0,X1] :
( k1_rmod_5(X0,X1,u1_struct_0(X1)) = X1
| k1_rlvect_1(X0) = k2_group_1(X0)
| ~ m1_rmod_2(X1,X0,X1)
| ~ v3_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ l3_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| v10_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f16311,f17853]) ).
fof(f22025,plain,
! [X0,X1] :
( k1_rmod_5(X0,X1,u1_struct_0(X1)) = X1
| k1_rlvect_1(X0) = k2_group_1(X0)
| ~ v3_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ l3_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| v10_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f22019,f12356]) ).
fof(f22109,plain,
! [X0] :
( k1_rmod_5(X0,sK846_skl,sK847_skl) = sK846_skl
| k1_rlvect_1(X0) = k2_group_1(X0)
| ~ v3_vectsp_2(sK846_skl,X0)
| ~ l1_vectsp_2(sK846_skl,X0)
| ~ v5_vectsp_2(sK846_skl,X0)
| ~ v6_rlvect_1(sK846_skl)
| ~ v5_rlvect_1(sK846_skl)
| ~ v4_rlvect_1(sK846_skl)
| ~ v3_rlvect_1(sK846_skl)
| v3_struct_0(sK846_skl)
| ~ l3_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| v10_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ),
inference(paramodulation,[status(thm)],[f13172,f22025]) ).
fof(f22110,definition,
! [X0] :
( sQ901_spl
<=> ( k1_rmod_5(X0,sK846_skl,sK847_skl) = sK846_skl
| k1_rlvect_1(X0) = k2_group_1(X0)
| ~ v3_vectsp_2(sK846_skl,X0)
| ~ l1_vectsp_2(sK846_skl,X0)
| ~ v5_vectsp_2(sK846_skl,X0)
| ~ l3_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| v10_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ901_spl])],[split_symbol_definition]) ).
fof(f22111,plain,
! [X0] :
( ~ sQ901_spl
| k1_rmod_5(X0,sK846_skl,sK847_skl) = sK846_skl
| k1_rlvect_1(X0) = k2_group_1(X0)
| ~ v3_vectsp_2(sK846_skl,X0)
| ~ l1_vectsp_2(sK846_skl,X0)
| ~ v5_vectsp_2(sK846_skl,X0)
| ~ l3_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| v10_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_group_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f22110]) ).
fof(f22113,plain,
( ~ sQ528_spl
| ~ sQ527_spl
| ~ sQ549_spl
| ~ sQ526_spl
| sQ523_spl
| sQ901_spl ),
inference(split_clause,[status(thm)],[f22109,f22110,f18632,f18656,f18727,f18659,f18662]) ).
fof(f22114,plain,
( ~ sQ901_spl
| k1_rlvect_1(sK845_skl) = k2_group_1(sK845_skl)
| ~ v3_vectsp_2(sK846_skl,sK845_skl)
| ~ l1_vectsp_2(sK846_skl,sK845_skl)
| ~ v5_vectsp_2(sK846_skl,sK845_skl)
| ~ l3_vectsp_1(sK845_skl)
| ~ v2_vectsp_2(sK845_skl)
| v10_vectsp_1(sK845_skl)
| ~ v8_vectsp_1(sK845_skl)
| ~ v7_vectsp_1(sK845_skl)
| ~ v6_vectsp_1(sK845_skl)
| ~ v7_group_1(sK845_skl)
| ~ v4_group_1(sK845_skl)
| ~ v6_rlvect_1(sK845_skl)
| ~ v5_rlvect_1(sK845_skl)
| ~ v4_rlvect_1(sK845_skl)
| ~ v3_rlvect_1(sK845_skl)
| v3_struct_0(sK845_skl) ),
inference(resolution,[status(thm)],[f22111,f13174]) ).
fof(f22115,plain,
( ~ sQ901_spl
| sQ574_spl
| ~ sQ572_spl
| ~ sQ571_spl
| ~ sQ570_spl
| ~ sQ547_spl
| ~ sQ548_spl
| sQ546_spl
| ~ sQ544_spl
| ~ sQ543_spl
| ~ sQ569_spl
| ~ sQ542_spl
| ~ sQ541_spl
| ~ sQ540_spl
| ~ sQ539_spl
| ~ sQ550_spl
| ~ sQ538_spl
| sQ537_spl ),
inference(split_clause,[status(thm)],[f22114,f18690,f18693,f18731,f18696,f18699,f18702,f18705,f18880,f18708,f18711,f18717,f18723,f18720,f18883,f18886,f18889,f18895,f22110]) ).
fof(f22116,plain,
$false,
inference(sat_refutation,[status(thm)],[f18643,f18780,f18782,f18784,f18786,f18788,f18790,f18792,f18794,f18796,f18798,f18800,f18802,f18804,f18806,f18808,f18900,f18902,f18904,f18906,f18908,f18910,f18961,f18963,f18965,f18967,f18974,f19038,f19040,f19042,f19044,f19051,f19093,f19133,f19135,f19142,f19215,f19217,f19219,f19221,f19228,f19270,f19272,f19274,f19276,f19283,f19363,f19412,f19464,f19466,f19473,f19569,f19571,f19573,f19580,f19622,f19624,f19626,f19628,f19630,f19632,f19634,f19636,f19638,f19640,f19642,f19649,f19731,f19733,f19735,f19737,f19739,f19741,f19743,f19745,f19747,f19749,f19751,f19758,f19962,f19964,f19966,f19968,f19970,f19972,f19974,f19981,f20080,f20133,f20135,f20137,f20139,f20141,f20143,f20145,f20147,f20154,f20204,f20206,f20208,f20210,f20212,f20214,f20216,f20218,f20220,f20227,f20347,f20349,f20351,f20353,f20355,f20357,f20359,f20361,f20363,f20370,f20433,f20591,f20593,f20595,f20597,f20599,f20601,f20603,f20605,f20607,f20609,f20616,f20781,f20783,f20785,f20787,f20789,f20791,f20793,f20795,f20797,f20799,f20806,f21016,f21018,f21020,f21022,f21024,f21026,f21028,f21030,f21032,f21034,f21041,f22113,f22115]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG219+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n011.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 13:03:42 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.45/0.72 % Drodi V4.1.1
% 267.25/34.77 % Refutation found
% 267.25/34.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 267.25/34.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.89/35.03 % Elapsed time: 34.649805 seconds
% 15.89/35.03 % CPU time: 270.150277 seconds
% 15.89/35.03 % Total memory used: 1.161 GB
% 15.89/35.03 % Net memory used: 1.094 GB
%------------------------------------------------------------------------------