%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG214+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 : n009.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:49 AM UTC 2026
% Result : Theorem 0.14s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG214+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.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 13:01:57 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 0.14/0.42 % Refutation found
% 0.14/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.42 fof(f1,conjecture,(
% 0.14/0.42 (! [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_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)& v1_rmod_5(D,A,B) )=> v1_rmod_5(C,A,B) ) ) )) )) )) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f2,negated_conjecture,(
% 0.14/0.42 ~((! [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_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)& v1_rmod_5(D,A,B) )=> v1_rmod_5(C,A,B) ) ) )) )) )) ))),
% 0.14/0.42 inference(negated_conjecture,[status(cth)],[f1])).
% 0.14/0.42 fof(f5,axiom,(
% 0.14/0.42 (! [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_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))=> ( v1_rmod_5(C,A,B)<=> (! [D] :( m2_rmod_4(D,A,B,C)=> ( k5_rmod_4(A,B,D) = k1_rlvect_1(B)=> k2_rmod_4(A,B,D) = k1_xboole_0 ) ) )) ) )) )) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f54,axiom,(
% 0.14/0.42 (? [A] : v1_xboole_0(A) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f68,axiom,(
% 0.14/0.42 (! [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_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))=> (! [E] :( m2_rmod_4(E,A,B,C)=> ( r1_tarski(C,D)=> m2_rmod_4(E,A,B,D) ) ) )) )) )) )) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f74,axiom,(
% 0.14/0.42 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f77,plain,(
% 0.14/0.42 (?[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_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)&v1_rmod_5(D,A,B))&~v1_rmod_5(C,A,B))))))))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.42 fof(f78,plain,(
% 0.14/0.42 ((((((((((~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))&(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)))&((r1_tarski(sK2_skl,sK3_skl)&v1_rmod_5(sK3_skl,sK0_skl,sK1_skl))&~v1_rmod_5(sK2_skl,sK0_skl,sK1_skl))))))),
% 0.14/0.42 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)],[f77])).
% 0.14/0.42 fof(f79,plain,(
% 0.14/0.42 ~v3_struct_0(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f80,plain,(
% 0.14/0.42 v3_rlvect_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f81,plain,(
% 0.14/0.42 v4_rlvect_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f82,plain,(
% 0.14/0.42 v5_rlvect_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f83,plain,(
% 0.14/0.42 v6_rlvect_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f84,plain,(
% 0.14/0.42 v4_group_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f85,plain,(
% 0.14/0.42 v6_vectsp_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f86,plain,(
% 0.14/0.42 v7_vectsp_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f87,plain,(
% 0.14/0.42 v8_vectsp_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f88,plain,(
% 0.14/0.42 l3_vectsp_1(sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f89,plain,(
% 0.14/0.42 ~v3_struct_0(sK1_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f90,plain,(
% 0.14/0.42 v3_rlvect_1(sK1_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f91,plain,(
% 0.14/0.42 v4_rlvect_1(sK1_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f92,plain,(
% 0.14/0.42 v5_rlvect_1(sK1_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f93,plain,(
% 0.14/0.42 v6_rlvect_1(sK1_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f94,plain,(
% 0.14/0.42 v5_vectsp_2(sK1_skl,sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f95,plain,(
% 0.14/0.42 l1_vectsp_2(sK1_skl,sK0_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f96,plain,(
% 0.14/0.42 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f97,plain,(
% 0.14/0.42 m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f98,plain,(
% 0.14/0.42 r1_tarski(sK2_skl,sK3_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f99,plain,(
% 0.14/0.42 v1_rmod_5(sK3_skl,sK0_skl,sK1_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f100,plain,(
% 0.14/0.42 ~v1_rmod_5(sK2_skl,sK0_skl,sK1_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.42 fof(f106,plain,(
% 0.14/0.42 ![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_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|(v1_rmod_5(C,A,B)<=>(![D]: (~m2_rmod_4(D,A,B,C)|(~k5_rmod_4(A,B,D)=k1_rlvect_1(B)|k2_rmod_4(A,B,D)=k1_xboole_0)))))))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.14/0.42 fof(f107,plain,(
% 0.14/0.42 ![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_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|((~v1_rmod_5(C,A,B)|(![D]: (~m2_rmod_4(D,A,B,C)|(~k5_rmod_4(A,B,D)=k1_rlvect_1(B)|k2_rmod_4(A,B,D)=k1_xboole_0))))&(v1_rmod_5(C,A,B)|(?[D]: (m2_rmod_4(D,A,B,C)&(k5_rmod_4(A,B,D)=k1_rlvect_1(B)&~k2_rmod_4(A,B,D)=k1_xboole_0))))))))))),
% 0.14/0.42 inference(NNF_transformation,[status(thm)],[f106])).
% 0.14/0.42 fof(f108,plain,(
% 0.14/0.42 ![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_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|((~v1_rmod_5(C,A,B)|(![D]: (~m2_rmod_4(D,A,B,C)|(~k5_rmod_4(A,B,D)=k1_rlvect_1(B)|k2_rmod_4(A,B,D)=k1_xboole_0))))&(v1_rmod_5(C,A,B)|(m2_rmod_4(sK4_skl(C,B,A),A,B,C)&(k5_rmod_4(A,B,sK4_skl(C,B,A))=k1_rlvect_1(B)&~k2_rmod_4(A,B,sK4_skl(C,B,A))=k1_xboole_0)))))))))),
% 0.14/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(D,sK4_skl(C,B,A))],[f107])).
% 0.14/0.42 fof(f109,plain,(
% 0.14/0.42 ![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)|~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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|~v1_rmod_5(X2,X0,X1)|~m2_rmod_4(X3,X0,X1,X2)|~k5_rmod_4(X0,X1,X3)=k1_rlvect_1(X1)|k2_rmod_4(X0,X1,X3)=k1_xboole_0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f108])).
% 0.14/0.42 fof(f110,plain,(
% 0.14/0.42 ![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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|v1_rmod_5(X2,X0,X1)|m2_rmod_4(sK4_skl(X2,X1,X0),X0,X1,X2))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f108])).
% 0.14/0.42 fof(f111,plain,(
% 0.14/0.42 ![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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|v1_rmod_5(X2,X0,X1)|k5_rmod_4(X0,X1,sK4_skl(X2,X1,X0))=k1_rlvect_1(X1))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f108])).
% 0.14/0.42 fof(f112,plain,(
% 0.14/0.42 ![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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|v1_rmod_5(X2,X0,X1)|~k2_rmod_4(X0,X1,sK4_skl(X2,X1,X0))=k1_xboole_0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f108])).
% 0.14/0.42 fof(f209,plain,(
% 0.14/0.42 v1_xboole_0(sK22_skl)),
% 0.14/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(A,sK22_skl)],[f54])).
% 0.14/0.42 fof(f210,plain,(
% 0.14/0.42 v1_xboole_0(sK22_skl)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f209])).
% 0.14/0.42 fof(f253,plain,(
% 0.14/0.42 ![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_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|(![D]: (~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))|(![E]: (~m2_rmod_4(E,A,B,C)|(~r1_tarski(C,D)|m2_rmod_4(E,A,B,D)))))))))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.14/0.42 fof(f254,plain,(
% 0.14/0.42 ![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_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))|~m2_rmod_4(X4,X0,X1,X2)|~r1_tarski(X2,X3)|m2_rmod_4(X4,X0,X1,X3))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f253])).
% 0.14/0.42 fof(f272,plain,(
% 0.14/0.42 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 0.14/0.42 fof(f273,plain,(
% 0.14/0.42 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f272])).
% 0.14/0.42 fof(f293,plain,(
% 0.14/0.42 ![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_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_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_rmod_5(X1,sK0_skl,X0)|k5_rmod_4(sK0_skl,X0,sK4_skl(X1,X0,sK0_skl))=k1_rlvect_1(X0))),
% 0.14/0.42 inference(resolution,[status(thm)],[f111,f85])).
% 0.14/0.42 fof(f296,definition,(
% 0.14/0.42 sQ0_spl <=> (v3_struct_0(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f297,plain,(
% 0.14/0.42 v3_struct_0(sK0_skl)|~sQ0_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f296])).
% 0.14/0.42 fof(f299,definition,(
% 0.14/0.42 sQ1_spl <=> (v3_rlvect_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f301,plain,(
% 0.14/0.42 ~v3_rlvect_1(sK0_skl)|sQ1_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f299])).
% 0.14/0.42 fof(f302,definition,(
% 0.14/0.42 sQ2_spl <=> (v4_rlvect_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f304,plain,(
% 0.14/0.42 ~v4_rlvect_1(sK0_skl)|sQ2_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f302])).
% 0.14/0.42 fof(f305,definition,(
% 0.14/0.42 sQ3_spl <=> (v5_rlvect_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f307,plain,(
% 0.14/0.42 ~v5_rlvect_1(sK0_skl)|sQ3_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f305])).
% 0.14/0.42 fof(f308,definition,(
% 0.14/0.42 sQ4_spl <=> (v6_rlvect_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f310,plain,(
% 0.14/0.42 ~v6_rlvect_1(sK0_skl)|sQ4_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f308])).
% 0.14/0.42 fof(f311,definition,(
% 0.14/0.42 sQ5_spl <=> (v4_group_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f313,plain,(
% 0.14/0.42 ~v4_group_1(sK0_skl)|sQ5_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f311])).
% 0.14/0.42 fof(f314,definition,(
% 0.14/0.42 sQ6_spl <=> (v7_vectsp_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f316,plain,(
% 0.14/0.42 ~v7_vectsp_1(sK0_skl)|sQ6_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f314])).
% 0.14/0.42 fof(f317,definition,(
% 0.14/0.42 sQ7_spl <=> (v8_vectsp_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f319,plain,(
% 0.14/0.42 ~v8_vectsp_1(sK0_skl)|sQ7_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f317])).
% 0.14/0.42 fof(f320,definition,(
% 0.14/0.42 sQ8_spl <=> (l3_vectsp_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f322,plain,(
% 0.14/0.42 ~l3_vectsp_1(sK0_skl)|sQ8_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f320])).
% 0.14/0.42 fof(f323,definition,(
% 0.14/0.42 ![X0,X1]: (sQ9_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)))|v1_rmod_5(X1,sK0_skl,X0)|k5_rmod_4(sK0_skl,X0,sK4_skl(X1,X0,sK0_skl))=k1_rlvect_1(X0)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f324,plain,(
% 0.14/0.42 ![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)))|v1_rmod_5(X1,sK0_skl,X0)|k5_rmod_4(sK0_skl,X0,sK4_skl(X1,X0,sK0_skl))=k1_rlvect_1(X0)|~sQ9_spl)),
% 0.14/0.42 inference(component_clause,[status(thm)],[f323])).
% 0.14/0.42 fof(f326,plain,(
% 0.14/0.42 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ9_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f293,f296,f299,f302,f305,f308,f311,f314,f317,f320,f323])).
% 0.14/0.42 fof(f327,definition,(
% 0.14/0.42 sQ10_spl <=> (v6_vectsp_1(sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f329,plain,(
% 0.14/0.42 ~v6_vectsp_1(sK0_skl)|sQ10_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f327])).
% 0.14/0.42 fof(f334,plain,(
% 0.14/0.42 ![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)|~v5_vectsp_2(sK1_skl,sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|k5_rmod_4(sK0_skl,sK1_skl,sK4_skl(X0,sK1_skl,sK0_skl))=k1_rlvect_1(sK1_skl)|~sQ9_spl)),
% 0.14/0.42 inference(resolution,[status(thm)],[f324,f95])).
% 0.14/0.42 fof(f335,definition,(
% 0.14/0.42 sQ11_spl <=> (v3_struct_0(sK1_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f336,plain,(
% 0.14/0.42 v3_struct_0(sK1_skl)|~sQ11_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f335])).
% 0.14/0.42 fof(f338,definition,(
% 0.14/0.42 sQ12_spl <=> (v3_rlvect_1(sK1_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f340,plain,(
% 0.14/0.42 ~v3_rlvect_1(sK1_skl)|sQ12_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f338])).
% 0.14/0.42 fof(f341,definition,(
% 0.14/0.42 sQ13_spl <=> (v4_rlvect_1(sK1_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f343,plain,(
% 0.14/0.42 ~v4_rlvect_1(sK1_skl)|sQ13_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f341])).
% 0.14/0.42 fof(f344,definition,(
% 0.14/0.42 sQ14_spl <=> (v5_rlvect_1(sK1_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f346,plain,(
% 0.14/0.42 ~v5_rlvect_1(sK1_skl)|sQ14_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f344])).
% 0.14/0.42 fof(f347,definition,(
% 0.14/0.42 sQ15_spl <=> (v6_rlvect_1(sK1_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f349,plain,(
% 0.14/0.42 ~v6_rlvect_1(sK1_skl)|sQ15_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f347])).
% 0.14/0.42 fof(f350,definition,(
% 0.14/0.42 sQ16_spl <=> (v5_vectsp_2(sK1_skl,sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f352,plain,(
% 0.14/0.42 ~v5_vectsp_2(sK1_skl,sK0_skl)|sQ16_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f350])).
% 0.14/0.42 fof(f353,definition,(
% 0.14/0.42 ![X0]: (sQ17_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|k5_rmod_4(sK0_skl,sK1_skl,sK4_skl(X0,sK1_skl,sK0_skl))=k1_rlvect_1(sK1_skl)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f354,plain,(
% 0.14/0.42 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|k5_rmod_4(sK0_skl,sK1_skl,sK4_skl(X0,sK1_skl,sK0_skl))=k1_rlvect_1(sK1_skl)|~sQ17_spl)),
% 0.14/0.42 inference(component_clause,[status(thm)],[f353])).
% 0.14/0.42 fof(f356,plain,(
% 0.14/0.42 sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|sQ17_spl|~sQ9_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f334,f335,f338,f341,f344,f347,f350,f353,f323])).
% 0.14/0.42 fof(f357,plain,(
% 0.14/0.42 $false|sQ8_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f322,f88])).
% 0.14/0.42 fof(f358,plain,(
% 0.14/0.42 sQ8_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f357])).
% 0.14/0.42 fof(f359,plain,(
% 0.14/0.42 $false|sQ5_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f313,f84])).
% 0.14/0.42 fof(f360,plain,(
% 0.14/0.42 sQ5_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f359])).
% 0.14/0.42 fof(f361,plain,(
% 0.14/0.42 $false|sQ4_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f310,f83])).
% 0.14/0.42 fof(f362,plain,(
% 0.14/0.42 sQ4_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f361])).
% 0.14/0.42 fof(f363,plain,(
% 0.14/0.42 $false|sQ3_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f307,f82])).
% 0.14/0.42 fof(f364,plain,(
% 0.14/0.42 sQ3_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f363])).
% 0.14/0.42 fof(f365,plain,(
% 0.14/0.42 $false|sQ2_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f304,f81])).
% 0.14/0.42 fof(f366,plain,(
% 0.14/0.42 sQ2_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f365])).
% 0.14/0.42 fof(f367,plain,(
% 0.14/0.42 $false|sQ1_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f301,f80])).
% 0.14/0.42 fof(f368,plain,(
% 0.14/0.42 sQ1_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f367])).
% 0.14/0.42 fof(f369,plain,(
% 0.14/0.42 $false|~sQ0_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f297,f79])).
% 0.14/0.42 fof(f370,plain,(
% 0.14/0.42 ~sQ0_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f369])).
% 0.14/0.42 fof(f371,plain,(
% 0.14/0.42 $false|sQ6_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f316,f86])).
% 0.14/0.42 fof(f372,plain,(
% 0.14/0.42 sQ6_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f371])).
% 0.14/0.42 fof(f373,plain,(
% 0.14/0.42 $false|sQ10_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f329,f85])).
% 0.14/0.42 fof(f374,plain,(
% 0.14/0.42 sQ10_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f373])).
% 0.14/0.42 fof(f375,plain,(
% 0.14/0.42 $false|sQ7_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f319,f87])).
% 0.14/0.42 fof(f376,plain,(
% 0.14/0.42 sQ7_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f375])).
% 0.14/0.42 fof(f381,plain,(
% 0.14/0.42 v1_rmod_5(sK2_skl,sK0_skl,sK1_skl)|k5_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=k1_rlvect_1(sK1_skl)|~sQ17_spl),
% 0.14/0.42 inference(resolution,[status(thm)],[f354,f96])).
% 0.14/0.42 fof(f383,definition,(
% 0.14/0.42 sQ18_spl <=> (v1_rmod_5(sK3_skl,sK0_skl,sK1_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f385,plain,(
% 0.14/0.42 ~v1_rmod_5(sK3_skl,sK0_skl,sK1_skl)|sQ18_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f383])).
% 0.14/0.42 fof(f390,definition,(
% 0.14/0.42 sQ20_spl <=> (v1_rmod_5(sK2_skl,sK0_skl,sK1_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f391,plain,(
% 0.14/0.42 v1_rmod_5(sK2_skl,sK0_skl,sK1_skl)|~sQ20_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f390])).
% 0.14/0.42 fof(f393,definition,(
% 0.14/0.42 sQ21_spl <=> (k5_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=k1_rlvect_1(sK1_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f394,plain,(
% 0.14/0.42 k5_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=k1_rlvect_1(sK1_skl)|~sQ21_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f393])).
% 0.14/0.42 fof(f396,plain,(
% 0.14/0.42 sQ20_spl|sQ21_spl|~sQ17_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f381,f390,f393,f353])).
% 0.14/0.42 fof(f397,plain,(
% 0.14/0.42 $false|~sQ20_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f391,f100])).
% 0.14/0.42 fof(f398,plain,(
% 0.14/0.42 ~sQ20_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f397])).
% 0.14/0.42 fof(f399,plain,(
% 0.14/0.42 $false|sQ16_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f352,f94])).
% 0.14/0.42 fof(f400,plain,(
% 0.14/0.42 sQ16_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f399])).
% 0.14/0.42 fof(f401,plain,(
% 0.14/0.42 $false|sQ15_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f349,f93])).
% 0.14/0.42 fof(f402,plain,(
% 0.14/0.42 sQ15_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f401])).
% 0.14/0.42 fof(f403,plain,(
% 0.14/0.42 $false|sQ14_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f346,f92])).
% 0.14/0.42 fof(f404,plain,(
% 0.14/0.42 sQ14_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f403])).
% 0.14/0.42 fof(f405,plain,(
% 0.14/0.42 $false|sQ13_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f343,f91])).
% 0.14/0.42 fof(f406,plain,(
% 0.14/0.42 sQ13_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f405])).
% 0.14/0.42 fof(f407,plain,(
% 0.14/0.42 $false|sQ12_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f340,f90])).
% 0.14/0.42 fof(f408,plain,(
% 0.14/0.42 sQ12_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f407])).
% 0.14/0.42 fof(f409,plain,(
% 0.14/0.42 $false|~sQ11_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f336,f89])).
% 0.14/0.42 fof(f410,plain,(
% 0.14/0.42 ~sQ11_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f409])).
% 0.14/0.42 fof(f411,plain,(
% 0.14/0.42 ![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)|~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)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~m2_rmod_4(sK4_skl(sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,X0)|k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=k1_xboole_0|~sQ21_spl)),
% 0.14/0.42 inference(resolution,[status(thm)],[f394,f109])).
% 0.14/0.42 fof(f413,definition,(
% 0.14/0.42 sQ22_spl <=> (l1_vectsp_2(sK1_skl,sK0_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f415,plain,(
% 0.14/0.42 ~l1_vectsp_2(sK1_skl,sK0_skl)|sQ22_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f413])).
% 0.14/0.42 fof(f416,definition,(
% 0.14/0.42 ![X0]: (sQ23_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~m2_rmod_4(sK4_skl(sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,X0)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f417,plain,(
% 0.14/0.42 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~m2_rmod_4(sK4_skl(sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,X0)|~sQ23_spl)),
% 0.14/0.42 inference(component_clause,[status(thm)],[f416])).
% 0.14/0.42 fof(f419,definition,(
% 0.14/0.42 sQ24_spl <=> (k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=k1_xboole_0)),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f420,plain,(
% 0.14/0.42 k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=k1_xboole_0|~sQ24_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f419])).
% 0.14/0.42 fof(f422,plain,(
% 0.14/0.42 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ10_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ22_spl|sQ23_spl|sQ24_spl|~sQ21_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f411,f296,f299,f302,f305,f308,f311,f327,f314,f317,f320,f335,f338,f341,f344,f347,f350,f413,f416,f419,f393])).
% 0.14/0.42 fof(f439,plain,(
% 0.14/0.42 ![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_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_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_rmod_5(X1,sK0_skl,X0)|~k2_rmod_4(sK0_skl,X0,sK4_skl(X1,X0,sK0_skl))=k1_xboole_0)),
% 0.14/0.42 inference(resolution,[status(thm)],[f112,f85])).
% 0.14/0.42 fof(f442,definition,(
% 0.14/0.42 ![X0,X1]: (sQ27_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)))|v1_rmod_5(X1,sK0_skl,X0)|~k2_rmod_4(sK0_skl,X0,sK4_skl(X1,X0,sK0_skl))=k1_xboole_0))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f443,plain,(
% 0.14/0.42 ![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)))|v1_rmod_5(X1,sK0_skl,X0)|~k2_rmod_4(sK0_skl,X0,sK4_skl(X1,X0,sK0_skl))=k1_xboole_0|~sQ27_spl)),
% 0.14/0.42 inference(component_clause,[status(thm)],[f442])).
% 0.14/0.42 fof(f445,plain,(
% 0.14/0.42 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ27_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f439,f296,f299,f302,f305,f308,f311,f314,f317,f320,f442])).
% 0.14/0.42 fof(f448,plain,(
% 0.14/0.42 ![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)|~v5_vectsp_2(sK1_skl,sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|~k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(X0,sK1_skl,sK0_skl))=k1_xboole_0|~sQ27_spl)),
% 0.14/0.42 inference(resolution,[status(thm)],[f443,f95])).
% 0.14/0.42 fof(f449,definition,(
% 0.14/0.42 ![X0]: (sQ28_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|~k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(X0,sK1_skl,sK0_skl))=k1_xboole_0))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f450,plain,(
% 0.14/0.42 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|~k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(X0,sK1_skl,sK0_skl))=k1_xboole_0|~sQ28_spl)),
% 0.14/0.42 inference(component_clause,[status(thm)],[f449])).
% 0.14/0.42 fof(f452,plain,(
% 0.14/0.42 sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|sQ28_spl|~sQ27_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f448,f335,f338,f341,f344,f347,f350,f449,f442])).
% 0.14/0.42 fof(f454,plain,(
% 0.14/0.42 sK22_skl=k1_xboole_0),
% 0.14/0.42 inference(resolution,[status(thm)],[f273,f210])).
% 0.14/0.42 fof(f458,plain,(
% 0.14/0.42 k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=sK22_skl|~sQ24_spl),
% 0.14/0.42 inference(backward_demodulation,[status(thm)],[f454,f420])).
% 0.14/0.42 fof(f472,plain,(
% 0.14/0.42 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|~k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(X0,sK1_skl,sK0_skl))=sK22_skl|~sQ28_spl)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f454,f450])).
% 0.14/0.42 fof(f474,plain,(
% 0.14/0.42 v1_rmod_5(sK2_skl,sK0_skl,sK1_skl)|~k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=sK22_skl|~sQ28_spl),
% 0.14/0.42 inference(resolution,[status(thm)],[f472,f96])).
% 0.14/0.42 fof(f480,definition,(
% 0.14/0.42 sQ30_spl <=> (k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=sK22_skl)),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f482,plain,(
% 0.14/0.42 ~k2_rmod_4(sK0_skl,sK1_skl,sK4_skl(sK2_skl,sK1_skl,sK0_skl))=sK22_skl|sQ30_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f480])).
% 0.14/0.42 fof(f483,plain,(
% 0.14/0.42 sQ20_spl|~sQ30_spl|~sQ28_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f474,f390,f480,f449])).
% 0.14/0.42 fof(f484,plain,(
% 0.14/0.42 ~sK22_skl=sK22_skl|~sQ24_spl|sQ30_spl),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f458,f482])).
% 0.14/0.42 fof(f485,plain,(
% 0.14/0.42 $false|~sQ24_spl|sQ30_spl),
% 0.14/0.42 inference(trivial_equality_resolution,[status(thm)],[f484])).
% 0.14/0.42 fof(f486,plain,(
% 0.14/0.42 ~sQ24_spl|sQ30_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f485])).
% 0.14/0.42 fof(f487,plain,(
% 0.14/0.42 $false|sQ22_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f415,f95])).
% 0.14/0.42 fof(f488,plain,(
% 0.14/0.42 sQ22_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f487])).
% 0.14/0.42 fof(f491,plain,(
% 0.14/0.42 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|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)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m2_rmod_4(sK4_skl(sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,X1)|~r1_tarski(X1,X0)|~sQ23_spl)),
% 0.14/0.42 inference(resolution,[status(thm)],[f417,f254])).
% 0.14/0.42 fof(f492,definition,(
% 0.14/0.42 sQ31_spl <=> (m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f494,plain,(
% 0.14/0.42 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ31_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f492])).
% 0.14/0.42 fof(f496,definition,(
% 0.14/0.42 ![X0,X1]: (sQ32_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m2_rmod_4(sK4_skl(sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,X1)|~r1_tarski(X1,X0)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f497,plain,(
% 0.14/0.42 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m2_rmod_4(sK4_skl(sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,X1)|~r1_tarski(X1,X0)|~sQ32_spl)),
% 0.14/0.42 inference(component_clause,[status(thm)],[f496])).
% 0.14/0.42 fof(f499,plain,(
% 0.14/0.42 sQ32_spl|sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ10_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ22_spl|~sQ23_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f491,f496,f296,f299,f302,f305,f308,f311,f327,f314,f317,f320,f335,f338,f341,f344,f347,f350,f413,f416])).
% 0.14/0.42 fof(f500,plain,(
% 0.14/0.42 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m2_rmod_4(sK4_skl(sK2_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,X1)|~r1_tarski(X1,X0)|~sQ32_spl)),
% 0.14/0.42 inference(duplicate_literals_removal,[status(thm)],[f497])).
% 0.14/0.42 fof(f508,plain,(
% 0.14/0.42 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(sK2_skl,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)|~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)|~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(sK2_skl,sK0_skl,sK1_skl)|~sQ32_spl)),
% 0.14/0.42 inference(resolution,[status(thm)],[f500,f110])).
% 0.14/0.42 fof(f510,definition,(
% 0.14/0.42 ![X0]: (sQ34_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~r1_tarski(sK2_skl,X0)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f511,plain,(
% 0.14/0.42 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_rmod_5(X0,sK0_skl,sK1_skl)|~r1_tarski(sK2_skl,X0)|~sQ34_spl)),
% 0.14/0.42 inference(component_clause,[status(thm)],[f510])).
% 0.14/0.42 fof(f513,plain,(
% 0.14/0.42 sQ34_spl|~sQ31_spl|sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ10_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ22_spl|sQ20_spl|~sQ32_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f508,f510,f492,f296,f299,f302,f305,f308,f311,f327,f314,f317,f320,f335,f338,f341,f344,f347,f350,f413,f390,f496])).
% 0.14/0.42 fof(f519,plain,(
% 0.14/0.42 ~v1_rmod_5(sK3_skl,sK0_skl,sK1_skl)|~r1_tarski(sK2_skl,sK3_skl)|~sQ34_spl),
% 0.14/0.42 inference(resolution,[status(thm)],[f511,f97])).
% 0.14/0.42 fof(f522,definition,(
% 0.14/0.42 sQ36_spl <=> (r1_tarski(sK2_skl,sK3_skl))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f524,plain,(
% 0.14/0.42 ~r1_tarski(sK2_skl,sK3_skl)|sQ36_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f522])).
% 0.14/0.42 fof(f525,plain,(
% 0.14/0.42 ~sQ18_spl|~sQ36_spl|~sQ34_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f519,f383,f522,f510])).
% 0.14/0.42 fof(f530,plain,(
% 0.14/0.42 $false|sQ31_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f494,f96])).
% 0.14/0.42 fof(f531,plain,(
% 0.14/0.42 sQ31_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f530])).
% 0.14/0.42 fof(f532,plain,(
% 0.14/0.42 $false|sQ18_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f385,f99])).
% 0.14/0.42 fof(f533,plain,(
% 0.14/0.42 sQ18_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f532])).
% 0.14/0.42 fof(f534,plain,(
% 0.14/0.42 $false|sQ36_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f524,f98])).
% 0.14/0.42 fof(f535,plain,(
% 0.14/0.42 sQ36_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f534])).
% 0.14/0.42 fof(f536,plain,(
% 0.14/0.42 $false),
% 0.14/0.42 inference(sat_refutation,[status(thm)],[f326,f356,f358,f360,f362,f364,f366,f368,f370,f372,f374,f376,f396,f398,f400,f402,f404,f406,f408,f410,f422,f445,f452,f483,f486,f488,f499,f513,f525,f531,f533,f535])).
% 0.14/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.45 % Elapsed time: 0.071664 seconds
% 0.14/0.45 % CPU time: 0.232005 seconds
% 0.14/0.45 % Total memory used: 82.909 MB
% 0.14/0.45 % Net memory used: 82.655 MB
%------------------------------------------------------------------------------