%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG220+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 : n018.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 0.14s 5.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG220+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n018.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 13:06:50 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 0.14/5.45 % Refutation found
% 0.14/5.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.45 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.45 fof(f1,conjecture,(
% 0.14/5.45 (! [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)& v3_vectsp_2(B,A)& 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)))=> ( ( k1_rmod_5(A,B,C) = B& r1_tarski(C,D) )=> k1_rmod_5(A,B,D) = B ) ) )) )) )) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f2,negated_conjecture,(
% 0.14/5.45 ~((! [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)& v3_vectsp_2(B,A)& 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)))=> ( ( k1_rmod_5(A,B,C) = B& r1_tarski(C,D) )=> k1_rmod_5(A,B,D) = B ) ) )) )) )) ))),
% 0.14/5.45 inference(negated_conjecture,[status(cth)],[f1])).
% 0.14/5.45 fof(f9,axiom,(
% 0.14/5.45 (! [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) ) ) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f14,axiom,(
% 0.14/5.45 (! [A] :( l1_rlvect_1(A)=> l2_struct_0(A) ) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f18,axiom,(
% 0.14/5.45 (! [A] :( l2_struct_0(A)=> l1_struct_0(A) ) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f20,axiom,(
% 0.14/5.45 (! [A] :( l3_vectsp_1(A)=> ( l1_rlvect_1(A)& l2_vectsp_1(A) ) ) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f22,axiom,(
% 0.14/5.45 (! [A,B] :( ( ~ 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)& ~ 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)=> ( ~ v3_struct_0(C)& v3_rlvect_1(C)& v4_rlvect_1(C)& v5_rlvect_1(C)& v6_rlvect_1(C)& v5_vectsp_2(C,A)& l1_vectsp_2(C,A) ) ) )) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f60,axiom,(
% 0.14/5.45 (! [A,B] : r1_tarski(A,A) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f61,axiom,(
% 0.14/5.45 (! [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)) ) ) )) )) )) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f64,axiom,(
% 0.14/5.45 (! [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)& v3_vectsp_2(B,A)& v5_vectsp_2(B,A)& l1_vectsp_2(B,A) )=> (! [C] :( ( ~ v3_struct_0(C)& v3_rlvect_1(C)& v4_rlvect_1(C)& v5_rlvect_1(C)& v6_rlvect_1(C)& v3_vectsp_2(C,A)& v5_vectsp_2(C,A)& l1_vectsp_2(C,A) )=> ( ( m1_rmod_2(C,A,B)& m1_rmod_2(B,A,C) )=> C = B ) ) )) )) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f65,axiom,(
% 0.14/5.45 (! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) )),
% 0.14/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.45 fof(f71,plain,(
% 0.14/5.45 (?[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))&v3_vectsp_2(B,A))&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)))&((k1_rmod_5(A,B,C)=B&r1_tarski(C,D))&~k1_rmod_5(A,B,D)=B)))))))))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/5.45 fof(f72,plain,(
% 0.14/5.45 (((((((((((((~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))&v3_vectsp_2(sK1_skl,sK0_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)))&((k1_rmod_5(sK0_skl,sK1_skl,sK2_skl)=sK1_skl&r1_tarski(sK2_skl,sK3_skl))&~k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)=sK1_skl)))))),
% 0.14/5.45 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)],[f71])).
% 0.14/5.45 fof(f73,plain,(
% 0.14/5.45 ~v3_struct_0(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f74,plain,(
% 0.14/5.45 v3_rlvect_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f75,plain,(
% 0.14/5.45 v4_rlvect_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f76,plain,(
% 0.14/5.45 v5_rlvect_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f77,plain,(
% 0.14/5.45 v6_rlvect_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f78,plain,(
% 0.14/5.45 v4_group_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f79,plain,(
% 0.14/5.45 v7_group_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f80,plain,(
% 0.14/5.45 v6_vectsp_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f81,plain,(
% 0.14/5.45 v7_vectsp_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f82,plain,(
% 0.14/5.45 v8_vectsp_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f83,plain,(
% 0.14/5.45 ~v10_vectsp_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f84,plain,(
% 0.14/5.45 v2_vectsp_2(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f85,plain,(
% 0.14/5.45 l3_vectsp_1(sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f86,plain,(
% 0.14/5.45 ~v3_struct_0(sK1_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f87,plain,(
% 0.14/5.45 v3_rlvect_1(sK1_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f88,plain,(
% 0.14/5.45 v4_rlvect_1(sK1_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f89,plain,(
% 0.14/5.45 v5_rlvect_1(sK1_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f90,plain,(
% 0.14/5.45 v6_rlvect_1(sK1_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f91,plain,(
% 0.14/5.45 v3_vectsp_2(sK1_skl,sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f92,plain,(
% 0.14/5.45 v5_vectsp_2(sK1_skl,sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f93,plain,(
% 0.14/5.45 l1_vectsp_2(sK1_skl,sK0_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f94,plain,(
% 0.14/5.45 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f95,plain,(
% 0.14/5.45 m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f96,plain,(
% 0.14/5.45 k1_rmod_5(sK0_skl,sK1_skl,sK2_skl)=sK1_skl),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f97,plain,(
% 0.14/5.45 r1_tarski(sK2_skl,sK3_skl)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f98,plain,(
% 0.14/5.45 ~k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)=sK1_skl),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.45 fof(f119,plain,(
% 0.14/5.45 ![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)))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/5.45 fof(f120,plain,(
% 0.14/5.45 ![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)))|v3_vectsp_2(k1_rmod_5(X0,X1,X2),X0))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f119])).
% 0.14/5.45 fof(f121,plain,(
% 0.14/5.45 ![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))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f119])).
% 0.14/5.45 fof(f124,plain,(
% 0.14/5.45 ![A]: (~l1_rlvect_1(A)|l2_struct_0(A))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.14/5.45 fof(f125,plain,(
% 0.14/5.45 ![X0]: (~l1_rlvect_1(X0)|l2_struct_0(X0))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f124])).
% 0.14/5.45 fof(f130,plain,(
% 0.14/5.45 ![A]: (~l2_struct_0(A)|l1_struct_0(A))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.14/5.45 fof(f131,plain,(
% 0.14/5.45 ![X0]: (~l2_struct_0(X0)|l1_struct_0(X0))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f130])).
% 0.14/5.45 fof(f135,plain,(
% 0.14/5.45 ![A]: (~l3_vectsp_1(A)|(l1_rlvect_1(A)&l2_vectsp_1(A)))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.14/5.45 fof(f136,plain,(
% 0.14/5.45 ![X0]: (~l3_vectsp_1(X0)|l1_rlvect_1(X0))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f135])).
% 0.14/5.45 fof(f138,plain,(
% 0.14/5.45 ![A,B]: (((((((((((((((((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))|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)|((((((~v3_struct_0(C)&v3_rlvect_1(C))&v4_rlvect_1(C))&v5_rlvect_1(C))&v6_rlvect_1(C))&v5_vectsp_2(C,A))&l1_vectsp_2(C,A)))))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.14/5.45 fof(f139,plain,(
% 0.14/5.45 ![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)|~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)|~v3_struct_0(X2))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/5.45 fof(f140,plain,(
% 0.14/5.45 ![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)|~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)|v3_rlvect_1(X2))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/5.45 fof(f141,plain,(
% 0.14/5.45 ![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)|~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)|v4_rlvect_1(X2))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/5.45 fof(f142,plain,(
% 0.14/5.45 ![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)|~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)|v5_rlvect_1(X2))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/5.45 fof(f143,plain,(
% 0.14/5.45 ![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)|~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)|v6_rlvect_1(X2))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/5.45 fof(f144,plain,(
% 0.14/5.45 ![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)|~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)|v5_vectsp_2(X2,X0))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/5.45 fof(f145,plain,(
% 0.14/5.45 ![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)|~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)|l1_vectsp_2(X2,X0))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/5.45 fof(f261,plain,(
% 0.14/5.45 ![A]: r1_tarski(A,A)),
% 0.14/5.45 inference(miniscoping,[status(thm)],[f60])).
% 0.14/5.45 fof(f262,plain,(
% 0.14/5.45 ![X0]: (r1_tarski(X0,X0))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f261])).
% 0.14/5.45 fof(f263,plain,(
% 0.14/5.45 ![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))))))))))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.14/5.45 fof(f264,plain,(
% 0.14/5.45 ![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)))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f263])).
% 0.14/5.45 fof(f269,plain,(
% 0.14/5.45 ![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))|~v3_vectsp_2(B,A))|~v5_vectsp_2(B,A))|~l1_vectsp_2(B,A))|(![C]: ((((((((v3_struct_0(C)|~v3_rlvect_1(C))|~v4_rlvect_1(C))|~v5_rlvect_1(C))|~v6_rlvect_1(C))|~v3_vectsp_2(C,A))|~v5_vectsp_2(C,A))|~l1_vectsp_2(C,A))|((~m1_rmod_2(C,A,B)|~m1_rmod_2(B,A,C))|C=B))))))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.14/5.45 fof(f270,plain,(
% 0.14/5.45 ![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)|~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)|~v3_vectsp_2(X1,X0)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|v3_struct_0(X2)|~v3_rlvect_1(X2)|~v4_rlvect_1(X2)|~v5_rlvect_1(X2)|~v6_rlvect_1(X2)|~v3_vectsp_2(X2,X0)|~v5_vectsp_2(X2,X0)|~l1_vectsp_2(X2,X0)|~m1_rmod_2(X2,X0,X1)|~m1_rmod_2(X1,X0,X2)|X2=X1)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f269])).
% 0.14/5.45 fof(f271,plain,(
% 0.14/5.45 ![A,B]: ((~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B))&(m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 0.14/5.45 inference(NNF_transformation,[status(thm)],[f65])).
% 0.14/5.45 fof(f272,plain,(
% 0.14/5.45 (![A,B]: (~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B)))&(![A,B]: (m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 0.14/5.45 inference(miniscoping,[status(thm)],[f271])).
% 0.14/5.45 fof(f273,plain,(
% 0.14/5.45 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|r1_tarski(X0,X1))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f272])).
% 0.14/5.45 fof(f290,definition,(
% 0.14/5.45 sQ0_spl <=> (l1_struct_0(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f292,plain,(
% 0.14/5.45 ~l1_struct_0(sK0_skl)|sQ0_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f290])).
% 0.14/5.45 fof(f293,definition,(
% 0.14/5.45 sQ1_spl <=> (v3_vectsp_2(sK1_skl,sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f295,plain,(
% 0.14/5.45 ~v3_vectsp_2(sK1_skl,sK0_skl)|sQ1_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f293])).
% 0.14/5.45 fof(f301,plain,(
% 0.14/5.45 r1_tarski(sK2_skl,u1_struct_0(sK1_skl))),
% 0.14/5.45 inference(resolution,[status(thm)],[f273,f94])).
% 0.14/5.45 fof(f302,plain,(
% 0.14/5.45 ![X0]: (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)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v3_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl))),
% 0.14/5.45 inference(resolution,[status(thm)],[f120,f93])).
% 0.14/5.45 fof(f303,definition,(
% 0.14/5.45 sQ3_spl <=> (v3_struct_0(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f304,plain,(
% 0.14/5.45 v3_struct_0(sK0_skl)|~sQ3_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f303])).
% 0.14/5.45 fof(f306,definition,(
% 0.14/5.45 sQ4_spl <=> (v3_rlvect_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f308,plain,(
% 0.14/5.45 ~v3_rlvect_1(sK0_skl)|sQ4_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f306])).
% 0.14/5.45 fof(f309,definition,(
% 0.14/5.45 sQ5_spl <=> (v4_rlvect_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f311,plain,(
% 0.14/5.45 ~v4_rlvect_1(sK0_skl)|sQ5_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f309])).
% 0.14/5.45 fof(f312,definition,(
% 0.14/5.45 sQ6_spl <=> (v5_rlvect_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f314,plain,(
% 0.14/5.45 ~v5_rlvect_1(sK0_skl)|sQ6_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f312])).
% 0.14/5.45 fof(f315,definition,(
% 0.14/5.45 sQ7_spl <=> (v6_rlvect_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f317,plain,(
% 0.14/5.45 ~v6_rlvect_1(sK0_skl)|sQ7_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f315])).
% 0.14/5.45 fof(f318,definition,(
% 0.14/5.45 sQ8_spl <=> (v4_group_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f320,plain,(
% 0.14/5.45 ~v4_group_1(sK0_skl)|sQ8_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f318])).
% 0.14/5.45 fof(f321,definition,(
% 0.14/5.45 sQ9_spl <=> (v7_group_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f323,plain,(
% 0.14/5.45 ~v7_group_1(sK0_skl)|sQ9_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f321])).
% 0.14/5.45 fof(f324,definition,(
% 0.14/5.45 sQ10_spl <=> (v6_vectsp_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f326,plain,(
% 0.14/5.45 ~v6_vectsp_1(sK0_skl)|sQ10_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f324])).
% 0.14/5.45 fof(f327,definition,(
% 0.14/5.45 sQ11_spl <=> (v7_vectsp_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f329,plain,(
% 0.14/5.45 ~v7_vectsp_1(sK0_skl)|sQ11_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f327])).
% 0.14/5.45 fof(f330,definition,(
% 0.14/5.45 sQ12_spl <=> (v8_vectsp_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f332,plain,(
% 0.14/5.45 ~v8_vectsp_1(sK0_skl)|sQ12_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f330])).
% 0.14/5.45 fof(f333,definition,(
% 0.14/5.45 sQ13_spl <=> (v10_vectsp_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f334,plain,(
% 0.14/5.45 v10_vectsp_1(sK0_skl)|~sQ13_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f333])).
% 0.14/5.45 fof(f336,definition,(
% 0.14/5.45 sQ14_spl <=> (v2_vectsp_2(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f338,plain,(
% 0.14/5.45 ~v2_vectsp_2(sK0_skl)|sQ14_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f336])).
% 0.14/5.45 fof(f339,definition,(
% 0.14/5.45 sQ15_spl <=> (l3_vectsp_1(sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f341,plain,(
% 0.14/5.45 ~l3_vectsp_1(sK0_skl)|sQ15_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f339])).
% 0.14/5.45 fof(f342,definition,(
% 0.14/5.45 sQ16_spl <=> (v3_struct_0(sK1_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f343,plain,(
% 0.14/5.45 v3_struct_0(sK1_skl)|~sQ16_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f342])).
% 0.14/5.45 fof(f345,definition,(
% 0.14/5.45 sQ17_spl <=> (v3_rlvect_1(sK1_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f347,plain,(
% 0.14/5.45 ~v3_rlvect_1(sK1_skl)|sQ17_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f345])).
% 0.14/5.45 fof(f348,definition,(
% 0.14/5.45 sQ18_spl <=> (v4_rlvect_1(sK1_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f350,plain,(
% 0.14/5.45 ~v4_rlvect_1(sK1_skl)|sQ18_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f348])).
% 0.14/5.45 fof(f351,definition,(
% 0.14/5.45 sQ19_spl <=> (v5_rlvect_1(sK1_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f353,plain,(
% 0.14/5.45 ~v5_rlvect_1(sK1_skl)|sQ19_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f351])).
% 0.14/5.45 fof(f354,definition,(
% 0.14/5.45 sQ20_spl <=> (v6_rlvect_1(sK1_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f356,plain,(
% 0.14/5.45 ~v6_rlvect_1(sK1_skl)|sQ20_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f354])).
% 0.14/5.45 fof(f357,definition,(
% 0.14/5.45 sQ21_spl <=> (v5_vectsp_2(sK1_skl,sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f359,plain,(
% 0.14/5.45 ~v5_vectsp_2(sK1_skl,sK0_skl)|sQ21_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f357])).
% 0.14/5.45 fof(f360,definition,(
% 0.14/5.45 ![X0]: (sQ22_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v3_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl)))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f361,plain,(
% 0.14/5.45 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v3_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl)|~sQ22_spl)),
% 0.14/5.45 inference(component_clause,[status(thm)],[f360])).
% 0.14/5.45 fof(f363,plain,(
% 0.14/5.45 sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ13_spl|~sQ14_spl|~sQ15_spl|sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ21_spl|sQ22_spl),
% 0.14/5.45 inference(split_clause,[status(thm)],[f302,f303,f306,f309,f312,f315,f318,f321,f324,f327,f330,f333,f336,f339,f342,f345,f348,f351,f354,f357,f360])).
% 0.14/5.45 fof(f364,plain,(
% 0.14/5.45 $false|sQ21_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f359,f92])).
% 0.14/5.45 fof(f365,plain,(
% 0.14/5.45 sQ21_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f364])).
% 0.14/5.45 fof(f366,plain,(
% 0.14/5.45 $false|sQ20_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f356,f90])).
% 0.14/5.45 fof(f367,plain,(
% 0.14/5.45 sQ20_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f366])).
% 0.14/5.45 fof(f368,plain,(
% 0.14/5.45 $false|sQ19_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f353,f89])).
% 0.14/5.45 fof(f369,plain,(
% 0.14/5.45 sQ19_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f368])).
% 0.14/5.45 fof(f370,plain,(
% 0.14/5.45 $false|sQ18_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f350,f88])).
% 0.14/5.45 fof(f371,plain,(
% 0.14/5.45 sQ18_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f370])).
% 0.14/5.45 fof(f372,plain,(
% 0.14/5.45 $false|sQ17_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f347,f87])).
% 0.14/5.45 fof(f373,plain,(
% 0.14/5.45 sQ17_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f372])).
% 0.14/5.45 fof(f374,plain,(
% 0.14/5.45 $false|~sQ16_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f343,f86])).
% 0.14/5.45 fof(f375,plain,(
% 0.14/5.45 ~sQ16_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f374])).
% 0.14/5.45 fof(f376,plain,(
% 0.14/5.45 $false|sQ15_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f341,f85])).
% 0.14/5.45 fof(f377,plain,(
% 0.14/5.45 sQ15_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f376])).
% 0.14/5.45 fof(f378,plain,(
% 0.14/5.45 $false|sQ14_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f338,f84])).
% 0.14/5.45 fof(f379,plain,(
% 0.14/5.45 sQ14_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f378])).
% 0.14/5.45 fof(f380,plain,(
% 0.14/5.45 $false|~sQ13_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f334,f83])).
% 0.14/5.45 fof(f381,plain,(
% 0.14/5.45 ~sQ13_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f380])).
% 0.14/5.45 fof(f382,plain,(
% 0.14/5.45 $false|sQ12_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f332,f82])).
% 0.14/5.45 fof(f383,plain,(
% 0.14/5.45 sQ12_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f382])).
% 0.14/5.45 fof(f384,plain,(
% 0.14/5.45 $false|sQ11_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f329,f81])).
% 0.14/5.45 fof(f385,plain,(
% 0.14/5.45 sQ11_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f384])).
% 0.14/5.45 fof(f386,plain,(
% 0.14/5.45 $false|sQ10_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f326,f80])).
% 0.14/5.45 fof(f387,plain,(
% 0.14/5.45 sQ10_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f386])).
% 0.14/5.45 fof(f388,plain,(
% 0.14/5.45 $false|sQ9_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f323,f79])).
% 0.14/5.45 fof(f389,plain,(
% 0.14/5.45 sQ9_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f388])).
% 0.14/5.45 fof(f390,plain,(
% 0.14/5.45 $false|sQ8_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f320,f78])).
% 0.14/5.45 fof(f391,plain,(
% 0.14/5.45 sQ8_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f390])).
% 0.14/5.45 fof(f392,plain,(
% 0.14/5.45 $false|sQ7_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f317,f77])).
% 0.14/5.45 fof(f393,plain,(
% 0.14/5.45 sQ7_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f392])).
% 0.14/5.45 fof(f394,plain,(
% 0.14/5.45 $false|sQ6_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f314,f76])).
% 0.14/5.45 fof(f395,plain,(
% 0.14/5.45 sQ6_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f394])).
% 0.14/5.45 fof(f396,plain,(
% 0.14/5.45 $false|sQ5_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f311,f75])).
% 0.14/5.45 fof(f397,plain,(
% 0.14/5.45 sQ5_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f396])).
% 0.14/5.45 fof(f398,plain,(
% 0.14/5.45 $false|sQ4_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f308,f74])).
% 0.14/5.45 fof(f399,plain,(
% 0.14/5.45 sQ4_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f398])).
% 0.14/5.45 fof(f400,plain,(
% 0.14/5.45 $false|~sQ3_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f304,f73])).
% 0.14/5.45 fof(f401,plain,(
% 0.14/5.45 ~sQ3_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f400])).
% 0.14/5.45 fof(f402,plain,(
% 0.14/5.45 ![X0]: (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)|~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))),
% 0.14/5.45 inference(resolution,[status(thm)],[f121,f93])).
% 0.14/5.45 fof(f403,definition,(
% 0.14/5.45 ![X0]: (sQ23_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)))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f404,plain,(
% 0.14/5.45 ![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)|~sQ23_spl)),
% 0.14/5.45 inference(component_clause,[status(thm)],[f403])).
% 0.14/5.45 fof(f406,plain,(
% 0.14/5.45 sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ13_spl|~sQ14_spl|~sQ15_spl|sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ21_spl|sQ23_spl),
% 0.14/5.45 inference(split_clause,[status(thm)],[f402,f303,f306,f309,f312,f315,f318,f321,f324,f327,f330,f333,f336,f339,f342,f345,f348,f351,f354,f357,f403])).
% 0.14/5.45 fof(f426,plain,(
% 0.14/5.45 v3_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl)|~sQ22_spl),
% 0.14/5.45 inference(resolution,[status(thm)],[f361,f95])).
% 0.14/5.45 fof(f436,plain,(
% 0.14/5.45 ![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)|~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)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(X0,X1)|m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,X1)))),
% 0.14/5.45 inference(resolution,[status(thm)],[f264,f93])).
% 0.14/5.45 fof(f437,definition,(
% 0.14/5.45 ![X0,X1]: (sQ29_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(X0,X1)|m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,X1))))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f438,plain,(
% 0.14/5.45 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(X0,X1)|m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,X0),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,X1))|~sQ29_spl)),
% 0.14/5.45 inference(component_clause,[status(thm)],[f437])).
% 0.14/5.45 fof(f440,plain,(
% 0.14/5.45 sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ13_spl|~sQ14_spl|~sQ15_spl|sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ21_spl|sQ29_spl),
% 0.14/5.45 inference(split_clause,[status(thm)],[f436,f303,f306,f309,f312,f315,f318,f321,f324,f327,f330,f333,f336,f339,f342,f345,f348,f351,f354,f357,f437])).
% 0.14/5.45 fof(f446,plain,(
% 0.14/5.45 m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl,sK1_skl)|~sQ23_spl),
% 0.14/5.45 inference(resolution,[status(thm)],[f404,f95])).
% 0.14/5.45 fof(f451,definition,(
% 0.14/5.45 sQ30_spl <=> (l1_vectsp_2(sK1_skl,sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f453,plain,(
% 0.14/5.45 ~l1_vectsp_2(sK1_skl,sK0_skl)|sQ30_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f451])).
% 0.14/5.45 fof(f461,plain,(
% 0.14/5.45 $false|sQ1_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f295,f91])).
% 0.14/5.45 fof(f462,plain,(
% 0.14/5.45 sQ1_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f461])).
% 0.14/5.45 fof(f464,plain,(
% 0.14/5.45 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(sK2_skl,X0)|m1_rmod_2(k1_rmod_5(sK0_skl,sK1_skl,sK2_skl),sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,X0))|~sQ29_spl)),
% 0.14/5.45 inference(resolution,[status(thm)],[f438,f94])).
% 0.14/5.45 fof(f466,plain,(
% 0.14/5.45 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(sK2_skl,X0)|m1_rmod_2(sK1_skl,sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,X0))|~sQ29_spl)),
% 0.14/5.45 inference(forward_demodulation,[status(thm)],[f96,f464])).
% 0.14/5.45 fof(f486,definition,(
% 0.14/5.45 sQ38_spl <=> (v3_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f488,plain,(
% 0.14/5.45 ~v3_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl)|sQ38_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f486])).
% 0.14/5.45 fof(f489,definition,(
% 0.14/5.45 sQ39_spl <=> (v5_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f492,definition,(
% 0.14/5.45 sQ40_spl <=> (l1_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f495,definition,(
% 0.14/5.45 sQ41_spl <=> (m1_rmod_2(sK1_skl,sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f498,definition,(
% 0.14/5.45 sQ42_spl <=> (k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)=sK1_skl)),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f499,plain,(
% 0.14/5.45 k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)=sK1_skl|~sQ42_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f498])).
% 0.14/5.45 fof(f502,plain,(
% 0.14/5.45 $false|sQ30_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f453,f93])).
% 0.14/5.45 fof(f503,plain,(
% 0.14/5.45 sQ30_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f502])).
% 0.14/5.45 fof(f506,plain,(
% 0.14/5.45 $false|~sQ42_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f499,f98])).
% 0.14/5.45 fof(f507,plain,(
% 0.14/5.45 ~sQ42_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f506])).
% 0.14/5.45 fof(f581,plain,(
% 0.14/5.45 ~r1_tarski(sK2_skl,sK3_skl)|m1_rmod_2(sK1_skl,sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK3_skl))|~sQ29_spl),
% 0.14/5.45 inference(resolution,[status(thm)],[f466,f95])).
% 0.14/5.45 fof(f584,definition,(
% 0.14/5.45 sQ60_spl <=> (r1_tarski(sK2_skl,sK3_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f586,plain,(
% 0.14/5.45 ~r1_tarski(sK2_skl,sK3_skl)|sQ60_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f584])).
% 0.14/5.45 fof(f587,plain,(
% 0.14/5.45 ~sQ60_spl|sQ41_spl|~sQ29_spl),
% 0.14/5.45 inference(split_clause,[status(thm)],[f581,f584,f495,f437])).
% 0.14/5.45 fof(f588,definition,(
% 0.14/5.45 sQ61_spl <=> (r1_tarski(sK2_skl,sK2_skl))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f590,plain,(
% 0.14/5.45 ~r1_tarski(sK2_skl,sK2_skl)|sQ61_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f588])).
% 0.14/5.45 fof(f595,definition,(
% 0.14/5.45 sQ63_spl <=> (r1_tarski(sK2_skl,u1_struct_0(sK1_skl)))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f597,plain,(
% 0.14/5.45 ~r1_tarski(sK2_skl,u1_struct_0(sK1_skl))|sQ63_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f595])).
% 0.14/5.45 fof(f599,plain,(
% 0.14/5.45 $false|sQ60_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f586,f97])).
% 0.14/5.45 fof(f600,plain,(
% 0.14/5.45 sQ60_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f599])).
% 0.14/5.45 fof(f601,plain,(
% 0.14/5.45 $false|sQ61_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f590,f262])).
% 0.14/5.45 fof(f602,plain,(
% 0.14/5.45 sQ61_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f601])).
% 0.14/5.45 fof(f603,plain,(
% 0.14/5.45 $false|sQ63_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f597,f301])).
% 0.14/5.45 fof(f604,plain,(
% 0.14/5.45 sQ63_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f603])).
% 0.14/5.45 fof(f624,definition,(
% 0.14/5.45 sQ68_spl <=> (r1_tarski(u1_struct_0(sK1_skl),u1_struct_0(sK1_skl)))),
% 0.14/5.45 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.14/5.45 fof(f626,plain,(
% 0.14/5.45 ~r1_tarski(u1_struct_0(sK1_skl),u1_struct_0(sK1_skl))|sQ68_spl),
% 0.14/5.45 inference(component_clause,[status(thm)],[f624])).
% 0.14/5.45 fof(f631,plain,(
% 0.14/5.45 $false|sQ68_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f626,f262])).
% 0.14/5.45 fof(f632,plain,(
% 0.14/5.45 sQ68_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f631])).
% 0.14/5.45 fof(f640,plain,(
% 0.14/5.45 l1_rlvect_1(sK0_skl)),
% 0.14/5.45 inference(resolution,[status(thm)],[f136,f85])).
% 0.14/5.45 fof(f643,plain,(
% 0.14/5.45 l2_struct_0(sK0_skl)),
% 0.14/5.45 inference(resolution,[status(thm)],[f640,f125])).
% 0.14/5.45 fof(f646,plain,(
% 0.14/5.45 l1_struct_0(sK0_skl)),
% 0.14/5.45 inference(resolution,[status(thm)],[f643,f131])).
% 0.14/5.45 fof(f647,plain,(
% 0.14/5.45 $false|sQ0_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f646,f292])).
% 0.14/5.45 fof(f648,plain,(
% 0.14/5.45 sQ0_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f647])).
% 0.14/5.45 fof(f673,plain,(
% 0.14/5.45 ![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)|~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)|~v3_vectsp_2(X1,X0)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~v3_rlvect_1(X2)|~v4_rlvect_1(X2)|~v5_rlvect_1(X2)|~v6_rlvect_1(X2)|~v3_vectsp_2(X2,X0)|~v5_vectsp_2(X2,X0)|~l1_vectsp_2(X2,X0)|~m1_rmod_2(X2,X0,X1)|~m1_rmod_2(X1,X0,X2)|X2=X1)),
% 0.14/5.45 inference(backward_subsumption_resolution,[status(thm)],[f270,f139])).
% 0.14/5.45 fof(f705,plain,(
% 0.14/5.45 ![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)|~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)|~v3_vectsp_2(X1,X0)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~v4_rlvect_1(X2)|~v5_rlvect_1(X2)|~v6_rlvect_1(X2)|~v3_vectsp_2(X2,X0)|~v5_vectsp_2(X2,X0)|~l1_vectsp_2(X2,X0)|~m1_rmod_2(X2,X0,X1)|~m1_rmod_2(X1,X0,X2)|X2=X1)),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f673,f140])).
% 0.14/5.45 fof(f710,plain,(
% 0.14/5.45 $false|~sQ22_spl|sQ38_spl),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f488,f426])).
% 0.14/5.45 fof(f711,plain,(
% 0.14/5.45 ~sQ22_spl|sQ38_spl),
% 0.14/5.45 inference(contradiction_clause,[status(thm)],[f710])).
% 0.14/5.45 fof(f720,plain,(
% 0.14/5.45 ![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)|~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)|~v3_vectsp_2(X1,X0)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~v4_rlvect_1(X2)|~v6_rlvect_1(X2)|~v3_vectsp_2(X2,X0)|~v5_vectsp_2(X2,X0)|~l1_vectsp_2(X2,X0)|~m1_rmod_2(X2,X0,X1)|~m1_rmod_2(X1,X0,X2)|X2=X1)),
% 0.14/5.45 inference(backward_subsumption_resolution,[status(thm)],[f705,f142])).
% 0.14/5.45 fof(f723,plain,(
% 0.14/5.45 ![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)|~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)|~v3_vectsp_2(X1,X0)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~v6_rlvect_1(X2)|~v3_vectsp_2(X2,X0)|~v5_vectsp_2(X2,X0)|~l1_vectsp_2(X2,X0)|~m1_rmod_2(X2,X0,X1)|~m1_rmod_2(X1,X0,X2)|X2=X1)),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f720,f141])).
% 0.14/5.45 fof(f730,plain,(
% 0.14/5.45 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)|~v8_vectsp_1(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)|v5_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl)|~sQ23_spl),
% 0.14/5.45 inference(resolution,[status(thm)],[f144,f446])).
% 0.14/5.45 fof(f732,plain,(
% 0.14/5.45 sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ15_spl|sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ21_spl|~sQ30_spl|sQ39_spl|~sQ23_spl),
% 0.14/5.45 inference(split_clause,[status(thm)],[f730,f303,f306,f309,f312,f315,f318,f324,f327,f330,f339,f342,f345,f348,f351,f354,f357,f451,f489,f403])).
% 0.14/5.45 fof(f746,plain,(
% 0.14/5.45 ![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)|~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)|~v3_vectsp_2(X1,X0)|~v5_vectsp_2(X1,X0)|~l1_vectsp_2(X1,X0)|~v3_vectsp_2(X2,X0)|~v5_vectsp_2(X2,X0)|~l1_vectsp_2(X2,X0)|~m1_rmod_2(X2,X0,X1)|~m1_rmod_2(X1,X0,X2)|X2=X1)),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f723,f143])).
% 0.14/5.45 fof(f748,plain,(
% 0.14/5.45 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)|~v8_vectsp_1(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)|~v3_vectsp_2(sK1_skl,sK0_skl)|~v5_vectsp_2(sK1_skl,sK0_skl)|~l1_vectsp_2(sK1_skl,sK0_skl)|~v3_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl)|~v5_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl)|~l1_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl)|~m1_rmod_2(sK1_skl,sK0_skl,k1_rmod_5(sK0_skl,sK1_skl,sK3_skl))|k1_rmod_5(sK0_skl,sK1_skl,sK3_skl)=sK1_skl|~sQ23_spl),
% 0.14/5.46 inference(resolution,[status(thm)],[f746,f446])).
% 0.14/5.46 fof(f751,plain,(
% 0.14/5.46 sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ15_spl|sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ1_spl|~sQ21_spl|~sQ30_spl|~sQ38_spl|~sQ39_spl|~sQ40_spl|~sQ41_spl|sQ42_spl|~sQ23_spl),
% 0.14/5.46 inference(split_clause,[status(thm)],[f748,f303,f306,f309,f312,f315,f318,f324,f327,f330,f339,f342,f345,f348,f351,f354,f293,f357,f451,f486,f489,f492,f495,f498,f403])).
% 0.14/5.46 fof(f758,plain,(
% 0.14/5.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)|~v6_vectsp_1(sK0_skl)|~v7_vectsp_1(sK0_skl)|~v8_vectsp_1(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)|l1_vectsp_2(k1_rmod_5(sK0_skl,sK1_skl,sK3_skl),sK0_skl)|~sQ23_spl),
% 0.14/5.46 inference(resolution,[status(thm)],[f145,f446])).
% 0.14/5.46 fof(f762,plain,(
% 0.14/5.46 sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ15_spl|sQ16_spl|~sQ17_spl|~sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ21_spl|~sQ30_spl|sQ40_spl|~sQ23_spl),
% 0.14/5.46 inference(split_clause,[status(thm)],[f758,f303,f306,f309,f312,f315,f318,f324,f327,f330,f339,f342,f345,f348,f351,f354,f357,f451,f492,f403])).
% 0.14/5.46 fof(f764,plain,(
% 0.14/5.46 $false),
% 0.14/5.46 inference(sat_refutation,[status(thm)],[f363,f365,f367,f369,f371,f373,f375,f377,f379,f381,f383,f385,f387,f389,f391,f393,f395,f397,f399,f401,f406,f440,f462,f503,f507,f587,f600,f602,f604,f632,f648,f711,f732,f751,f762])).
% 0.14/5.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.48 % Elapsed time: 0.085277 seconds
% 0.14/5.48 % CPU time: 0.322314 seconds
% 0.14/5.48 % Total memory used: 112.343 MB
% 0.14/5.48 % Net memory used: 111.962 MB
%------------------------------------------------------------------------------