%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG215+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 : n006.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.15s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG215+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n006.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 13:02:41 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.45 % Drodi V4.1.1
% 0.15/0.59 % Refutation found
% 0.15/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.59 fof(f1,conjecture,(
% 0.15/0.59 (! [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) )=> v1_rmod_5(k1_subset_1(u1_struct_0(B)),A,B) ) )) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f2,negated_conjecture,(
% 0.15/0.59 ~((! [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) )=> v1_rmod_5(k1_subset_1(u1_struct_0(B)),A,B) ) )) ))),
% 0.15/0.59 inference(negated_conjecture,[status(cth)],[f1])).
% 0.15/0.59 fof(f5,axiom,(
% 0.15/0.59 (! [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.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f7,axiom,(
% 0.15/0.59 (! [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_rmod_4(D,A,B)=> ( m2_rmod_4(D,A,B,C)<=> r1_tarski(k2_rmod_4(A,B,D),C) ) ) )) )) )) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f12,axiom,(
% 0.15/0.59 (! [A] :( v1_xboole_0(k1_subset_1(A))& m1_subset_1(k1_subset_1(A),k1_zfmisc_1(A)) ) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f33,axiom,(
% 0.15/0.59 (! [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)& 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)& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )=> (! [D] :( m2_rmod_4(D,A,B,C)=> m1_rmod_4(D,A,B) ) )) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f56,axiom,(
% 0.15/0.59 (? [A] : v1_xboole_0(A) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f73,axiom,(
% 0.15/0.59 (! [A] :( r1_tarski(A,k1_xboole_0)=> A = k1_xboole_0 ) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f76,axiom,(
% 0.15/0.59 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f79,plain,(
% 0.15/0.59 (?[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))&~v1_rmod_5(k1_subset_1(u1_struct_0(B)),A,B)))))),
% 0.15/0.59 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.15/0.59 fof(f80,plain,(
% 0.15/0.59 ((((((((((~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))&~v1_rmod_5(k1_subset_1(u1_struct_0(sK1_skl)),sK0_skl,sK1_skl)))),
% 0.15/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f79])).
% 0.15/0.59 fof(f81,plain,(
% 0.15/0.59 ~v3_struct_0(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f82,plain,(
% 0.15/0.59 v3_rlvect_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f83,plain,(
% 0.15/0.59 v4_rlvect_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f84,plain,(
% 0.15/0.59 v5_rlvect_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f85,plain,(
% 0.15/0.59 v6_rlvect_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f86,plain,(
% 0.15/0.59 v4_group_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f87,plain,(
% 0.15/0.59 v6_vectsp_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f88,plain,(
% 0.15/0.59 v7_vectsp_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f89,plain,(
% 0.15/0.59 v8_vectsp_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f90,plain,(
% 0.15/0.59 l3_vectsp_1(sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f91,plain,(
% 0.15/0.59 ~v3_struct_0(sK1_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f92,plain,(
% 0.15/0.59 v3_rlvect_1(sK1_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f93,plain,(
% 0.15/0.59 v4_rlvect_1(sK1_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f94,plain,(
% 0.15/0.59 v5_rlvect_1(sK1_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f95,plain,(
% 0.15/0.59 v6_rlvect_1(sK1_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f96,plain,(
% 0.15/0.59 v5_vectsp_2(sK1_skl,sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f97,plain,(
% 0.15/0.59 l1_vectsp_2(sK1_skl,sK0_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f98,plain,(
% 0.15/0.59 ~v1_rmod_5(k1_subset_1(u1_struct_0(sK1_skl)),sK0_skl,sK1_skl)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f80])).
% 0.15/0.59 fof(f104,plain,(
% 0.15/0.59 ![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.15/0.59 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.15/0.59 fof(f105,plain,(
% 0.15/0.59 ![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.15/0.59 inference(NNF_transformation,[status(thm)],[f104])).
% 0.15/0.59 fof(f106,plain,(
% 0.15/0.59 ![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(sK2_skl(C,B,A),A,B,C)&(k5_rmod_4(A,B,sK2_skl(C,B,A))=k1_rlvect_1(B)&~k2_rmod_4(A,B,sK2_skl(C,B,A))=k1_xboole_0)))))))))),
% 0.15/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(D,sK2_skl(C,B,A))],[f105])).
% 0.15/0.59 fof(f108,plain,(
% 0.15/0.59 ![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(sK2_skl(X2,X1,X0),X0,X1,X2))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f106])).
% 0.15/0.59 fof(f110,plain,(
% 0.15/0.59 ![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,sK2_skl(X2,X1,X0))=k1_xboole_0)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f106])).
% 0.15/0.59 fof(f113,plain,(
% 0.15/0.59 ![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_rmod_4(D,A,B)|(m2_rmod_4(D,A,B,C)<=>r1_tarski(k2_rmod_4(A,B,D),C)))))))))),
% 0.15/0.59 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.15/0.59 fof(f114,plain,(
% 0.15/0.59 ![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_rmod_4(D,A,B)|((~m2_rmod_4(D,A,B,C)|r1_tarski(k2_rmod_4(A,B,D),C))&(m2_rmod_4(D,A,B,C)|~r1_tarski(k2_rmod_4(A,B,D),C))))))))))),
% 0.15/0.59 inference(NNF_transformation,[status(thm)],[f113])).
% 0.15/0.59 fof(f115,plain,(
% 0.15/0.59 ![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)))|~m1_rmod_4(X3,X0,X1)|~m2_rmod_4(X3,X0,X1,X2)|r1_tarski(k2_rmod_4(X0,X1,X3),X2))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f114])).
% 0.15/0.59 fof(f122,plain,(
% 0.15/0.59 (![A]: v1_xboole_0(k1_subset_1(A)))&(![A]: m1_subset_1(k1_subset_1(A),k1_zfmisc_1(A)))),
% 0.15/0.59 inference(miniscoping,[status(thm)],[f12])).
% 0.15/0.59 fof(f123,plain,(
% 0.15/0.59 ![X0]: (v1_xboole_0(k1_subset_1(X0)))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f122])).
% 0.15/0.59 fof(f124,plain,(
% 0.15/0.59 ![X0]: (m1_subset_1(k1_subset_1(X0),k1_zfmisc_1(X0)))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f122])).
% 0.15/0.59 fof(f160,plain,(
% 0.15/0.59 ![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))|~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))|~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))))|(![D]: (~m2_rmod_4(D,A,B,C)|m1_rmod_4(D,A,B))))),
% 0.15/0.60 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.15/0.60 fof(f161,plain,(
% 0.15/0.60 ![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)))|~m2_rmod_4(X3,X0,X1,X2)|m1_rmod_4(X3,X0,X1))),
% 0.15/0.60 inference(cnf_transformation,[status(thm)],[f160])).
% 0.15/0.60 fof(f214,plain,(
% 0.15/0.60 v1_xboole_0(sK20_skl)),
% 0.15/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f56])).
% 0.15/0.60 fof(f215,plain,(
% 0.15/0.60 v1_xboole_0(sK20_skl)),
% 0.15/0.60 inference(cnf_transformation,[status(thm)],[f214])).
% 0.15/0.60 fof(f269,plain,(
% 0.15/0.60 ![A]: (~r1_tarski(A,k1_xboole_0)|A=k1_xboole_0)),
% 0.15/0.60 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 0.15/0.60 fof(f270,plain,(
% 0.15/0.60 ![X0]: (~r1_tarski(X0,k1_xboole_0)|X0=k1_xboole_0)),
% 0.15/0.60 inference(cnf_transformation,[status(thm)],[f269])).
% 0.15/0.60 fof(f277,plain,(
% 0.15/0.60 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 0.15/0.60 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 0.15/0.60 fof(f278,plain,(
% 0.15/0.60 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 0.15/0.60 inference(cnf_transformation,[status(thm)],[f277])).
% 0.15/0.60 fof(f299,plain,(
% 0.15/0.60 ![X0]: (k1_subset_1(X0)=k1_xboole_0)),
% 0.15/0.60 inference(resolution,[status(thm)],[f278,f123])).
% 0.15/0.60 fof(f300,plain,(
% 0.15/0.60 sK20_skl=k1_xboole_0),
% 0.15/0.60 inference(resolution,[status(thm)],[f278,f215])).
% 0.15/0.60 fof(f304,definition,(
% 0.15/0.60 sQ0_spl <=> (v3_struct_0(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f305,plain,(
% 0.15/0.60 v3_struct_0(sK0_skl)|~sQ0_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f304])).
% 0.15/0.60 fof(f307,definition,(
% 0.15/0.60 sQ1_spl <=> (v3_rlvect_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f309,plain,(
% 0.15/0.60 ~v3_rlvect_1(sK0_skl)|sQ1_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f307])).
% 0.15/0.60 fof(f310,definition,(
% 0.15/0.60 sQ2_spl <=> (v4_rlvect_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f312,plain,(
% 0.15/0.60 ~v4_rlvect_1(sK0_skl)|sQ2_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f310])).
% 0.15/0.60 fof(f313,definition,(
% 0.15/0.60 sQ3_spl <=> (v5_rlvect_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f315,plain,(
% 0.15/0.60 ~v5_rlvect_1(sK0_skl)|sQ3_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f313])).
% 0.15/0.60 fof(f316,definition,(
% 0.15/0.60 sQ4_spl <=> (v6_rlvect_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f318,plain,(
% 0.15/0.60 ~v6_rlvect_1(sK0_skl)|sQ4_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f316])).
% 0.15/0.60 fof(f319,definition,(
% 0.15/0.60 sQ5_spl <=> (v4_group_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f321,plain,(
% 0.15/0.60 ~v4_group_1(sK0_skl)|sQ5_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f319])).
% 0.15/0.60 fof(f322,definition,(
% 0.15/0.60 sQ6_spl <=> (v7_vectsp_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f324,plain,(
% 0.15/0.60 ~v7_vectsp_1(sK0_skl)|sQ6_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f322])).
% 0.15/0.60 fof(f325,definition,(
% 0.15/0.60 sQ7_spl <=> (v8_vectsp_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f327,plain,(
% 0.15/0.60 ~v8_vectsp_1(sK0_skl)|sQ7_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f325])).
% 0.15/0.60 fof(f328,definition,(
% 0.15/0.60 sQ8_spl <=> (l3_vectsp_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f330,plain,(
% 0.15/0.60 ~l3_vectsp_1(sK0_skl)|sQ8_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f328])).
% 0.15/0.60 fof(f335,definition,(
% 0.15/0.60 sQ10_spl <=> (v6_vectsp_1(sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f337,plain,(
% 0.15/0.60 ~v6_vectsp_1(sK0_skl)|sQ10_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f335])).
% 0.15/0.60 fof(f341,definition,(
% 0.15/0.60 sQ11_spl <=> (v3_struct_0(sK1_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f342,plain,(
% 0.15/0.60 v3_struct_0(sK1_skl)|~sQ11_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f341])).
% 0.15/0.60 fof(f344,definition,(
% 0.15/0.60 sQ12_spl <=> (v3_rlvect_1(sK1_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f346,plain,(
% 0.15/0.60 ~v3_rlvect_1(sK1_skl)|sQ12_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f344])).
% 0.15/0.60 fof(f347,definition,(
% 0.15/0.60 sQ13_spl <=> (v4_rlvect_1(sK1_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f349,plain,(
% 0.15/0.60 ~v4_rlvect_1(sK1_skl)|sQ13_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f347])).
% 0.15/0.60 fof(f350,definition,(
% 0.15/0.60 sQ14_spl <=> (v5_rlvect_1(sK1_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f352,plain,(
% 0.15/0.60 ~v5_rlvect_1(sK1_skl)|sQ14_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f350])).
% 0.15/0.60 fof(f353,definition,(
% 0.15/0.60 sQ15_spl <=> (v6_rlvect_1(sK1_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f355,plain,(
% 0.15/0.60 ~v6_rlvect_1(sK1_skl)|sQ15_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f353])).
% 0.15/0.60 fof(f356,definition,(
% 0.15/0.60 sQ16_spl <=> (v5_vectsp_2(sK1_skl,sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f358,plain,(
% 0.15/0.60 ~v5_vectsp_2(sK1_skl,sK0_skl)|sQ16_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f356])).
% 0.15/0.60 fof(f363,plain,(
% 0.15/0.60 $false|sQ8_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f330,f90])).
% 0.15/0.60 fof(f364,plain,(
% 0.15/0.60 sQ8_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f363])).
% 0.15/0.60 fof(f365,plain,(
% 0.15/0.60 $false|sQ5_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f321,f86])).
% 0.15/0.60 fof(f366,plain,(
% 0.15/0.60 sQ5_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f365])).
% 0.15/0.60 fof(f367,plain,(
% 0.15/0.60 $false|sQ4_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f318,f85])).
% 0.15/0.60 fof(f368,plain,(
% 0.15/0.60 sQ4_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f367])).
% 0.15/0.60 fof(f369,plain,(
% 0.15/0.60 $false|sQ3_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f315,f84])).
% 0.15/0.60 fof(f370,plain,(
% 0.15/0.60 sQ3_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f369])).
% 0.15/0.60 fof(f371,plain,(
% 0.15/0.60 $false|sQ2_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f312,f83])).
% 0.15/0.60 fof(f372,plain,(
% 0.15/0.60 sQ2_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f371])).
% 0.15/0.60 fof(f373,plain,(
% 0.15/0.60 $false|sQ1_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f309,f82])).
% 0.15/0.60 fof(f374,plain,(
% 0.15/0.60 sQ1_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f373])).
% 0.15/0.60 fof(f375,plain,(
% 0.15/0.60 $false|~sQ0_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f305,f81])).
% 0.15/0.60 fof(f376,plain,(
% 0.15/0.60 ~sQ0_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f375])).
% 0.15/0.60 fof(f377,plain,(
% 0.15/0.60 $false|sQ6_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f324,f88])).
% 0.15/0.60 fof(f378,plain,(
% 0.15/0.60 sQ6_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f377])).
% 0.15/0.60 fof(f379,plain,(
% 0.15/0.60 $false|sQ10_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f337,f87])).
% 0.15/0.60 fof(f380,plain,(
% 0.15/0.60 sQ10_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f379])).
% 0.15/0.60 fof(f381,plain,(
% 0.15/0.60 $false|sQ7_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f327,f89])).
% 0.15/0.60 fof(f382,plain,(
% 0.15/0.60 sQ7_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f381])).
% 0.15/0.60 fof(f401,plain,(
% 0.15/0.60 $false|sQ16_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f358,f96])).
% 0.15/0.60 fof(f402,plain,(
% 0.15/0.60 sQ16_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f401])).
% 0.15/0.60 fof(f403,plain,(
% 0.15/0.60 $false|sQ15_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f355,f95])).
% 0.15/0.60 fof(f404,plain,(
% 0.15/0.60 sQ15_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f403])).
% 0.15/0.60 fof(f405,plain,(
% 0.15/0.60 $false|sQ14_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f352,f94])).
% 0.15/0.60 fof(f406,plain,(
% 0.15/0.60 sQ14_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f405])).
% 0.15/0.60 fof(f407,plain,(
% 0.15/0.60 $false|sQ13_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f349,f93])).
% 0.15/0.60 fof(f408,plain,(
% 0.15/0.60 sQ13_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f407])).
% 0.15/0.60 fof(f409,plain,(
% 0.15/0.60 $false|sQ12_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f346,f92])).
% 0.15/0.60 fof(f410,plain,(
% 0.15/0.60 sQ12_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f409])).
% 0.15/0.60 fof(f411,plain,(
% 0.15/0.60 $false|~sQ11_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f342,f91])).
% 0.15/0.60 fof(f412,plain,(
% 0.15/0.60 ~sQ11_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f411])).
% 0.15/0.60 fof(f420,plain,(
% 0.15/0.60 ~v1_rmod_5(k1_xboole_0,sK0_skl,sK1_skl)),
% 0.15/0.60 inference(backward_demodulation,[status(thm)],[f299,f98])).
% 0.15/0.60 fof(f422,plain,(
% 0.15/0.60 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 0.15/0.60 inference(backward_demodulation,[status(thm)],[f299,f124])).
% 0.15/0.60 fof(f437,definition,(
% 0.15/0.60 sQ24_spl <=> (l1_vectsp_2(sK1_skl,sK0_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f439,plain,(
% 0.15/0.60 ~l1_vectsp_2(sK1_skl,sK0_skl)|sQ24_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f437])).
% 0.15/0.60 fof(f452,plain,(
% 0.15/0.60 ![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,sK2_skl(X1,X0,sK0_skl))=k1_xboole_0)),
% 0.15/0.60 inference(resolution,[status(thm)],[f110,f87])).
% 0.15/0.60 fof(f455,definition,(
% 0.15/0.60 ![X0,X1]: (sQ28_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,sK2_skl(X1,X0,sK0_skl))=k1_xboole_0))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f456,plain,(
% 0.15/0.60 ![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,sK2_skl(X1,X0,sK0_skl))=k1_xboole_0|~sQ28_spl)),
% 0.15/0.60 inference(component_clause,[status(thm)],[f455])).
% 0.15/0.60 fof(f458,plain,(
% 0.15/0.60 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ28_spl),
% 0.15/0.60 inference(split_clause,[status(thm)],[f452,f304,f307,f310,f313,f316,f319,f322,f325,f328,f455])).
% 0.15/0.60 fof(f466,plain,(
% 0.15/0.60 ![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,sK2_skl(X1,X0,sK0_skl))=sK20_skl|~sQ28_spl)),
% 0.15/0.60 inference(backward_demodulation,[status(thm)],[f300,f456])).
% 0.15/0.60 fof(f470,plain,(
% 0.15/0.60 ![X0]: (m1_subset_1(sK20_skl,k1_zfmisc_1(X0)))),
% 0.15/0.60 inference(backward_demodulation,[status(thm)],[f300,f422])).
% 0.15/0.60 fof(f473,plain,(
% 0.15/0.60 ~v1_rmod_5(sK20_skl,sK0_skl,sK1_skl)),
% 0.15/0.60 inference(backward_demodulation,[status(thm)],[f300,f420])).
% 0.15/0.60 fof(f481,definition,(
% 0.15/0.60 sQ30_spl <=> (v1_rmod_5(sK20_skl,sK0_skl,sK1_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f482,plain,(
% 0.15/0.60 v1_rmod_5(sK20_skl,sK0_skl,sK1_skl)|~sQ30_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f481])).
% 0.15/0.60 fof(f488,plain,(
% 0.15/0.60 $false|~sQ30_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f482,f473])).
% 0.15/0.60 fof(f489,plain,(
% 0.15/0.60 ~sQ30_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f488])).
% 0.15/0.60 fof(f496,definition,(
% 0.15/0.60 sQ33_spl <=> (m1_rmod_4(sK2_skl(sK20_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f497,plain,(
% 0.15/0.60 m1_rmod_4(sK2_skl(sK20_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl)|~sQ33_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f496])).
% 0.15/0.60 fof(f500,plain,(
% 0.15/0.60 $false|sQ24_spl),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f439,f97])).
% 0.15/0.60 fof(f501,plain,(
% 0.15/0.60 sQ24_spl),
% 0.15/0.60 inference(contradiction_clause,[status(thm)],[f500])).
% 0.15/0.60 fof(f503,plain,(
% 0.15/0.60 ![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,sK2_skl(X0,sK1_skl,sK0_skl))=sK20_skl|~sQ28_spl)),
% 0.15/0.60 inference(resolution,[status(thm)],[f466,f97])).
% 0.15/0.60 fof(f504,definition,(
% 0.15/0.60 ![X0]: (sQ34_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,sK2_skl(X0,sK1_skl,sK0_skl))=sK20_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f505,plain,(
% 0.15/0.60 ![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,sK2_skl(X0,sK1_skl,sK0_skl))=sK20_skl|~sQ34_spl)),
% 0.15/0.60 inference(component_clause,[status(thm)],[f504])).
% 0.15/0.60 fof(f507,plain,(
% 0.15/0.60 sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|sQ34_spl|~sQ28_spl),
% 0.15/0.60 inference(split_clause,[status(thm)],[f503,f341,f344,f347,f350,f353,f356,f504,f455])).
% 0.15/0.60 fof(f508,plain,(
% 0.15/0.60 v1_rmod_5(sK20_skl,sK0_skl,sK1_skl)|~k2_rmod_4(sK0_skl,sK1_skl,sK2_skl(sK20_skl,sK1_skl,sK0_skl))=sK20_skl|~sQ34_spl),
% 0.15/0.60 inference(resolution,[status(thm)],[f505,f470])).
% 0.15/0.60 fof(f510,definition,(
% 0.15/0.60 sQ35_spl <=> (k2_rmod_4(sK0_skl,sK1_skl,sK2_skl(sK20_skl,sK1_skl,sK0_skl))=sK20_skl)),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f513,plain,(
% 0.15/0.60 sQ30_spl|~sQ35_spl|~sQ34_spl),
% 0.15/0.60 inference(split_clause,[status(thm)],[f508,f481,f510,f504])).
% 0.15/0.60 fof(f520,definition,(
% 0.15/0.60 sQ37_spl <=> (m1_subset_1(sK20_skl,k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f522,plain,(
% 0.15/0.60 ~m1_subset_1(sK20_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ37_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f520])).
% 0.15/0.60 fof(f562,plain,(
% 0.15/0.60 ![X0]: (~r1_tarski(X0,sK20_skl)|X0=k1_xboole_0)),
% 0.15/0.60 inference(forward_demodulation,[status(thm)],[f300,f270])).
% 0.15/0.60 fof(f563,plain,(
% 0.15/0.60 ![X0]: (~r1_tarski(X0,sK20_skl)|X0=sK20_skl)),
% 0.15/0.60 inference(forward_demodulation,[status(thm)],[f300,f562])).
% 0.15/0.60 fof(f565,plain,(
% 0.15/0.60 ![X0,X1,X2]: (k2_rmod_4(X0,X1,X2)=sK20_skl|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(sK20_skl,k1_zfmisc_1(u1_struct_0(X1)))|~m1_rmod_4(X2,X0,X1)|~m2_rmod_4(X2,X0,X1,sK20_skl))),
% 0.15/0.60 inference(resolution,[status(thm)],[f563,f115])).
% 0.15/0.60 fof(f568,plain,(
% 0.15/0.60 ![X0,X1,X2]: (k2_rmod_4(X0,X1,X2)=sK20_skl|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_4(X2,X0,X1)|~m2_rmod_4(X2,X0,X1,sK20_skl))),
% 0.15/0.60 inference(forward_subsumption_resolution,[status(thm)],[f565,f470])).
% 0.15/0.60 fof(f720,plain,(
% 0.15/0.60 ![X0,X1,X2]: (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)))|~m2_rmod_4(X2,sK0_skl,X0,X1)|m1_rmod_4(X2,sK0_skl,X0))),
% 0.15/0.60 inference(resolution,[status(thm)],[f161,f87])).
% 0.15/0.60 fof(f723,definition,(
% 0.15/0.60 ![X0,X1,X2]: (sQ68_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)))|~m2_rmod_4(X2,sK0_skl,X0,X1)|m1_rmod_4(X2,sK0_skl,X0)))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f724,plain,(
% 0.15/0.60 ![X0,X1,X2]: (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)))|~m2_rmod_4(X2,sK0_skl,X0,X1)|m1_rmod_4(X2,sK0_skl,X0)|~sQ68_spl)),
% 0.15/0.60 inference(component_clause,[status(thm)],[f723])).
% 0.15/0.60 fof(f726,plain,(
% 0.15/0.60 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ68_spl),
% 0.15/0.60 inference(split_clause,[status(thm)],[f720,f304,f307,f310,f313,f316,f319,f322,f325,f328,f723])).
% 0.15/0.60 fof(f753,plain,(
% 0.15/0.60 ![X0,X1]: (v3_struct_0(sK1_skl)|~v3_rlvect_1(sK1_skl)|~v4_rlvect_1(sK1_skl)|~v5_rlvect_1(sK1_skl)|~v6_rlvect_1(sK1_skl)|~l1_vectsp_2(sK1_skl,sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m2_rmod_4(X1,sK0_skl,sK1_skl,X0)|m1_rmod_4(X1,sK0_skl,sK1_skl)|~sQ68_spl)),
% 0.15/0.60 inference(resolution,[status(thm)],[f724,f96])).
% 0.15/0.60 fof(f754,definition,(
% 0.15/0.60 ![X0,X1]: (sQ75_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m2_rmod_4(X1,sK0_skl,sK1_skl,X0)|m1_rmod_4(X1,sK0_skl,sK1_skl)))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f755,plain,(
% 0.15/0.60 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~m2_rmod_4(X1,sK0_skl,sK1_skl,X0)|m1_rmod_4(X1,sK0_skl,sK1_skl)|~sQ75_spl)),
% 0.15/0.60 inference(component_clause,[status(thm)],[f754])).
% 0.15/0.60 fof(f757,plain,(
% 0.15/0.60 sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ24_spl|sQ75_spl|~sQ68_spl),
% 0.15/0.60 inference(split_clause,[status(thm)],[f753,f341,f344,f347,f350,f353,f437,f754,f723])).
% 0.15/0.60 fof(f758,plain,(
% 0.15/0.60 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|m1_rmod_4(sK2_skl(X0,sK1_skl,sK0_skl),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(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|~sQ75_spl)),
% 0.15/0.60 inference(resolution,[status(thm)],[f755,f108])).
% 0.15/0.60 fof(f759,definition,(
% 0.15/0.60 ![X0]: (sQ76_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|m1_rmod_4(sK2_skl(X0,sK1_skl,sK0_skl),sK0_skl,sK1_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f760,plain,(
% 0.15/0.60 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|m1_rmod_4(sK2_skl(X0,sK1_skl,sK0_skl),sK0_skl,sK1_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(X0,sK0_skl,sK1_skl)|~sQ76_spl)),
% 0.15/0.60 inference(component_clause,[status(thm)],[f759])).
% 0.15/0.60 fof(f762,plain,(
% 0.15/0.60 sQ76_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|~sQ24_spl|~sQ75_spl),
% 0.15/0.60 inference(split_clause,[status(thm)],[f758,f759,f304,f307,f310,f313,f316,f319,f335,f322,f325,f328,f341,f344,f347,f350,f353,f356,f437,f754])).
% 0.15/0.60 fof(f763,plain,(
% 0.15/0.60 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|m1_rmod_4(sK2_skl(X0,sK1_skl,sK0_skl),sK0_skl,sK1_skl)|v1_rmod_5(X0,sK0_skl,sK1_skl)|~sQ76_spl)),
% 0.15/0.60 inference(duplicate_literals_removal,[status(thm)],[f760])).
% 0.15/0.60 fof(f764,plain,(
% 0.15/0.60 m1_rmod_4(sK2_skl(sK20_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl)|v1_rmod_5(sK20_skl,sK0_skl,sK1_skl)|~sQ76_spl),
% 0.15/0.60 inference(resolution,[status(thm)],[f763,f470])).
% 0.15/0.60 fof(f767,plain,(
% 0.15/0.60 sQ33_spl|sQ30_spl|~sQ76_spl),
% 0.15/0.60 inference(split_clause,[status(thm)],[f764,f496,f481,f759])).
% 0.15/0.60 fof(f776,plain,(
% 0.15/0.60 k2_rmod_4(sK0_skl,sK1_skl,sK2_skl(sK20_skl,sK1_skl,sK0_skl))=sK20_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)|~m2_rmod_4(sK2_skl(sK20_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,sK20_skl)|~sQ33_spl),
% 0.15/0.60 inference(resolution,[status(thm)],[f497,f568])).
% 0.15/0.60 fof(f781,definition,(
% 0.15/0.60 sQ79_spl <=> (m2_rmod_4(sK2_skl(sK20_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,sK20_skl))),
% 0.15/0.60 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.15/0.60 fof(f783,plain,(
% 0.15/0.60 ~m2_rmod_4(sK2_skl(sK20_skl,sK1_skl,sK0_skl),sK0_skl,sK1_skl,sK20_skl)|sQ79_spl),
% 0.15/0.60 inference(component_clause,[status(thm)],[f781])).
% 0.15/0.60 fof(f784,plain,(
% 0.15/0.60 sQ35_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|~sQ24_spl|~sQ79_spl|~sQ33_spl),
% 0.15/0.60 inference(split_clause,[status(thm)],[f776,f510,f304,f307,f310,f313,f316,f319,f335,f322,f325,f328,f341,f344,f347,f350,f353,f356,f437,f781,f496])).
% 0.40/0.61 fof(f904,plain,(
% 0.40/0.61 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(sK20_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_rmod_5(sK20_skl,sK0_skl,sK1_skl)|sQ79_spl),
% 0.40/0.61 inference(resolution,[status(thm)],[f783,f108])).
% 0.40/0.61 fof(f905,plain,(
% 0.40/0.61 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|~sQ24_spl|~sQ37_spl|sQ30_spl|sQ79_spl),
% 0.40/0.61 inference(split_clause,[status(thm)],[f904,f304,f307,f310,f313,f316,f319,f335,f322,f325,f328,f341,f344,f347,f350,f353,f356,f437,f520,f481,f781])).
% 0.40/0.61 fof(f906,plain,(
% 0.40/0.61 $false|sQ37_spl),
% 0.40/0.61 inference(forward_subsumption_resolution,[status(thm)],[f522,f470])).
% 0.40/0.61 fof(f907,plain,(
% 0.40/0.61 sQ37_spl),
% 0.40/0.61 inference(contradiction_clause,[status(thm)],[f906])).
% 0.40/0.61 fof(f908,plain,(
% 0.40/0.61 $false),
% 0.40/0.61 inference(sat_refutation,[status(thm)],[f364,f366,f368,f370,f372,f374,f376,f378,f380,f382,f402,f404,f406,f408,f410,f412,f458,f489,f501,f507,f513,f726,f757,f762,f767,f784,f905,f907])).
% 0.40/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.40/0.62 % Elapsed time: 0.182403 seconds
% 0.40/0.62 % CPU time: 1.094381 seconds
% 0.40/0.62 % Total memory used: 102.396 MB
% 0.40/0.62 % Net memory used: 101.690 MB
%------------------------------------------------------------------------------