%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG222+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:49:51 AM UTC 2026
% Result : Theorem 29.66s 4.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG222+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.63 % Computer : n026.cluster.edu
% 0.16/0.63 % Model : x86_64 x86_64
% 0.16/0.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.63 % Memory : 8046.5625MB
% 0.16/0.63 % OS : Linux 6.8.0-71-generic
% 0.16/0.63 % CPULimit : 300
% 0.16/0.63 % WCLimit : 300
% 0.16/0.63 % DateTime : Mon Sep 21 13:07:39 UTC 2026
% 0.16/0.63 % CPUTime :
% 0.20/0.66 % Drodi V4.1.1
% 29.66/4.46 % Refutation found
% 29.66/4.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 29.66/4.46 % SZS output start CNFRefutation for theBenchmark
% 29.66/4.46 fof(f1,conjecture,(
% 29.66/4.46 (! [A] :( ( ~ v3_struct_0(A)& v3_rlvect_1(A)& v4_rlvect_1(A)& v5_rlvect_1(A)& v6_rlvect_1(A)& v4_group_1(A)& v7_group_1(A)& v6_vectsp_1(A)& v7_vectsp_1(A)& v8_vectsp_1(A)& ~ v10_vectsp_1(A)& v2_vectsp_2(A)& l3_vectsp_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_rlvect_1(B)& v4_rlvect_1(B)& v5_rlvect_1(B)& v6_rlvect_1(B)& v5_vectsp_2(B,A)& l1_vectsp_2(B,A) )=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))=> m1_rmod_2(k1_rmod_5(A,B,k5_subset_1(u1_struct_0(B),C,D)),A,k2_rmod_3(A,B,k1_rmod_5(A,B,C),k1_rmod_5(A,B,D))) ) )) )) )) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f2,negated_conjecture,(
% 29.66/4.46 ~((! [A] :( ( ~ v3_struct_0(A)& v3_rlvect_1(A)& v4_rlvect_1(A)& v5_rlvect_1(A)& v6_rlvect_1(A)& v4_group_1(A)& v7_group_1(A)& v6_vectsp_1(A)& v7_vectsp_1(A)& v8_vectsp_1(A)& ~ v10_vectsp_1(A)& v2_vectsp_2(A)& l3_vectsp_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_rlvect_1(B)& v4_rlvect_1(B)& v5_rlvect_1(B)& v6_rlvect_1(B)& v5_vectsp_2(B,A)& l1_vectsp_2(B,A) )=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))=> m1_rmod_2(k1_rmod_5(A,B,k5_subset_1(u1_struct_0(B),C,D)),A,k2_rmod_3(A,B,k1_rmod_5(A,B,C),k1_rmod_5(A,B,D))) ) )) )) )) ))),
% 29.66/4.46 inference(negated_conjecture,[status(cth)],[f1])).
% 29.66/4.46 fof(f6,axiom,(
% 29.66/4.46 (! [A] :( l1_vectsp_1(A)=> ( ( ~ v3_struct_0(A)& v7_group_1(A)& v8_vectsp_1(A) )=> ( ~ v3_struct_0(A)& v2_group_1(A)& v6_vectsp_1(A)& v8_vectsp_1(A) ) ) ) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f7,axiom,(
% 29.66/4.46 (! [A] :( l1_vectsp_1(A)=> ( ( ~ v3_struct_0(A)& v7_group_1(A)& v6_vectsp_1(A) )=> ( ~ v3_struct_0(A)& v2_group_1(A)& v6_vectsp_1(A)& v8_vectsp_1(A) ) ) ) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f8,axiom,(
% 29.66/4.46 (! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f11,axiom,(
% 29.66/4.46 (! [A,B,C] :( ( ~ v3_struct_0(A)& v3_rlvect_1(A)& v4_rlvect_1(A)& v5_rlvect_1(A)& v6_rlvect_1(A)& v4_group_1(A)& v7_group_1(A)& v6_vectsp_1(A)& v7_vectsp_1(A)& v8_vectsp_1(A)& ~ v10_vectsp_1(A)& v2_vectsp_2(A)& l3_vectsp_1(A)& ~ v3_struct_0(B)& v3_rlvect_1(B)& v4_rlvect_1(B)& v5_rlvect_1(B)& v6_rlvect_1(B)& v5_vectsp_2(B,A)& l1_vectsp_2(B,A)& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )=> ( v3_vectsp_2(k1_rmod_5(A,B,C),A)& m1_rmod_2(k1_rmod_5(A,B,C),A,B) ) ) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f17,axiom,(
% 29.66/4.46 (! [A,B,C] :( ( m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> m1_subset_1(k5_subset_1(A,B,C),k1_zfmisc_1(A)) ) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f24,axiom,(
% 29.66/4.46 (! [A] :( l2_vectsp_1(A)=> ( l1_vectsp_1(A)& l2_struct_0(A) ) ) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f25,axiom,(
% 29.66/4.46 (! [A] :( l3_vectsp_1(A)=> ( l1_rlvect_1(A)& l2_vectsp_1(A) ) ) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f66,axiom,(
% 29.66/4.46 (! [A,B,C] :( ( m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> k5_subset_1(A,B,C) = k3_xboole_0(B,C) ) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f69,axiom,(
% 29.66/4.46 (! [A] :( ( ~ v3_struct_0(A)& v3_rlvect_1(A)& v4_rlvect_1(A)& v5_rlvect_1(A)& v6_rlvect_1(A)& v4_group_1(A)& v7_group_1(A)& v6_vectsp_1(A)& v7_vectsp_1(A)& v8_vectsp_1(A)& ~ v10_vectsp_1(A)& v2_vectsp_2(A)& l3_vectsp_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_rlvect_1(B)& v4_rlvect_1(B)& v5_rlvect_1(B)& v6_rlvect_1(B)& v5_vectsp_2(B,A)& l1_vectsp_2(B,A) )=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))=> ( r1_tarski(C,D)=> m1_rmod_2(k1_rmod_5(A,B,C),A,k1_rmod_5(A,B,D)) ) ) )) )) )) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f70,axiom,(
% 29.66/4.46 (! [A,B] : r1_tarski(k3_xboole_0(A,B),A) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f72,axiom,(
% 29.66/4.46 (! [A] :( ( ~ v3_struct_0(A)& v3_rlvect_1(A)& v4_rlvect_1(A)& v5_rlvect_1(A)& v6_rlvect_1(A)& v4_group_1(A)& v6_vectsp_1(A)& v7_vectsp_1(A)& v8_vectsp_1(A)& l3_vectsp_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_rlvect_1(B)& v4_rlvect_1(B)& v5_rlvect_1(B)& v6_rlvect_1(B)& v5_vectsp_2(B,A)& l1_vectsp_2(B,A) )=> (! [C] :( m1_rmod_2(C,A,B)=> (! [D] :( m1_rmod_2(D,A,B)=> (! [E] :( m1_rmod_2(E,A,B)=> ( ( m1_rmod_2(C,A,D)& m1_rmod_2(C,A,E) )=> m1_rmod_2(C,A,k2_rmod_3(A,B,D,E)) ) ) )) )) )) )) )),
% 29.66/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.66/4.46 fof(f81,plain,(
% 29.66/4.46 (?[A]: (((((((((((((~v3_struct_0(A)&v3_rlvect_1(A))&v4_rlvect_1(A))&v5_rlvect_1(A))&v6_rlvect_1(A))&v4_group_1(A))&v7_group_1(A))&v6_vectsp_1(A))&v7_vectsp_1(A))&v8_vectsp_1(A))&~v10_vectsp_1(A))&v2_vectsp_2(A))&l3_vectsp_1(A))&(?[B]: (((((((~v3_struct_0(B)&v3_rlvect_1(B))&v4_rlvect_1(B))&v5_rlvect_1(B))&v6_rlvect_1(B))&v5_vectsp_2(B,A))&l1_vectsp_2(B,A))&(?[C]: (m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))&(?[D]: (m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))&~m1_rmod_2(k1_rmod_5(A,B,k5_subset_1(u1_struct_0(B),C,D)),A,k2_rmod_3(A,B,k1_rmod_5(A,B,C),k1_rmod_5(A,B,D)))))))))))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 29.66/4.46 fof(f82,plain,(
% 29.66/4.46 (((((((((((((~v3_struct_0(sK0_skl)&v3_rlvect_1(sK0_skl))&v4_rlvect_1(sK0_skl))&v5_rlvect_1(sK0_skl))&v6_rlvect_1(sK0_skl))&v4_group_1(sK0_skl))&v7_group_1(sK0_skl))&v6_vectsp_1(sK0_skl))&v7_vectsp_1(sK0_skl))&v8_vectsp_1(sK0_skl))&~v10_vectsp_1(sK0_skl))&v2_vectsp_2(sK0_skl))&l3_vectsp_1(sK0_skl))&(((((((~v3_struct_0(sK1_skl)&v3_rlvect_1(sK1_skl))&v4_rlvect_1(sK1_skl))&v5_rlvect_1(sK1_skl))&v6_rlvect_1(sK1_skl))&v5_vectsp_2(sK1_skl,sK0_skl))&l1_vectsp_2(sK1_skl,sK0_skl))&(m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))&(m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))&~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k5_subset_1(u1_struct_0(sK1_skl),sK2_skl,sK3_skl)),sK0_skl,k2_rmod_3(sK0_skl,sK1_skl,k1_rmod_5(sK0_skl,sK1_skl,sK2_skl),k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)))))))),
% 29.66/4.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f81])).
% 29.66/4.46 fof(f83,plain,(
% 29.66/4.46 ~v3_struct_0(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f84,plain,(
% 29.66/4.46 v3_rlvect_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f85,plain,(
% 29.66/4.46 v4_rlvect_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f86,plain,(
% 29.66/4.46 v5_rlvect_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f87,plain,(
% 29.66/4.46 v6_rlvect_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f88,plain,(
% 29.66/4.46 v4_group_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f89,plain,(
% 29.66/4.46 v7_group_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f90,plain,(
% 29.66/4.46 v6_vectsp_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f91,plain,(
% 29.66/4.46 v7_vectsp_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f92,plain,(
% 29.66/4.46 v8_vectsp_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f93,plain,(
% 29.66/4.46 ~v10_vectsp_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f94,plain,(
% 29.66/4.46 v2_vectsp_2(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f95,plain,(
% 29.66/4.46 l3_vectsp_1(sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f96,plain,(
% 29.66/4.46 ~v3_struct_0(sK1_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f97,plain,(
% 29.66/4.46 v3_rlvect_1(sK1_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f98,plain,(
% 29.66/4.46 v4_rlvect_1(sK1_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f99,plain,(
% 29.66/4.46 v5_rlvect_1(sK1_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f100,plain,(
% 29.66/4.46 v6_rlvect_1(sK1_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f101,plain,(
% 29.66/4.46 v5_vectsp_2(sK1_skl,sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f102,plain,(
% 29.66/4.46 l1_vectsp_2(sK1_skl,sK0_skl)),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f103,plain,(
% 29.66/4.46 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f104,plain,(
% 29.66/4.46 m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f105,plain,(
% 29.66/4.46 ~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k5_subset_1(u1_struct_0(sK1_skl),sK2_skl,sK3_skl)),sK0_skl,k2_rmod_3(sK0_skl,sK1_skl,k1_rmod_5(sK0_skl,sK1_skl,sK2_skl),k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f82])).
% 29.66/4.46 fof(f113,plain,(
% 29.66/4.46 ![A]: (~l1_vectsp_1(A)|(((v3_struct_0(A)|~v7_group_1(A))|~v8_vectsp_1(A))|(((~v3_struct_0(A)&v2_group_1(A))&v6_vectsp_1(A))&v8_vectsp_1(A))))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 29.66/4.46 fof(f116,plain,(
% 29.66/4.46 ![X0]: (~l1_vectsp_1(X0)|v3_struct_0(X0)|~v7_group_1(X0)|~v8_vectsp_1(X0)|v6_vectsp_1(X0))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f113])).
% 29.66/4.46 fof(f118,plain,(
% 29.66/4.46 ![A]: (~l1_vectsp_1(A)|(((v3_struct_0(A)|~v7_group_1(A))|~v6_vectsp_1(A))|(((~v3_struct_0(A)&v2_group_1(A))&v6_vectsp_1(A))&v8_vectsp_1(A))))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 29.66/4.46 fof(f122,plain,(
% 29.66/4.46 ![X0]: (~l1_vectsp_1(X0)|v3_struct_0(X0)|~v7_group_1(X0)|~v6_vectsp_1(X0)|v8_vectsp_1(X0))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f118])).
% 29.66/4.46 fof(f123,plain,(
% 29.66/4.46 ![X0,X1]: (k3_xboole_0(X0,X1)=k3_xboole_0(X1,X0))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f8])).
% 29.66/4.46 fof(f129,plain,(
% 29.66/4.46 ![A,B,C]: (((((((((((((((((((((v3_struct_0(A)|~v3_rlvect_1(A))|~v4_rlvect_1(A))|~v5_rlvect_1(A))|~v6_rlvect_1(A))|~v4_group_1(A))|~v7_group_1(A))|~v6_vectsp_1(A))|~v7_vectsp_1(A))|~v8_vectsp_1(A))|v10_vectsp_1(A))|~v2_vectsp_2(A))|~l3_vectsp_1(A))|v3_struct_0(B))|~v3_rlvect_1(B))|~v4_rlvect_1(B))|~v5_rlvect_1(B))|~v6_rlvect_1(B))|~v5_vectsp_2(B,A))|~l1_vectsp_2(B,A))|~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))))|(v3_vectsp_2(k1_rmod_5(A,B,C),A)&m1_rmod_2(k1_rmod_5(A,B,C),A,B)))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 29.66/4.46 fof(f131,plain,(
% 29.66/4.46 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v4_group_1(X0)|~v7_group_1(X0)|~v6_vectsp_1(X0)|~v7_vectsp_1(X0)|~v8_vectsp_1(X0)|v10_vectsp_1(X0)|~v2_vectsp_2(X0)|~l3_vectsp_1(X0)|v3_struct_0(X1)|~v3_rlvect_1(X1)|~v4_rlvect_1(X1)|~v5_rlvect_1(X1)|~v6_rlvect_1(X1)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,X1))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f129])).
% 29.66/4.46 fof(f135,plain,(
% 29.66/4.46 ![A,B,C]: ((~m1_subset_1(B,k1_zfmisc_1(A))|~m1_subset_1(C,k1_zfmisc_1(A)))|m1_subset_1(k5_subset_1(A,B,C),k1_zfmisc_1(A)))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 29.66/4.46 fof(f136,plain,(
% 29.66/4.46 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(X1))|m1_subset_1(k5_subset_1(X1,X0,X2),k1_zfmisc_1(X1)))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f135])).
% 29.66/4.46 fof(f147,plain,(
% 29.66/4.46 ![A]: (~l2_vectsp_1(A)|(l1_vectsp_1(A)&l2_struct_0(A)))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 29.66/4.46 fof(f148,plain,(
% 29.66/4.46 ![X0]: (~l2_vectsp_1(X0)|l1_vectsp_1(X0))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f147])).
% 29.66/4.46 fof(f150,plain,(
% 29.66/4.46 ![A]: (~l3_vectsp_1(A)|(l1_rlvect_1(A)&l2_vectsp_1(A)))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 29.66/4.46 fof(f152,plain,(
% 29.66/4.46 ![X0]: (~l3_vectsp_1(X0)|l2_vectsp_1(X0))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f150])).
% 29.66/4.46 fof(f277,plain,(
% 29.66/4.46 ![A,B,C]: ((~m1_subset_1(B,k1_zfmisc_1(A))|~m1_subset_1(C,k1_zfmisc_1(A)))|k5_subset_1(A,B,C)=k3_xboole_0(B,C))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 29.66/4.46 fof(f278,plain,(
% 29.66/4.46 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(X1))|k5_subset_1(X1,X0,X2)=k3_xboole_0(X0,X2))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f277])).
% 29.66/4.46 fof(f285,plain,(
% 29.66/4.46 ![A]: (((((((((((((v3_struct_0(A)|~v3_rlvect_1(A))|~v4_rlvect_1(A))|~v5_rlvect_1(A))|~v6_rlvect_1(A))|~v4_group_1(A))|~v7_group_1(A))|~v6_vectsp_1(A))|~v7_vectsp_1(A))|~v8_vectsp_1(A))|v10_vectsp_1(A))|~v2_vectsp_2(A))|~l3_vectsp_1(A))|(![B]: (((((((v3_struct_0(B)|~v3_rlvect_1(B))|~v4_rlvect_1(B))|~v5_rlvect_1(B))|~v6_rlvect_1(B))|~v5_vectsp_2(B,A))|~l1_vectsp_2(B,A))|(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|(![D]: (~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))|(~r1_tarski(C,D)|m1_rmod_2(k1_rmod_5(A,B,C),A,k1_rmod_5(A,B,D))))))))))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 29.66/4.46 fof(f286,plain,(
% 29.66/4.46 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v4_group_1(X0)|~v7_group_1(X0)|~v6_vectsp_1(X0)|~v7_vectsp_1(X0)|~v8_vectsp_1(X0)|v10_vectsp_1(X0)|~v2_vectsp_2(X0)|~l3_vectsp_1(X0)|v3_struct_0(X1)|~v3_rlvect_1(X1)|~v4_rlvect_1(X1)|~v5_rlvect_1(X1)|~v6_rlvect_1(X1)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))|~r1_tarski(X2,X3)|m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,k1_rmod_5(X0,X1,X3)))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f285])).
% 29.66/4.46 fof(f287,plain,(
% 29.66/4.46 ![X0,X1]: (r1_tarski(k3_xboole_0(X0,X1),X0))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f70])).
% 29.66/4.46 fof(f290,plain,(
% 29.66/4.46 ![A]: ((((((((((v3_struct_0(A)|~v3_rlvect_1(A))|~v4_rlvect_1(A))|~v5_rlvect_1(A))|~v6_rlvect_1(A))|~v4_group_1(A))|~v6_vectsp_1(A))|~v7_vectsp_1(A))|~v8_vectsp_1(A))|~l3_vectsp_1(A))|(![B]: (((((((v3_struct_0(B)|~v3_rlvect_1(B))|~v4_rlvect_1(B))|~v5_rlvect_1(B))|~v6_rlvect_1(B))|~v5_vectsp_2(B,A))|~l1_vectsp_2(B,A))|(![C]: (~m1_rmod_2(C,A,B)|(![D]: (~m1_rmod_2(D,A,B)|(![E]: (~m1_rmod_2(E,A,B)|((~m1_rmod_2(C,A,D)|~m1_rmod_2(C,A,E))|m1_rmod_2(C,A,k2_rmod_3(A,B,D,E))))))))))))),
% 29.66/4.46 inference(pre_NNF_transformation,[status(thm)],[f72])).
% 29.66/4.46 fof(f291,plain,(
% 29.66/4.46 ![X0,X1,X2,X3,X4]: (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v4_group_1(X0)|~v6_vectsp_1(X0)|~v7_vectsp_1(X0)|~v8_vectsp_1(X0)|~l3_vectsp_1(X0)|v3_struct_0(X1)|~v3_rlvect_1(X1)|~v4_rlvect_1(X1)|~v5_rlvect_1(X1)|~v6_rlvect_1(X1)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~m1_rmod_2(X2,X0,X1)|~m1_rmod_2(X3,X0,X1)|~m1_rmod_2(X4,X0,X1)|~m1_rmod_2(X2,X0,X3)|~m1_rmod_2(X2,X0,X4)|m1_rmod_2(X2,X0,k2_rmod_3(X0,X1,X3,X4)))),
% 29.66/4.46 inference(cnf_transformation,[status(thm)],[f290])).
% 29.66/4.46 fof(f327,plain,(
% 29.66/4.46 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|k5_subset_1(u1_struct_0(sK1_skl),X0,sK3_skl)=k3_xboole_0(X0,sK3_skl))),
% 29.66/4.46 inference(resolution,[status(thm)],[f278,f104])).
% 29.66/4.46 fof(f330,plain,(
% 29.66/4.46 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|m1_subset_1(k5_subset_1(u1_struct_0(sK1_skl),X0,sK3_skl),k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 29.66/4.46 inference(resolution,[status(thm)],[f136,f104])).
% 29.66/4.46 fof(f340,plain,(
% 29.66/4.46 k5_subset_1(u1_struct_0(sK1_skl),sK2_skl,sK3_skl)=k3_xboole_0(sK2_skl,sK3_skl)),
% 29.66/4.46 inference(resolution,[status(thm)],[f327,f103])).
% 29.66/4.46 fof(f344,plain,(
% 29.66/4.46 ~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,k2_rmod_3(sK0_skl,sK1_skl,k1_rmod_5(sK0_skl,sK1_skl,sK2_skl),k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)))),
% 29.66/4.46 inference(backward_demodulation,[status(thm)],[f340,f105])).
% 29.66/4.46 fof(f445,plain,(
% 29.66/4.46 ![X0]: (l1_vectsp_1(X0)|~l3_vectsp_1(X0))),
% 29.66/4.46 inference(resolution,[status(thm)],[f148,f152])).
% 29.66/4.46 fof(f446,plain,(
% 29.66/4.46 ![X0]: (~l3_vectsp_1(X0)|v3_struct_0(X0)|~v7_group_1(X0)|~v6_vectsp_1(X0)|v8_vectsp_1(X0))),
% 29.66/4.46 inference(resolution,[status(thm)],[f445,f122])).
% 29.66/4.46 fof(f447,plain,(
% 29.66/4.46 ![X0]: (~l3_vectsp_1(X0)|v3_struct_0(X0)|~v7_group_1(X0)|~v8_vectsp_1(X0)|v6_vectsp_1(X0))),
% 29.66/4.46 inference(resolution,[status(thm)],[f445,f116])).
% 29.66/4.46 fof(f448,plain,(
% 29.66/4.46 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v4_group_1(X0)|~v7_group_1(X0)|~v6_vectsp_1(X0)|~v7_vectsp_1(X0)|v10_vectsp_1(X0)|~v2_vectsp_2(X0)|~l3_vectsp_1(X0)|v3_struct_0(X1)|~v3_rlvect_1(X1)|~v4_rlvect_1(X1)|~v5_rlvect_1(X1)|~v6_rlvect_1(X1)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,X1))),
% 29.66/4.46 inference(backward_subsumption_resolution,[status(thm)],[f131,f446])).
% 29.66/4.46 fof(f450,plain,(
% 29.66/4.46 ~l3_vectsp_1(sK0_skl)|v3_struct_0(sK0_skl)|~v7_group_1(sK0_skl)|v8_vectsp_1(sK0_skl)),
% 29.66/4.46 inference(resolution,[status(thm)],[f446,f90])).
% 29.66/4.46 fof(f451,definition,(
% 29.66/4.46 sQ4_spl <=> (l3_vectsp_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f453,plain,(
% 29.66/4.46 ~l3_vectsp_1(sK0_skl)|sQ4_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f451])).
% 29.66/4.46 fof(f454,definition,(
% 29.66/4.46 sQ5_spl <=> (v3_struct_0(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f455,plain,(
% 29.66/4.46 v3_struct_0(sK0_skl)|~sQ5_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f454])).
% 29.66/4.46 fof(f457,definition,(
% 29.66/4.46 sQ6_spl <=> (v7_group_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f459,plain,(
% 29.66/4.46 ~v7_group_1(sK0_skl)|sQ6_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f457])).
% 29.66/4.46 fof(f460,definition,(
% 29.66/4.46 sQ7_spl <=> (v8_vectsp_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f463,plain,(
% 29.66/4.46 ~sQ4_spl|sQ5_spl|~sQ6_spl|sQ7_spl),
% 29.66/4.46 inference(split_clause,[status(thm)],[f450,f451,f454,f457,f460])).
% 29.66/4.46 fof(f464,plain,(
% 29.66/4.46 ~l3_vectsp_1(sK0_skl)|v3_struct_0(sK0_skl)|~v7_group_1(sK0_skl)|v6_vectsp_1(sK0_skl)),
% 29.66/4.46 inference(resolution,[status(thm)],[f447,f92])).
% 29.66/4.46 fof(f465,definition,(
% 29.66/4.46 sQ8_spl <=> (v6_vectsp_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f468,plain,(
% 29.66/4.46 ~sQ4_spl|sQ5_spl|~sQ6_spl|sQ8_spl),
% 29.66/4.46 inference(split_clause,[status(thm)],[f464,f451,f454,f457,f465])).
% 29.66/4.46 fof(f469,plain,(
% 29.66/4.46 $false|sQ6_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f459,f89])).
% 29.66/4.46 fof(f470,plain,(
% 29.66/4.46 sQ6_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f469])).
% 29.66/4.46 fof(f471,plain,(
% 29.66/4.46 $false|~sQ5_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f455,f83])).
% 29.66/4.46 fof(f472,plain,(
% 29.66/4.46 ~sQ5_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f471])).
% 29.66/4.46 fof(f473,plain,(
% 29.66/4.46 $false|sQ4_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f453,f95])).
% 29.66/4.46 fof(f474,plain,(
% 29.66/4.46 sQ4_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f473])).
% 29.66/4.46 fof(f505,plain,(
% 29.66/4.46 m1_subset_1(k5_subset_1(u1_struct_0(sK1_skl),sK2_skl,sK3_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 29.66/4.46 inference(resolution,[status(thm)],[f330,f103])).
% 29.66/4.46 fof(f510,plain,(
% 29.66/4.46 m1_subset_1(k3_xboole_0(sK2_skl,sK3_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 29.66/4.46 inference(forward_demodulation,[status(thm)],[f340,f505])).
% 29.66/4.46 fof(f570,definition,(
% 29.66/4.46 sQ15_spl <=> (v3_rlvect_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f572,plain,(
% 29.66/4.46 ~v3_rlvect_1(sK0_skl)|sQ15_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f570])).
% 29.66/4.46 fof(f573,definition,(
% 29.66/4.46 sQ16_spl <=> (v4_rlvect_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f575,plain,(
% 29.66/4.46 ~v4_rlvect_1(sK0_skl)|sQ16_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f573])).
% 29.66/4.46 fof(f576,definition,(
% 29.66/4.46 sQ17_spl <=> (v5_rlvect_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f578,plain,(
% 29.66/4.46 ~v5_rlvect_1(sK0_skl)|sQ17_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f576])).
% 29.66/4.46 fof(f579,definition,(
% 29.66/4.46 sQ18_spl <=> (v6_rlvect_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f581,plain,(
% 29.66/4.46 ~v6_rlvect_1(sK0_skl)|sQ18_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f579])).
% 29.66/4.46 fof(f582,definition,(
% 29.66/4.46 sQ19_spl <=> (v4_group_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f584,plain,(
% 29.66/4.46 ~v4_group_1(sK0_skl)|sQ19_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f582])).
% 29.66/4.46 fof(f585,definition,(
% 29.66/4.46 sQ20_spl <=> (v7_vectsp_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f587,plain,(
% 29.66/4.46 ~v7_vectsp_1(sK0_skl)|sQ20_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f585])).
% 29.66/4.46 fof(f594,plain,(
% 29.66/4.46 $false|sQ19_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f584,f88])).
% 29.66/4.46 fof(f595,plain,(
% 29.66/4.46 sQ19_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f594])).
% 29.66/4.46 fof(f596,plain,(
% 29.66/4.46 $false|sQ18_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f581,f87])).
% 29.66/4.46 fof(f597,plain,(
% 29.66/4.46 sQ18_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f596])).
% 29.66/4.46 fof(f598,plain,(
% 29.66/4.46 $false|sQ17_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f578,f86])).
% 29.66/4.46 fof(f599,plain,(
% 29.66/4.46 sQ17_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f598])).
% 29.66/4.46 fof(f600,plain,(
% 29.66/4.46 $false|sQ16_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f575,f85])).
% 29.66/4.46 fof(f601,plain,(
% 29.66/4.46 sQ16_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f600])).
% 29.66/4.46 fof(f602,plain,(
% 29.66/4.46 $false|sQ15_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f572,f84])).
% 29.66/4.46 fof(f603,plain,(
% 29.66/4.46 sQ15_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f602])).
% 29.66/4.46 fof(f604,plain,(
% 29.66/4.46 $false|sQ20_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f587,f91])).
% 29.66/4.46 fof(f605,plain,(
% 29.66/4.46 sQ20_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f604])).
% 29.66/4.46 fof(f797,plain,(
% 29.66/4.46 ![X0,X1]: (r1_tarski(k3_xboole_0(X0,X1),X1))),
% 29.66/4.46 inference(paramodulation,[status(thm)],[f123,f287])).
% 29.66/4.46 fof(f969,definition,(
% 29.66/4.46 sQ27_spl <=> (v3_struct_0(sK1_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f970,plain,(
% 29.66/4.46 v3_struct_0(sK1_skl)|~sQ27_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f969])).
% 29.66/4.46 fof(f972,definition,(
% 29.66/4.46 sQ28_spl <=> (v3_rlvect_1(sK1_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f974,plain,(
% 29.66/4.46 ~v3_rlvect_1(sK1_skl)|sQ28_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f972])).
% 29.66/4.46 fof(f975,definition,(
% 29.66/4.46 sQ29_spl <=> (v4_rlvect_1(sK1_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f977,plain,(
% 29.66/4.46 ~v4_rlvect_1(sK1_skl)|sQ29_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f975])).
% 29.66/4.46 fof(f978,definition,(
% 29.66/4.46 sQ30_spl <=> (v5_rlvect_1(sK1_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f980,plain,(
% 29.66/4.46 ~v5_rlvect_1(sK1_skl)|sQ30_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f978])).
% 29.66/4.46 fof(f981,definition,(
% 29.66/4.46 sQ31_spl <=> (v6_rlvect_1(sK1_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f983,plain,(
% 29.66/4.46 ~v6_rlvect_1(sK1_skl)|sQ31_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f981])).
% 29.66/4.46 fof(f984,definition,(
% 29.66/4.46 sQ32_spl <=> (v5_vectsp_2(sK1_skl,sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f986,plain,(
% 29.66/4.46 ~v5_vectsp_2(sK1_skl,sK0_skl)|sQ32_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f984])).
% 29.66/4.46 fof(f995,definition,(
% 29.66/4.46 sQ35_spl <=> (l1_vectsp_2(sK1_skl,sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f997,plain,(
% 29.66/4.46 ~l1_vectsp_2(sK1_skl,sK0_skl)|sQ35_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f995])).
% 29.66/4.46 fof(f999,plain,(
% 29.66/4.46 $false|sQ32_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f986,f101])).
% 29.66/4.46 fof(f1000,plain,(
% 29.66/4.46 sQ32_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f999])).
% 29.66/4.46 fof(f1001,plain,(
% 29.66/4.46 $false|sQ31_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f983,f100])).
% 29.66/4.46 fof(f1002,plain,(
% 29.66/4.46 sQ31_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f1001])).
% 29.66/4.46 fof(f1003,plain,(
% 29.66/4.46 $false|sQ30_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f980,f99])).
% 29.66/4.46 fof(f1004,plain,(
% 29.66/4.46 sQ30_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f1003])).
% 29.66/4.46 fof(f1005,plain,(
% 29.66/4.46 $false|sQ29_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f977,f98])).
% 29.66/4.46 fof(f1006,plain,(
% 29.66/4.46 sQ29_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f1005])).
% 29.66/4.46 fof(f1007,plain,(
% 29.66/4.46 $false|sQ28_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f974,f97])).
% 29.66/4.46 fof(f1008,plain,(
% 29.66/4.46 sQ28_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f1007])).
% 29.66/4.46 fof(f1009,plain,(
% 29.66/4.46 $false|~sQ27_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f970,f96])).
% 29.66/4.46 fof(f1010,plain,(
% 29.66/4.46 ~sQ27_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f1009])).
% 29.66/4.46 fof(f1127,plain,(
% 29.66/4.46 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v4_group_1(X0)|~v7_group_1(X0)|~v7_vectsp_1(X0)|~v8_vectsp_1(X0)|v10_vectsp_1(X0)|~v2_vectsp_2(X0)|~l3_vectsp_1(X0)|v3_struct_0(X1)|~v3_rlvect_1(X1)|~v4_rlvect_1(X1)|~v5_rlvect_1(X1)|~v6_rlvect_1(X1)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))|~r1_tarski(X2,X3)|m1_rmod_2(k1_rmod_5(X0,X1,X2),X0,k1_rmod_5(X0,X1,X3)))),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f286,f447])).
% 29.66/4.46 fof(f1128,plain,(
% 29.66/4.46 ![X0,X1,X2,X3]: (v3_struct_0(sK0_skl)|~v3_rlvect_1(sK0_skl)|~v4_rlvect_1(sK0_skl)|~v5_rlvect_1(sK0_skl)|~v6_rlvect_1(sK0_skl)|~v4_group_1(sK0_skl)|~v7_vectsp_1(sK0_skl)|~v8_vectsp_1(sK0_skl)|~l3_vectsp_1(sK0_skl)|v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v5_vectsp_2(X0,sK0_skl)|~l1_vectsp_2(X0,sK0_skl)|~m1_rmod_2(X1,sK0_skl,X0)|~m1_rmod_2(X2,sK0_skl,X0)|~m1_rmod_2(X3,sK0_skl,X0)|~m1_rmod_2(X1,sK0_skl,X2)|~m1_rmod_2(X1,sK0_skl,X3)|m1_rmod_2(X1,sK0_skl,k2_rmod_3(sK0_skl,X0,X2,X3)))),
% 29.66/4.46 inference(resolution,[status(thm)],[f291,f90])).
% 29.66/4.46 fof(f1131,definition,(
% 29.66/4.46 ![X0,X1,X2,X3]: (sQ36_spl <=> (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v5_vectsp_2(X0,sK0_skl)|~l1_vectsp_2(X0,sK0_skl)|~m1_rmod_2(X1,sK0_skl,X0)|~m1_rmod_2(X2,sK0_skl,X0)|~m1_rmod_2(X3,sK0_skl,X0)|~m1_rmod_2(X1,sK0_skl,X2)|~m1_rmod_2(X1,sK0_skl,X3)|m1_rmod_2(X1,sK0_skl,k2_rmod_3(sK0_skl,X0,X2,X3))))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f1132,plain,(
% 29.66/4.46 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v5_vectsp_2(X0,sK0_skl)|~l1_vectsp_2(X0,sK0_skl)|~m1_rmod_2(X1,sK0_skl,X0)|~m1_rmod_2(X2,sK0_skl,X0)|~m1_rmod_2(X3,sK0_skl,X0)|~m1_rmod_2(X1,sK0_skl,X2)|~m1_rmod_2(X1,sK0_skl,X3)|m1_rmod_2(X1,sK0_skl,k2_rmod_3(sK0_skl,X0,X2,X3))|~sQ36_spl)),
% 29.66/4.46 inference(component_clause,[status(thm)],[f1131])).
% 29.66/4.46 fof(f1134,plain,(
% 29.66/4.46 sQ5_spl|~sQ15_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ7_spl|~sQ4_spl|sQ36_spl),
% 29.66/4.46 inference(split_clause,[status(thm)],[f1128,f454,f570,f573,f576,f579,f582,f585,f460,f451,f1131])).
% 29.66/4.46 fof(f1604,plain,(
% 29.66/4.46 $false|sQ35_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f997,f102])).
% 29.66/4.46 fof(f1605,plain,(
% 29.66/4.46 sQ35_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f1604])).
% 29.66/4.46 fof(f1717,plain,(
% 29.66/4.46 ![X0,X1]: (v3_struct_0(sK0_skl)|~v3_rlvect_1(sK0_skl)|~v4_rlvect_1(sK0_skl)|~v5_rlvect_1(sK0_skl)|~v6_rlvect_1(sK0_skl)|~v4_group_1(sK0_skl)|~v6_vectsp_1(sK0_skl)|~v7_vectsp_1(sK0_skl)|v10_vectsp_1(sK0_skl)|~v2_vectsp_2(sK0_skl)|~l3_vectsp_1(sK0_skl)|v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v5_vectsp_2(X0,sK0_skl)|~l1_vectsp_2(X0,sK0_skl)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m1_rmod_2(k1_rmod_5(sK0_skl,X0,X1),sK0_skl,X0))),
% 29.66/4.46 inference(resolution,[status(thm)],[f448,f89])).
% 29.66/4.46 fof(f1721,definition,(
% 29.66/4.46 sQ40_spl <=> (v10_vectsp_1(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f1722,plain,(
% 29.66/4.46 v10_vectsp_1(sK0_skl)|~sQ40_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f1721])).
% 29.66/4.46 fof(f1724,definition,(
% 29.66/4.46 sQ41_spl <=> (v2_vectsp_2(sK0_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f1726,plain,(
% 29.66/4.46 ~v2_vectsp_2(sK0_skl)|sQ41_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f1724])).
% 29.66/4.46 fof(f1727,definition,(
% 29.66/4.46 ![X0,X1]: (sQ42_spl <=> (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v5_vectsp_2(X0,sK0_skl)|~l1_vectsp_2(X0,sK0_skl)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m1_rmod_2(k1_rmod_5(sK0_skl,X0,X1),sK0_skl,X0)))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f1728,plain,(
% 29.66/4.46 ![X0,X1]: (v3_struct_0(X0)|~v3_rlvect_1(X0)|~v4_rlvect_1(X0)|~v5_rlvect_1(X0)|~v6_rlvect_1(X0)|~v5_vectsp_2(X0,sK0_skl)|~l1_vectsp_2(X0,sK0_skl)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m1_rmod_2(k1_rmod_5(sK0_skl,X0,X1),sK0_skl,X0)|~sQ42_spl)),
% 29.66/4.46 inference(component_clause,[status(thm)],[f1727])).
% 29.66/4.46 fof(f1730,plain,(
% 29.66/4.46 sQ5_spl|~sQ15_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ8_spl|~sQ20_spl|sQ40_spl|~sQ41_spl|~sQ4_spl|sQ42_spl),
% 29.66/4.46 inference(split_clause,[status(thm)],[f1717,f454,f570,f573,f576,f579,f582,f465,f585,f1721,f1724,f451,f1727])).
% 29.66/4.46 fof(f1734,plain,(
% 29.66/4.46 $false|~sQ40_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f1722,f93])).
% 29.66/4.46 fof(f1735,plain,(
% 29.66/4.46 ~sQ40_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f1734])).
% 29.66/4.46 fof(f1736,plain,(
% 29.66/4.46 $false|sQ41_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f1726,f94])).
% 29.66/4.46 fof(f1737,plain,(
% 29.66/4.46 sQ41_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f1736])).
% 29.66/4.46 fof(f3178,plain,(
% 29.66/4.46 ![X0,X1,X2]: (v3_struct_0(sK1_skl)|~v3_rlvect_1(sK1_skl)|~v4_rlvect_1(sK1_skl)|~v5_rlvect_1(sK1_skl)|~v6_rlvect_1(sK1_skl)|~l1_vectsp_2(sK1_skl,sK0_skl)|~m1_rmod_2(X0,sK0_skl,sK1_skl)|~m1_rmod_2(X1,sK0_skl,sK1_skl)|~m1_rmod_2(X2,sK0_skl,sK1_skl)|~m1_rmod_2(X0,sK0_skl,X1)|~m1_rmod_2(X0,sK0_skl,X2)|m1_rmod_2(X0,sK0_skl,k2_rmod_3(sK0_skl,sK1_skl,X1,X2))|~sQ36_spl)),
% 29.66/4.46 inference(resolution,[status(thm)],[f1132,f101])).
% 29.66/4.46 fof(f3179,definition,(
% 29.66/4.46 ![X0,X1,X2]: (sQ62_spl <=> (~m1_rmod_2(X0,sK0_skl,sK1_skl)|~m1_rmod_2(X1,sK0_skl,sK1_skl)|~m1_rmod_2(X2,sK0_skl,sK1_skl)|~m1_rmod_2(X0,sK0_skl,X1)|~m1_rmod_2(X0,sK0_skl,X2)|m1_rmod_2(X0,sK0_skl,k2_rmod_3(sK0_skl,sK1_skl,X1,X2))))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f3180,plain,(
% 29.66/4.46 ![X0,X1,X2]: (~m1_rmod_2(X0,sK0_skl,sK1_skl)|~m1_rmod_2(X1,sK0_skl,sK1_skl)|~m1_rmod_2(X2,sK0_skl,sK1_skl)|~m1_rmod_2(X0,sK0_skl,X1)|~m1_rmod_2(X0,sK0_skl,X2)|m1_rmod_2(X0,sK0_skl,k2_rmod_3(sK0_skl,sK1_skl,X1,X2))|~sQ62_spl)),
% 29.66/4.46 inference(component_clause,[status(thm)],[f3179])).
% 29.66/4.46 fof(f3182,plain,(
% 29.66/4.46 sQ27_spl|~sQ28_spl|~sQ29_spl|~sQ30_spl|~sQ31_spl|~sQ35_spl|sQ62_spl|~sQ36_spl),
% 29.66/4.46 inference(split_clause,[status(thm)],[f3178,f969,f972,f975,f978,f981,f995,f3179,f1131])).
% 29.66/4.46 fof(f3672,plain,(
% 29.66/4.46 ![X0]: (v3_struct_0(sK1_skl)|~v3_rlvect_1(sK1_skl)|~v4_rlvect_1(sK1_skl)|~v5_rlvect_1(sK1_skl)|~v6_rlvect_1(sK1_skl)|~l1_vectsp_2(sK1_skl,sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl,sK1_skl)|~sQ42_spl)),
% 29.66/4.46 inference(resolution,[status(thm)],[f1728,f101])).
% 29.66/4.46 fof(f3673,definition,(
% 29.66/4.46 ![X0]: (sQ63_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl,sK1_skl)))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f3674,plain,(
% 29.66/4.46 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl,sK1_skl)|~sQ63_spl)),
% 29.66/4.46 inference(component_clause,[status(thm)],[f3673])).
% 29.66/4.46 fof(f3676,plain,(
% 29.66/4.46 sQ27_spl|~sQ28_spl|~sQ29_spl|~sQ30_spl|~sQ31_spl|~sQ35_spl|sQ63_spl|~sQ42_spl),
% 29.66/4.46 inference(split_clause,[status(thm)],[f3672,f969,f972,f975,f978,f981,f995,f3673,f1727])).
% 29.66/4.46 fof(f9868,plain,(
% 29.66/4.46 ~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,sK1_skl)|~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,sK2_skl),sK0_skl,sK1_skl)|~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl,sK1_skl)|~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK2_skl))|~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK3_skl))|~sQ62_spl),
% 29.66/4.46 inference(resolution,[status(thm)],[f3180,f344])).
% 29.66/4.46 fof(f9869,definition,(
% 29.66/4.46 sQ101_spl <=> (m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,sK1_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f9871,plain,(
% 29.66/4.46 ~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,sK1_skl)|sQ101_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f9869])).
% 29.66/4.46 fof(f9872,definition,(
% 29.66/4.46 sQ102_spl <=> (m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,sK2_skl),sK0_skl,sK1_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f9874,plain,(
% 29.66/4.46 ~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,sK2_skl),sK0_skl,sK1_skl)|sQ102_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f9872])).
% 29.66/4.46 fof(f9875,definition,(
% 29.66/4.46 sQ103_spl <=> (m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl,sK1_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f9877,plain,(
% 29.66/4.46 ~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl,sK1_skl)|sQ103_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f9875])).
% 29.66/4.46 fof(f9878,definition,(
% 29.66/4.46 sQ104_spl <=> (m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK2_skl)))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f9880,plain,(
% 29.66/4.46 ~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK2_skl))|sQ104_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f9878])).
% 29.66/4.46 fof(f9881,definition,(
% 29.66/4.46 sQ105_spl <=> (m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f9883,plain,(
% 29.66/4.46 ~m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,k3_xboole_0(sK2_skl,sK3_skl)),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK3_skl))|sQ105_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f9881])).
% 29.66/4.46 fof(f9884,plain,(
% 29.66/4.46 ~sQ101_spl|~sQ102_spl|~sQ103_spl|~sQ104_spl|~sQ105_spl|~sQ62_spl),
% 29.66/4.46 inference(split_clause,[status(thm)],[f9868,f9869,f9872,f9875,f9878,f9881,f3179])).
% 29.66/4.46 fof(f13956,plain,(
% 29.66/4.46 v3_struct_0(sK0_skl)|~v3_rlvect_1(sK0_skl)|~v4_rlvect_1(sK0_skl)|~v5_rlvect_1(sK0_skl)|~v6_rlvect_1(sK0_skl)|~v4_group_1(sK0_skl)|~v7_group_1(sK0_skl)|~v7_vectsp_1(sK0_skl)|~v8_vectsp_1(sK0_skl)|v10_vectsp_1(sK0_skl)|~v2_vectsp_2(sK0_skl)|~l3_vectsp_1(sK0_skl)|v3_struct_0(sK1_skl)|~v3_rlvect_1(sK1_skl)|~v4_rlvect_1(sK1_skl)|~v5_rlvect_1(sK1_skl)|~v6_rlvect_1(sK1_skl)|~v5_vectsp_2(sK1_skl,sK0_skl)|~l1_vectsp_2(sK1_skl,sK0_skl)|~m1_subset_1(k3_xboole_0(sK2_skl,sK3_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(k3_xboole_0(sK2_skl,sK3_skl),sK3_skl)|sQ105_spl),
% 29.66/4.46 inference(resolution,[status(thm)],[f9883,f1127])).
% 29.66/4.46 fof(f13957,definition,(
% 29.66/4.46 sQ109_spl <=> (m1_subset_1(k3_xboole_0(sK2_skl,sK3_skl),k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f13959,plain,(
% 29.66/4.46 ~m1_subset_1(k3_xboole_0(sK2_skl,sK3_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ109_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f13957])).
% 29.66/4.46 fof(f13960,definition,(
% 29.66/4.46 sQ110_spl <=> (m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f13962,plain,(
% 29.66/4.46 ~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ110_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f13960])).
% 29.66/4.46 fof(f13963,definition,(
% 29.66/4.46 sQ111_spl <=> (r1_tarski(k3_xboole_0(sK2_skl,sK3_skl),sK3_skl))),
% 29.66/4.46 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 29.66/4.46 fof(f13965,plain,(
% 29.66/4.46 ~r1_tarski(k3_xboole_0(sK2_skl,sK3_skl),sK3_skl)|sQ111_spl),
% 29.66/4.46 inference(component_clause,[status(thm)],[f13963])).
% 29.66/4.46 fof(f13966,plain,(
% 29.66/4.46 sQ5_spl|~sQ15_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ6_spl|~sQ20_spl|~sQ7_spl|sQ40_spl|~sQ41_spl|~sQ4_spl|sQ27_spl|~sQ28_spl|~sQ29_spl|~sQ30_spl|~sQ31_spl|~sQ32_spl|~sQ35_spl|~sQ109_spl|~sQ110_spl|~sQ111_spl|sQ105_spl),
% 29.66/4.46 inference(split_clause,[status(thm)],[f13956,f454,f570,f573,f576,f579,f582,f457,f585,f460,f1721,f1724,f451,f969,f972,f975,f978,f981,f984,f995,f13957,f13960,f13963,f9881])).
% 29.66/4.46 fof(f13967,plain,(
% 29.66/4.46 $false|sQ111_spl),
% 29.66/4.46 inference(forward_subsumption_resolution,[status(thm)],[f13965,f797])).
% 29.66/4.46 fof(f13968,plain,(
% 29.66/4.46 sQ111_spl),
% 29.66/4.46 inference(contradiction_clause,[status(thm)],[f13967])).
% 29.66/4.48 fof(f13969,plain,(
% 29.66/4.48 $false|sQ110_spl),
% 29.66/4.48 inference(forward_subsumption_resolution,[status(thm)],[f13962,f104])).
% 29.66/4.48 fof(f13970,plain,(
% 29.66/4.48 sQ110_spl),
% 29.66/4.48 inference(contradiction_clause,[status(thm)],[f13969])).
% 29.66/4.48 fof(f13971,plain,(
% 29.66/4.48 $false|sQ109_spl),
% 29.66/4.48 inference(forward_subsumption_resolution,[status(thm)],[f13959,f510])).
% 29.66/4.48 fof(f13972,plain,(
% 29.66/4.48 sQ109_spl),
% 29.66/4.48 inference(contradiction_clause,[status(thm)],[f13971])).
% 29.66/4.48 fof(f13973,plain,(
% 29.66/4.48 v3_struct_0(sK0_skl)|~v3_rlvect_1(sK0_skl)|~v4_rlvect_1(sK0_skl)|~v5_rlvect_1(sK0_skl)|~v6_rlvect_1(sK0_skl)|~v4_group_1(sK0_skl)|~v7_group_1(sK0_skl)|~v7_vectsp_1(sK0_skl)|~v8_vectsp_1(sK0_skl)|v10_vectsp_1(sK0_skl)|~v2_vectsp_2(sK0_skl)|~l3_vectsp_1(sK0_skl)|v3_struct_0(sK1_skl)|~v3_rlvect_1(sK1_skl)|~v4_rlvect_1(sK1_skl)|~v5_rlvect_1(sK1_skl)|~v6_rlvect_1(sK1_skl)|~v5_vectsp_2(sK1_skl,sK0_skl)|~l1_vectsp_2(sK1_skl,sK0_skl)|~m1_subset_1(k3_xboole_0(sK2_skl,sK3_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(k3_xboole_0(sK2_skl,sK3_skl),sK2_skl)|sQ104_spl),
% 29.66/4.48 inference(resolution,[status(thm)],[f9880,f1127])).
% 29.66/4.48 fof(f13974,definition,(
% 29.66/4.48 sQ112_spl <=> (m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 29.66/4.48 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 29.66/4.48 fof(f13976,plain,(
% 29.66/4.48 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ112_spl),
% 29.66/4.48 inference(component_clause,[status(thm)],[f13974])).
% 29.66/4.48 fof(f13977,definition,(
% 29.66/4.48 sQ113_spl <=> (r1_tarski(k3_xboole_0(sK2_skl,sK3_skl),sK2_skl))),
% 29.66/4.48 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 29.66/4.48 fof(f13979,plain,(
% 29.66/4.48 ~r1_tarski(k3_xboole_0(sK2_skl,sK3_skl),sK2_skl)|sQ113_spl),
% 29.66/4.48 inference(component_clause,[status(thm)],[f13977])).
% 29.66/4.48 fof(f13980,plain,(
% 29.66/4.48 sQ5_spl|~sQ15_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ6_spl|~sQ20_spl|~sQ7_spl|sQ40_spl|~sQ41_spl|~sQ4_spl|sQ27_spl|~sQ28_spl|~sQ29_spl|~sQ30_spl|~sQ31_spl|~sQ32_spl|~sQ35_spl|~sQ109_spl|~sQ112_spl|~sQ113_spl|sQ104_spl),
% 29.66/4.48 inference(split_clause,[status(thm)],[f13973,f454,f570,f573,f576,f579,f582,f457,f585,f460,f1721,f1724,f451,f969,f972,f975,f978,f981,f984,f995,f13957,f13974,f13977,f9878])).
% 29.66/4.48 fof(f13981,plain,(
% 29.66/4.48 $false|sQ113_spl),
% 29.66/4.48 inference(forward_subsumption_resolution,[status(thm)],[f13979,f287])).
% 29.66/4.48 fof(f13982,plain,(
% 29.66/4.48 sQ113_spl),
% 29.66/4.48 inference(contradiction_clause,[status(thm)],[f13981])).
% 29.66/4.48 fof(f13983,plain,(
% 29.66/4.48 $false|sQ112_spl),
% 29.66/4.48 inference(forward_subsumption_resolution,[status(thm)],[f13976,f103])).
% 29.66/4.48 fof(f13984,plain,(
% 29.66/4.48 sQ112_spl),
% 29.66/4.48 inference(contradiction_clause,[status(thm)],[f13983])).
% 29.66/4.48 fof(f13985,plain,(
% 29.66/4.48 ~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ103_spl|~sQ63_spl),
% 29.66/4.48 inference(resolution,[status(thm)],[f9877,f3674])).
% 29.66/4.48 fof(f13986,plain,(
% 29.66/4.48 ~sQ110_spl|sQ103_spl|~sQ63_spl),
% 29.66/4.48 inference(split_clause,[status(thm)],[f13985,f13960,f9875,f3673])).
% 29.66/4.48 fof(f14094,plain,(
% 29.66/4.48 ~m1_subset_1(k3_xboole_0(sK2_skl,sK3_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ101_spl|~sQ63_spl),
% 29.66/4.48 inference(resolution,[status(thm)],[f9871,f3674])).
% 29.66/4.48 fof(f14095,plain,(
% 29.66/4.48 ~sQ109_spl|sQ101_spl|~sQ63_spl),
% 29.66/4.48 inference(split_clause,[status(thm)],[f14094,f13957,f9869,f3673])).
% 29.66/4.48 fof(f14096,plain,(
% 29.66/4.48 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ102_spl|~sQ63_spl),
% 29.66/4.48 inference(resolution,[status(thm)],[f9874,f3674])).
% 29.66/4.48 fof(f14097,plain,(
% 29.66/4.48 ~sQ112_spl|sQ102_spl|~sQ63_spl),
% 29.66/4.48 inference(split_clause,[status(thm)],[f14096,f13974,f9872,f3673])).
% 29.66/4.48 fof(f14098,plain,(
% 29.66/4.48 $false),
% 29.66/4.48 inference(sat_refutation,[status(thm)],[f463,f468,f470,f472,f474,f595,f597,f599,f601,f603,f605,f1000,f1002,f1004,f1006,f1008,f1010,f1134,f1605,f1730,f1735,f1737,f3182,f3676,f9884,f13966,f13968,f13970,f13972,f13980,f13982,f13984,f13986,f14095,f14097])).
% 29.66/4.48 % SZS output end CNFRefutation for theBenchmark.p
% 4.29/4.52 % Elapsed time: 3.870668 seconds
% 4.29/4.52 % CPU time: 30.432500 seconds
% 4.29/4.52 % Total memory used: 355.687 MB
% 4.29/4.52 % Net memory used: 347.651 MB
%------------------------------------------------------------------------------