%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP640+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 12:37:00 PM UTC 2026
% Result : Theorem 0.25s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP640+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n013.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sun Sep 20 20:23:52 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.46 % Drodi V4.1.1
% 0.25/0.62 % Refutation found
% 0.25/0.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.25/0.62 % SZS output start CNFRefutation for theBenchmark
% 0.25/0.62 fof(f1,conjecture,(
% 0.25/0.62 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B) )=> (! [C] :( m1_group_2(C,A)=> (! [D] :( m1_group_2(D,A)=> (! [E] :( ( v1_funct_1(E)& v1_funct_2(E,u1_struct_0(A),u1_struct_0(B))& m2_relset_1(E,u1_struct_0(A),u1_struct_0(B)) )=> (! [F] :( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A)))=> ( F = k2_xboole_0(u1_struct_0(C),u1_struct_0(D))=> k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k8_group_4(A,C,D))) = k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k5_group_4(A,F))) ) ) )) )) )) )) )) )),
% 0.25/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.62 fof(f2,negated_conjecture,(
% 0.25/0.62 ~((! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B) )=> (! [C] :( m1_group_2(C,A)=> (! [D] :( m1_group_2(D,A)=> (! [E] :( ( v1_funct_1(E)& v1_funct_2(E,u1_struct_0(A),u1_struct_0(B))& m2_relset_1(E,u1_struct_0(A),u1_struct_0(B)) )=> (! [F] :( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A)))=> ( F = k2_xboole_0(u1_struct_0(C),u1_struct_0(D))=> k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k8_group_4(A,C,D))) = k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k5_group_4(A,F))) ) ) )) )) )) )) )) ))),
% 0.25/0.62 inference(negated_conjecture,[status(cth)],[f1])).
% 0.25/0.62 fof(f49,axiom,(
% 0.25/0.62 (! [A,B,C,D] :( ( v1_funct_1(C)& v1_funct_2(C,A,B)& m1_relset_1(C,A,B) )=> k2_funct_2(A,B,C,D) = k9_relat_1(C,D) ) )),
% 0.25/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.62 fof(f50,axiom,(
% 0.25/0.62 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 0.25/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.62 fof(f51,axiom,(
% 0.25/0.62 (! [A,B,C] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A)& v1_group_1(B)& m1_group_2(B,A)& v1_group_1(C)& m1_group_2(C,A) )=> ( r1_group_2(A,B,C)<=> B = C ) ) )),
% 0.25/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.62 fof(f55,axiom,(
% 0.25/0.62 (! [A,B] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> ( v1_group_1(k5_group_4(A,B))& m1_group_2(k5_group_4(A,B),A) ) ) )),
% 0.25/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.62 fof(f56,axiom,(
% 0.25/0.62 (! [A,B,C] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A)& m1_group_2(B,A)& m1_group_2(C,A) )=> ( v1_group_1(k8_group_4(A,B,C))& m1_group_2(k8_group_4(A,B,C),A) ) ) )),
% 0.25/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.62 fof(f64,axiom,(
% 0.25/0.62 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_group_2(B,A)=> (! [C] :( m1_group_2(C,A)=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))=> ( D = k2_xboole_0(u1_struct_0(B),u1_struct_0(C))=> r1_group_2(A,k8_group_4(A,B,C),k5_group_4(A,D)) ) ) )) )) )) )),
% 0.25/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.62 fof(f65,plain,(
% 0.25/0.62 (?[A]: ((((~v3_struct_0(A)&v3_group_1(A))&v4_group_1(A))&l1_group_1(A))&(?[B]: ((((~v3_struct_0(B)&v3_group_1(B))&v4_group_1(B))&l1_group_1(B))&(?[C]: (m1_group_2(C,A)&(?[D]: (m1_group_2(D,A)&(?[E]: (((v1_funct_1(E)&v1_funct_2(E,u1_struct_0(A),u1_struct_0(B)))&m2_relset_1(E,u1_struct_0(A),u1_struct_0(B)))&(?[F]: (m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A)))&(F=k2_xboole_0(u1_struct_0(C),u1_struct_0(D))&~k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k8_group_4(A,C,D)))=k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k5_group_4(A,F))))))))))))))))),
% 0.25/0.62 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.25/0.62 fof(f66,plain,(
% 0.25/0.62 ((((~v3_struct_0(sK0_skl)&v3_group_1(sK0_skl))&v4_group_1(sK0_skl))&l1_group_1(sK0_skl))&((((~v3_struct_0(sK1_skl)&v3_group_1(sK1_skl))&v4_group_1(sK1_skl))&l1_group_1(sK1_skl))&(m1_group_2(sK2_skl,sK0_skl)&(m1_group_2(sK3_skl,sK0_skl)&(((v1_funct_1(sK4_skl)&v1_funct_2(sK4_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))&m2_relset_1(sK4_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))&(m1_subset_1(sK5_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))&(sK5_skl=k2_xboole_0(u1_struct_0(sK2_skl),u1_struct_0(sK3_skl))&~k2_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK4_skl,u1_struct_0(k8_group_4(sK0_skl,sK2_skl,sK3_skl)))=k2_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK4_skl,u1_struct_0(k5_group_4(sK0_skl,sK5_skl))))))))))),
% 0.25/0.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl),skolemize(E,sK4_skl),skolemize(F,sK5_skl)],[f65])).
% 0.25/0.62 fof(f67,plain,(
% 0.25/0.62 ~v3_struct_0(sK0_skl)),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f68,plain,(
% 0.25/0.62 v3_group_1(sK0_skl)),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f69,plain,(
% 0.25/0.62 v4_group_1(sK0_skl)),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f70,plain,(
% 0.25/0.62 l1_group_1(sK0_skl)),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f75,plain,(
% 0.25/0.62 m1_group_2(sK2_skl,sK0_skl)),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f76,plain,(
% 0.25/0.62 m1_group_2(sK3_skl,sK0_skl)),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f77,plain,(
% 0.25/0.62 v1_funct_1(sK4_skl)),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f78,plain,(
% 0.25/0.62 v1_funct_2(sK4_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f79,plain,(
% 0.25/0.62 m2_relset_1(sK4_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f80,plain,(
% 0.25/0.62 m1_subset_1(sK5_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f81,plain,(
% 0.25/0.62 sK5_skl=k2_xboole_0(u1_struct_0(sK2_skl),u1_struct_0(sK3_skl))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f82,plain,(
% 0.25/0.62 ~k2_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK4_skl,u1_struct_0(k8_group_4(sK0_skl,sK2_skl,sK3_skl)))=k2_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK4_skl,u1_struct_0(k5_group_4(sK0_skl,sK5_skl)))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f66])).
% 0.25/0.62 fof(f193,plain,(
% 0.25/0.62 ![A,B,C,D]: (((~v1_funct_1(C)|~v1_funct_2(C,A,B))|~m1_relset_1(C,A,B))|k2_funct_2(A,B,C,D)=k9_relat_1(C,D))),
% 0.25/0.62 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.25/0.62 fof(f194,plain,(
% 0.25/0.62 ![A,B,C]: (((~v1_funct_1(C)|~v1_funct_2(C,A,B))|~m1_relset_1(C,A,B))|(![D]: k2_funct_2(A,B,C,D)=k9_relat_1(C,D)))),
% 0.25/0.62 inference(miniscoping,[status(thm)],[f193])).
% 0.25/0.62 fof(f195,plain,(
% 0.25/0.62 ![X0,X1,X2,X3]: (~v1_funct_1(X0)|~v1_funct_2(X0,X1,X2)|~m1_relset_1(X0,X1,X2)|k2_funct_2(X1,X2,X0,X3)=k9_relat_1(X0,X3))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f194])).
% 0.25/0.62 fof(f196,plain,(
% 0.25/0.62 ![A,B,C]: ((~m2_relset_1(C,A,B)|m1_relset_1(C,A,B))&(m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 0.25/0.62 inference(NNF_transformation,[status(thm)],[f50])).
% 0.25/0.62 fof(f197,plain,(
% 0.25/0.62 (![A,B,C]: (~m2_relset_1(C,A,B)|m1_relset_1(C,A,B)))&(![A,B,C]: (m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 0.25/0.62 inference(miniscoping,[status(thm)],[f196])).
% 0.25/0.62 fof(f198,plain,(
% 0.25/0.62 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f197])).
% 0.25/0.62 fof(f200,plain,(
% 0.25/0.62 ![A,B,C]: ((((((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|~v1_group_1(B))|~m1_group_2(B,A))|~v1_group_1(C))|~m1_group_2(C,A))|(r1_group_2(A,B,C)<=>B=C))),
% 0.25/0.62 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.25/0.62 fof(f201,plain,(
% 0.25/0.62 ![A,B,C]: ((((((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|~v1_group_1(B))|~m1_group_2(B,A))|~v1_group_1(C))|~m1_group_2(C,A))|((~r1_group_2(A,B,C)|B=C)&(r1_group_2(A,B,C)|~B=C)))),
% 0.25/0.62 inference(NNF_transformation,[status(thm)],[f200])).
% 0.25/0.62 fof(f202,plain,(
% 0.25/0.62 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v1_group_1(X1)|~m1_group_2(X1,X0)|~v1_group_1(X2)|~m1_group_2(X2,X0)|~r1_group_2(X0,X1,X2)|X1=X2)),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f201])).
% 0.25/0.62 fof(f207,plain,(
% 0.25/0.62 ![A,B]: (((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|(v1_group_1(k5_group_4(A,B))&m1_group_2(k5_group_4(A,B),A)))),
% 0.25/0.62 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.25/0.62 fof(f208,plain,(
% 0.25/0.62 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_group_1(k5_group_4(X0,X1)))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f207])).
% 0.25/0.62 fof(f209,plain,(
% 0.25/0.62 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m1_group_2(k5_group_4(X0,X1),X0))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f207])).
% 0.25/0.62 fof(f210,plain,(
% 0.25/0.62 ![A,B,C]: ((((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|~m1_group_2(B,A))|~m1_group_2(C,A))|(v1_group_1(k8_group_4(A,B,C))&m1_group_2(k8_group_4(A,B,C),A)))),
% 0.25/0.62 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.25/0.62 fof(f211,plain,(
% 0.25/0.62 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~m1_group_2(X2,X0)|v1_group_1(k8_group_4(X0,X1,X2)))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f210])).
% 0.25/0.62 fof(f212,plain,(
% 0.25/0.62 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~m1_group_2(X2,X0)|m1_group_2(k8_group_4(X0,X1,X2),X0))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f210])).
% 0.25/0.62 fof(f226,plain,(
% 0.25/0.62 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_group_2(B,A)|(![C]: (~m1_group_2(C,A)|(![D]: (~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))|(~D=k2_xboole_0(u1_struct_0(B),u1_struct_0(C))|r1_group_2(A,k8_group_4(A,B,C),k5_group_4(A,D))))))))))),
% 0.25/0.62 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.25/0.62 fof(f227,plain,(
% 0.25/0.62 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~m1_group_2(X2,X0)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))|~X3=k2_xboole_0(u1_struct_0(X1),u1_struct_0(X2))|r1_group_2(X0,k8_group_4(X0,X1,X2),k5_group_4(X0,X3)))),
% 0.25/0.62 inference(cnf_transformation,[status(thm)],[f226])).
% 0.25/0.62 fof(f230,plain,(
% 0.25/0.62 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~m1_group_2(X2,X0)|~m1_subset_1(k2_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),k1_zfmisc_1(u1_struct_0(X0)))|r1_group_2(X0,k8_group_4(X0,X1,X2),k5_group_4(X0,k2_xboole_0(u1_struct_0(X1),u1_struct_0(X2)))))),
% 0.25/0.62 inference(destructive_equality_resolution,[status(thm)],[f227])).
% 0.25/0.62 fof(f300,definition,(
% 0.25/0.62 sQ8_spl <=> (v3_struct_0(sK0_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f301,plain,(
% 0.25/0.62 v3_struct_0(sK0_skl)|~sQ8_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f300])).
% 0.25/0.62 fof(f303,definition,(
% 0.25/0.62 sQ9_spl <=> (l1_group_1(sK0_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f305,plain,(
% 0.25/0.62 ~l1_group_1(sK0_skl)|sQ9_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f303])).
% 0.25/0.62 fof(f310,plain,(
% 0.25/0.62 $false|sQ9_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f305,f70])).
% 0.25/0.62 fof(f311,plain,(
% 0.25/0.62 sQ9_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f310])).
% 0.25/0.62 fof(f312,plain,(
% 0.25/0.62 $false|~sQ8_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f301,f67])).
% 0.25/0.62 fof(f313,plain,(
% 0.25/0.62 ~sQ8_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f312])).
% 0.25/0.62 fof(f317,plain,(
% 0.25/0.62 ![X0]: (v3_struct_0(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|v1_group_1(k5_group_4(sK0_skl,X0)))),
% 0.25/0.62 inference(resolution,[status(thm)],[f208,f68])).
% 0.25/0.62 fof(f325,definition,(
% 0.25/0.62 sQ13_spl <=> (v4_group_1(sK0_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f327,plain,(
% 0.25/0.62 ~v4_group_1(sK0_skl)|sQ13_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f325])).
% 0.25/0.62 fof(f328,definition,(
% 0.25/0.62 ![X0]: (sQ14_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|v1_group_1(k5_group_4(sK0_skl,X0))))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f329,plain,(
% 0.25/0.62 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|v1_group_1(k5_group_4(sK0_skl,X0))|~sQ14_spl)),
% 0.25/0.62 inference(component_clause,[status(thm)],[f328])).
% 0.25/0.62 fof(f331,plain,(
% 0.25/0.62 sQ8_spl|~sQ13_spl|~sQ9_spl|sQ14_spl),
% 0.25/0.62 inference(split_clause,[status(thm)],[f317,f300,f325,f303,f328])).
% 0.25/0.62 fof(f334,plain,(
% 0.25/0.62 $false|sQ13_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f327,f69])).
% 0.25/0.62 fof(f335,plain,(
% 0.25/0.62 sQ13_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f334])).
% 0.25/0.62 fof(f341,definition,(
% 0.25/0.62 sQ15_spl <=> (v3_group_1(sK0_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f343,plain,(
% 0.25/0.62 ~v3_group_1(sK0_skl)|sQ15_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f341])).
% 0.25/0.62 fof(f348,plain,(
% 0.25/0.62 $false|sQ15_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f343,f68])).
% 0.25/0.62 fof(f349,plain,(
% 0.25/0.62 sQ15_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f348])).
% 0.25/0.62 fof(f404,plain,(
% 0.25/0.62 v1_group_1(k5_group_4(sK0_skl,sK5_skl))|~sQ14_spl),
% 0.25/0.62 inference(resolution,[status(thm)],[f329,f80])).
% 0.25/0.62 fof(f452,plain,(
% 0.25/0.62 ![X0,X1]: (v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m1_group_2(X0,sK0_skl)|~m1_group_2(X1,sK0_skl)|m1_group_2(k8_group_4(sK0_skl,X0,X1),sK0_skl))),
% 0.25/0.62 inference(resolution,[status(thm)],[f212,f69])).
% 0.25/0.62 fof(f457,definition,(
% 0.25/0.62 ![X0,X1]: (sQ38_spl <=> (~m1_group_2(X0,sK0_skl)|~m1_group_2(X1,sK0_skl)|m1_group_2(k8_group_4(sK0_skl,X0,X1),sK0_skl)))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f458,plain,(
% 0.25/0.62 ![X0,X1]: (~m1_group_2(X0,sK0_skl)|~m1_group_2(X1,sK0_skl)|m1_group_2(k8_group_4(sK0_skl,X0,X1),sK0_skl)|~sQ38_spl)),
% 0.25/0.62 inference(component_clause,[status(thm)],[f457])).
% 0.25/0.62 fof(f460,plain,(
% 0.25/0.62 sQ8_spl|~sQ15_spl|~sQ9_spl|sQ38_spl),
% 0.25/0.62 inference(split_clause,[status(thm)],[f452,f300,f341,f303,f457])).
% 0.25/0.62 fof(f523,plain,(
% 0.25/0.62 ![X0,X1]: (v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m1_group_2(X0,sK0_skl)|~m1_group_2(X1,sK0_skl)|~m1_subset_1(k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(sK0_skl)))|r1_group_2(sK0_skl,k8_group_4(sK0_skl,X0,X1),k5_group_4(sK0_skl,k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))))),
% 0.25/0.62 inference(resolution,[status(thm)],[f230,f69])).
% 0.25/0.62 fof(f528,definition,(
% 0.25/0.62 ![X0,X1]: (sQ49_spl <=> (~m1_group_2(X0,sK0_skl)|~m1_group_2(X1,sK0_skl)|~m1_subset_1(k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(sK0_skl)))|r1_group_2(sK0_skl,k8_group_4(sK0_skl,X0,X1),k5_group_4(sK0_skl,k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))))))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f529,plain,(
% 0.25/0.62 ![X0,X1]: (~m1_group_2(X0,sK0_skl)|~m1_group_2(X1,sK0_skl)|~m1_subset_1(k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(sK0_skl)))|r1_group_2(sK0_skl,k8_group_4(sK0_skl,X0,X1),k5_group_4(sK0_skl,k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))))|~sQ49_spl)),
% 0.25/0.62 inference(component_clause,[status(thm)],[f528])).
% 0.25/0.62 fof(f531,plain,(
% 0.25/0.62 sQ8_spl|~sQ15_spl|~sQ9_spl|sQ49_spl),
% 0.25/0.62 inference(split_clause,[status(thm)],[f523,f300,f341,f303,f528])).
% 0.25/0.62 fof(f667,definition,(
% 0.25/0.62 sQ72_spl <=> (m1_relset_1(sK4_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f669,plain,(
% 0.25/0.62 ~m1_relset_1(sK4_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ72_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f667])).
% 0.25/0.62 fof(f670,definition,(
% 0.25/0.62 sQ73_spl <=> (v1_funct_1(sK4_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f672,plain,(
% 0.25/0.62 ~v1_funct_1(sK4_skl)|sQ73_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f670])).
% 0.25/0.62 fof(f685,plain,(
% 0.25/0.62 ~m1_group_2(sK2_skl,sK0_skl)|~m1_group_2(sK3_skl,sK0_skl)|~m1_subset_1(k2_xboole_0(u1_struct_0(sK2_skl),u1_struct_0(sK3_skl)),k1_zfmisc_1(u1_struct_0(sK0_skl)))|r1_group_2(sK0_skl,k8_group_4(sK0_skl,sK2_skl,sK3_skl),k5_group_4(sK0_skl,sK5_skl))|~sQ49_spl),
% 0.25/0.62 inference(paramodulation,[status(thm)],[f81,f529])).
% 0.25/0.62 fof(f689,definition,(
% 0.25/0.62 sQ77_spl <=> (m1_group_2(sK2_skl,sK0_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f691,plain,(
% 0.25/0.62 ~m1_group_2(sK2_skl,sK0_skl)|sQ77_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f689])).
% 0.25/0.62 fof(f692,definition,(
% 0.25/0.62 sQ78_spl <=> (m1_group_2(sK3_skl,sK0_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f694,plain,(
% 0.25/0.62 ~m1_group_2(sK3_skl,sK0_skl)|sQ78_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f692])).
% 0.25/0.62 fof(f695,definition,(
% 0.25/0.62 sQ79_spl <=> (m1_subset_1(k2_xboole_0(u1_struct_0(sK2_skl),u1_struct_0(sK3_skl)),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f697,plain,(
% 0.25/0.62 ~m1_subset_1(k2_xboole_0(u1_struct_0(sK2_skl),u1_struct_0(sK3_skl)),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ79_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f695])).
% 0.25/0.62 fof(f698,definition,(
% 0.25/0.62 sQ80_spl <=> (r1_group_2(sK0_skl,k8_group_4(sK0_skl,sK2_skl,sK3_skl),k5_group_4(sK0_skl,sK5_skl)))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f699,plain,(
% 0.25/0.62 r1_group_2(sK0_skl,k8_group_4(sK0_skl,sK2_skl,sK3_skl),k5_group_4(sK0_skl,sK5_skl))|~sQ80_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f698])).
% 0.25/0.62 fof(f701,plain,(
% 0.25/0.62 ~sQ77_spl|~sQ78_spl|~sQ79_spl|sQ80_spl|~sQ49_spl),
% 0.25/0.62 inference(split_clause,[status(thm)],[f685,f689,f692,f695,f698,f528])).
% 0.25/0.62 fof(f704,plain,(
% 0.25/0.62 ~m1_subset_1(sK5_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ79_spl),
% 0.25/0.62 inference(forward_demodulation,[status(thm)],[f81,f697])).
% 0.25/0.62 fof(f705,plain,(
% 0.25/0.62 $false|sQ79_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f704,f80])).
% 0.25/0.62 fof(f706,plain,(
% 0.25/0.62 sQ79_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f705])).
% 0.25/0.62 fof(f707,plain,(
% 0.25/0.62 $false|sQ78_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f694,f76])).
% 0.25/0.62 fof(f708,plain,(
% 0.25/0.62 sQ78_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f707])).
% 0.25/0.62 fof(f709,plain,(
% 0.25/0.62 $false|sQ77_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f691,f75])).
% 0.25/0.62 fof(f710,plain,(
% 0.25/0.62 sQ77_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f709])).
% 0.25/0.62 fof(f793,plain,(
% 0.25/0.62 $false|sQ73_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f672,f77])).
% 0.25/0.62 fof(f794,plain,(
% 0.25/0.62 sQ73_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f793])).
% 0.25/0.62 fof(f844,plain,(
% 0.25/0.62 ![X0]: (~v1_funct_1(sK4_skl)|~m1_relset_1(sK4_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|k2_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK4_skl,X0)=k9_relat_1(sK4_skl,X0))),
% 0.25/0.62 inference(resolution,[status(thm)],[f195,f78])).
% 0.25/0.62 fof(f847,definition,(
% 0.25/0.62 ![X0]: (sQ97_spl <=> (k2_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK4_skl,X0)=k9_relat_1(sK4_skl,X0)))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f848,plain,(
% 0.25/0.62 ![X0]: (k2_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK4_skl,X0)=k9_relat_1(sK4_skl,X0)|~sQ97_spl)),
% 0.25/0.62 inference(component_clause,[status(thm)],[f847])).
% 0.25/0.62 fof(f850,plain,(
% 0.25/0.62 ~sQ73_spl|~sQ72_spl|sQ97_spl),
% 0.25/0.62 inference(split_clause,[status(thm)],[f844,f670,f667,f847])).
% 0.25/0.62 fof(f888,plain,(
% 0.25/0.62 ~m2_relset_1(sK4_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ72_spl),
% 0.25/0.62 inference(resolution,[status(thm)],[f669,f198])).
% 0.25/0.62 fof(f889,plain,(
% 0.25/0.62 $false|sQ72_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f888,f79])).
% 0.25/0.62 fof(f890,plain,(
% 0.25/0.62 sQ72_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f889])).
% 0.25/0.62 fof(f976,plain,(
% 0.25/0.62 ![X0,X1]: (v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_group_1(X0)|~m1_group_2(X0,sK0_skl)|~v1_group_1(X1)|~m1_group_2(X1,sK0_skl)|~r1_group_2(sK0_skl,X0,X1)|X0=X1)),
% 0.25/0.62 inference(resolution,[status(thm)],[f202,f69])).
% 0.25/0.62 fof(f981,definition,(
% 0.25/0.62 ![X0,X1]: (sQ123_spl <=> (~v1_group_1(X0)|~m1_group_2(X0,sK0_skl)|~v1_group_1(X1)|~m1_group_2(X1,sK0_skl)|~r1_group_2(sK0_skl,X0,X1)|X0=X1))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f982,plain,(
% 0.25/0.62 ![X0,X1]: (~v1_group_1(X0)|~m1_group_2(X0,sK0_skl)|~v1_group_1(X1)|~m1_group_2(X1,sK0_skl)|~r1_group_2(sK0_skl,X0,X1)|X0=X1|~sQ123_spl)),
% 0.25/0.62 inference(component_clause,[status(thm)],[f981])).
% 0.25/0.62 fof(f984,plain,(
% 0.25/0.62 sQ8_spl|~sQ15_spl|~sQ9_spl|sQ123_spl),
% 0.25/0.62 inference(split_clause,[status(thm)],[f976,f300,f341,f303,f981])).
% 0.25/0.62 fof(f1023,plain,(
% 0.25/0.62 ~k2_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK4_skl,u1_struct_0(k8_group_4(sK0_skl,sK2_skl,sK3_skl)))=k9_relat_1(sK4_skl,u1_struct_0(k5_group_4(sK0_skl,sK5_skl)))|~sQ97_spl),
% 0.25/0.62 inference(backward_demodulation,[status(thm)],[f848,f82])).
% 0.25/0.62 fof(f1026,plain,(
% 0.25/0.62 ~k9_relat_1(sK4_skl,u1_struct_0(k8_group_4(sK0_skl,sK2_skl,sK3_skl)))=k9_relat_1(sK4_skl,u1_struct_0(k5_group_4(sK0_skl,sK5_skl)))|~sQ97_spl),
% 0.25/0.62 inference(forward_demodulation,[status(thm)],[f848,f1023])).
% 0.25/0.62 fof(f1559,definition,(
% 0.25/0.62 sQ213_spl <=> (m1_subset_1(sK5_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f1561,plain,(
% 0.25/0.62 ~m1_subset_1(sK5_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ213_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f1559])).
% 0.25/0.62 fof(f1568,plain,(
% 0.25/0.62 $false|sQ213_spl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f1561,f80])).
% 0.25/0.62 fof(f1569,plain,(
% 0.25/0.62 sQ213_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f1568])).
% 0.25/0.62 fof(f1597,plain,(
% 0.25/0.62 ~v1_group_1(k8_group_4(sK0_skl,sK2_skl,sK3_skl))|~m1_group_2(k8_group_4(sK0_skl,sK2_skl,sK3_skl),sK0_skl)|~v1_group_1(k5_group_4(sK0_skl,sK5_skl))|~m1_group_2(k5_group_4(sK0_skl,sK5_skl),sK0_skl)|k8_group_4(sK0_skl,sK2_skl,sK3_skl)=k5_group_4(sK0_skl,sK5_skl)|~sQ80_spl|~sQ123_spl),
% 0.25/0.62 inference(resolution,[status(thm)],[f699,f982])).
% 0.25/0.62 fof(f1598,definition,(
% 0.25/0.62 sQ219_spl <=> (v1_group_1(k8_group_4(sK0_skl,sK2_skl,sK3_skl)))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f1600,plain,(
% 0.25/0.62 ~v1_group_1(k8_group_4(sK0_skl,sK2_skl,sK3_skl))|sQ219_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f1598])).
% 0.25/0.62 fof(f1601,definition,(
% 0.25/0.62 sQ220_spl <=> (m1_group_2(k8_group_4(sK0_skl,sK2_skl,sK3_skl),sK0_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f1603,plain,(
% 0.25/0.62 ~m1_group_2(k8_group_4(sK0_skl,sK2_skl,sK3_skl),sK0_skl)|sQ220_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f1601])).
% 0.25/0.62 fof(f1604,definition,(
% 0.25/0.62 sQ221_spl <=> (v1_group_1(k5_group_4(sK0_skl,sK5_skl)))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f1606,plain,(
% 0.25/0.62 ~v1_group_1(k5_group_4(sK0_skl,sK5_skl))|sQ221_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f1604])).
% 0.25/0.62 fof(f1607,definition,(
% 0.25/0.62 sQ222_spl <=> (m1_group_2(k5_group_4(sK0_skl,sK5_skl),sK0_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f1609,plain,(
% 0.25/0.62 ~m1_group_2(k5_group_4(sK0_skl,sK5_skl),sK0_skl)|sQ222_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f1607])).
% 0.25/0.62 fof(f1610,definition,(
% 0.25/0.62 sQ223_spl <=> (k8_group_4(sK0_skl,sK2_skl,sK3_skl)=k5_group_4(sK0_skl,sK5_skl))),
% 0.25/0.62 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 0.25/0.62 fof(f1611,plain,(
% 0.25/0.62 k8_group_4(sK0_skl,sK2_skl,sK3_skl)=k5_group_4(sK0_skl,sK5_skl)|~sQ223_spl),
% 0.25/0.62 inference(component_clause,[status(thm)],[f1610])).
% 0.25/0.62 fof(f1613,plain,(
% 0.25/0.62 ~sQ219_spl|~sQ220_spl|~sQ221_spl|~sQ222_spl|sQ223_spl|~sQ80_spl|~sQ123_spl),
% 0.25/0.62 inference(split_clause,[status(thm)],[f1597,f1598,f1601,f1604,f1607,f1610,f698,f981])).
% 0.25/0.62 fof(f1622,plain,(
% 0.25/0.62 ~k9_relat_1(sK4_skl,u1_struct_0(k5_group_4(sK0_skl,sK5_skl)))=k9_relat_1(sK4_skl,u1_struct_0(k5_group_4(sK0_skl,sK5_skl)))|~sQ223_spl|~sQ97_spl),
% 0.25/0.62 inference(backward_demodulation,[status(thm)],[f1611,f1026])).
% 0.25/0.62 fof(f1629,plain,(
% 0.25/0.62 $false|~sQ223_spl|~sQ97_spl),
% 0.25/0.62 inference(trivial_equality_resolution,[status(thm)],[f1622])).
% 0.25/0.62 fof(f1630,plain,(
% 0.25/0.62 ~sQ223_spl|~sQ97_spl),
% 0.25/0.62 inference(contradiction_clause,[status(thm)],[f1629])).
% 0.25/0.62 fof(f1631,plain,(
% 0.25/0.62 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m1_subset_1(sK5_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ222_spl),
% 0.25/0.62 inference(resolution,[status(thm)],[f1609,f209])).
% 0.25/0.62 fof(f1632,plain,(
% 0.25/0.62 sQ8_spl|~sQ15_spl|~sQ13_spl|~sQ9_spl|~sQ213_spl|sQ222_spl),
% 0.25/0.62 inference(split_clause,[status(thm)],[f1631,f300,f341,f325,f303,f1559,f1607])).
% 0.25/0.64 fof(f1633,plain,(
% 0.25/0.64 $false|~sQ14_spl|sQ221_spl),
% 0.25/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1606,f404])).
% 0.25/0.64 fof(f1634,plain,(
% 0.25/0.64 ~sQ14_spl|sQ221_spl),
% 0.25/0.64 inference(contradiction_clause,[status(thm)],[f1633])).
% 0.25/0.64 fof(f1639,plain,(
% 0.25/0.64 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m1_group_2(sK2_skl,sK0_skl)|~m1_group_2(sK3_skl,sK0_skl)|sQ219_spl),
% 0.25/0.64 inference(resolution,[status(thm)],[f1600,f211])).
% 0.25/0.64 fof(f1640,plain,(
% 0.25/0.64 sQ8_spl|~sQ15_spl|~sQ13_spl|~sQ9_spl|~sQ77_spl|~sQ78_spl|sQ219_spl),
% 0.25/0.64 inference(split_clause,[status(thm)],[f1639,f300,f341,f325,f303,f689,f692,f1598])).
% 0.25/0.64 fof(f1666,plain,(
% 0.25/0.64 ~m1_group_2(sK2_skl,sK0_skl)|~m1_group_2(sK3_skl,sK0_skl)|sQ220_spl|~sQ38_spl),
% 0.25/0.64 inference(resolution,[status(thm)],[f1603,f458])).
% 0.25/0.64 fof(f1667,plain,(
% 0.25/0.64 ~sQ77_spl|~sQ78_spl|sQ220_spl|~sQ38_spl),
% 0.25/0.64 inference(split_clause,[status(thm)],[f1666,f689,f692,f1601,f457])).
% 0.25/0.64 fof(f1668,plain,(
% 0.25/0.64 $false),
% 0.25/0.64 inference(sat_refutation,[status(thm)],[f311,f313,f331,f335,f349,f460,f531,f701,f706,f708,f710,f794,f850,f890,f984,f1569,f1613,f1630,f1632,f1634,f1640,f1667])).
% 0.25/0.64 % SZS output end CNFRefutation for theBenchmark.p
% 0.25/0.65 % Elapsed time: 0.187273 seconds
% 0.25/0.65 % CPU time: 1.166969 seconds
% 0.25/0.65 % Total memory used: 124.651 MB
% 0.25/0.65 % Net memory used: 124.029 MB
%------------------------------------------------------------------------------