%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP632+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 : n007.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:36:58 PM UTC 2026
% Result : Theorem 50.14s 6.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP632+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.33 % Computer : n007.cluster.edu
% 0.09/0.33 % Model : x86_64 x86_64
% 0.09/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.33 % Memory : 8046.5625MB
% 0.09/0.33 % OS : Linux 6.8.0-71-generic
% 0.09/0.33 % CPULimit : 300
% 0.09/0.33 % WCLimit : 300
% 0.09/0.33 % DateTime : Sun Sep 20 20:20:05 UTC 2026
% 0.09/0.33 % CPUTime :
% 0.09/0.35 % Drodi V4.1.1
% 50.14/6.94 % Refutation found
% 50.14/6.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 50.14/6.94 % SZS output start CNFRefutation for theBenchmark
% 50.14/6.94 fof(f1,conjecture,(
% 50.14/6.94 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))=> ( k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),k6_autgroup(A,k2_group_1(A)),B) = B& k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),B,k6_autgroup(A,k2_group_1(A))) = B ) ) )) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f2,negated_conjecture,(
% 50.14/6.94 ~((! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))=> ( k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),k6_autgroup(A,k2_group_1(A)),B) = B& k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),B,k6_autgroup(A,k2_group_1(A))) = B ) ) )) ))),
% 50.14/6.94 inference(negated_conjecture,[status(cth)],[f1])).
% 50.14/6.94 fof(f5,axiom,(
% 50.14/6.94 (! [A] :( v1_fraenkel(A)=> (! [B] :( m1_subset_1(B,A)=> ( v1_relat_1(B)& v1_funct_1(B) ) ) )) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f7,axiom,(
% 50.14/6.94 (! [A,B,C] :( m1_relset_1(C,A,B)=> ( ( v1_funct_1(C)& v1_partfun1(C,A,B) )=> ( v1_funct_1(C)& v1_funct_2(C,A,B) ) ) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f10,axiom,(
% 50.14/6.94 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> v1_relat_1(C) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f20,axiom,(
% 50.14/6.94 (! [A] :( ( ~ v3_struct_0(A)& l1_group_1(A) )=> m1_subset_1(k2_group_1(A),u1_struct_0(A)) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f22,axiom,(
% 50.14/6.94 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> m1_fraenkel(k4_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f23,axiom,(
% 50.14/6.94 (! [A,B] :( ( v1_relat_1(A)& v1_relat_1(B) )=> v1_relat_1(k5_relat_1(A,B)) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f24,axiom,(
% 50.14/6.94 (! [A,B] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A)& m1_subset_1(B,u1_struct_0(A)) )=> m2_fraenkel(k6_autgroup(A,B),u1_struct_0(A),u1_struct_0(A),k4_autgroup(A)) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f25,axiom,(
% 50.14/6.94 (! [A] :( v1_partfun1(k6_partfun1(A),A,A)& m2_relset_1(k6_partfun1(A),A,A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f29,axiom,(
% 50.14/6.94 (! [A] :( l1_group_1(A)=> l1_struct_0(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f31,axiom,(
% 50.14/6.94 (! [A,B,C] :( m1_fraenkel(C,A,B)=> ( ~ v1_xboole_0(C)& v1_fraenkel(C) ) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f34,axiom,(
% 50.14/6.94 (! [A,B,C] :( ( ~ v1_xboole_0(B)& m1_fraenkel(C,A,B) )=> (! [D] :( m2_fraenkel(D,A,B,C)=> ( v1_funct_1(D)& v1_funct_2(D,A,B)& m2_relset_1(D,A,B) ) ) )) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f35,axiom,(
% 50.14/6.94 (! [A,B,C] :( m2_relset_1(C,A,B)=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f36,axiom,(
% 50.14/6.94 (! [A] :( l1_group_1(A)=> ( v1_funct_1(u1_group_1(A))& v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))& m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f38,axiom,(
% 50.14/6.94 (? [A] : l1_group_1(A) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f42,axiom,(
% 50.14/6.94 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f47,axiom,(
% 50.14/6.94 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f49,axiom,(
% 50.14/6.94 (! [A] :( v1_relat_1(k6_relat_1(A))& v1_funct_1(k6_relat_1(A)) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f52,axiom,(
% 50.14/6.94 (? [A] :( ~ v1_xboole_0(A)& v1_fraenkel(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f53,axiom,(
% 50.14/6.94 (? [A] :( v1_relat_1(A)& v1_funct_1(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f55,axiom,(
% 50.14/6.94 (? [A] :( l1_group_1(A)& v1_group_1(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f56,axiom,(
% 50.14/6.94 (? [A] :( v1_relat_1(A)& v1_funct_1(A)& v2_funct_1(A)& v1_xboole_0(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f59,axiom,(
% 50.14/6.94 (! [A] :(? [B] :( m1_relset_1(B,A,A)& v1_relat_1(B)& v1_funct_1(B)& v2_funct_1(B)& v1_funct_2(B,A,A)& v2_funct_2(B,A,A)& v3_funct_2(B,A,A) ) ))),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f60,axiom,(
% 50.14/6.94 (? [A] :( l1_group_1(A)& ~ v3_struct_0(A)& v1_group_1(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f63,axiom,(
% 50.14/6.94 (? [A] :( v1_relat_1(A)& v1_funct_1(A)& v2_funct_1(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f64,axiom,(
% 50.14/6.94 (? [A] :( l1_group_1(A)& ~ v3_struct_0(A)& v1_group_1(A)& v2_group_1(A)& v3_group_1(A)& v4_group_1(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f66,axiom,(
% 50.14/6.94 (? [A] :( l1_struct_0(A)& ~ v3_struct_0(A) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f68,axiom,(
% 50.14/6.94 (! [A] : k6_partfun1(A) = k6_relat_1(A) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f69,axiom,(
% 50.14/6.94 (! [A,B,C,D,E] :( ( ~ v1_xboole_0(B)& v1_funct_1(D)& v1_funct_2(D,A,B)& m1_relset_1(D,A,B)& v1_funct_1(E)& v1_funct_2(E,B,C)& m1_relset_1(E,B,C) )=> k7_funct_2(A,B,C,D,E) = k5_relat_1(D,E) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f70,axiom,(
% 50.14/6.94 (! [A,B,C,D,E,F] :( ( m1_relset_1(E,A,B)& m1_relset_1(F,C,D) )=> k7_relset_1(A,B,C,D,E,F) = k5_relat_1(E,F) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f71,axiom,(
% 50.14/6.94 (! [A,B,C] :( ( ~ v1_xboole_0(B)& m1_fraenkel(C,A,B) )=> (! [D] :( m2_fraenkel(D,A,B,C)<=> m1_subset_1(D,C) ) )) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f72,axiom,(
% 50.14/6.94 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f75,axiom,(
% 50.14/6.94 (! [A,B,C] :( m2_relset_1(C,A,B)=> ( k7_relset_1(A,A,A,B,k6_partfun1(A),C) = C& k7_relset_1(A,B,B,B,C,k6_partfun1(B)) = C ) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f76,axiom,(
% 50.14/6.94 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> k6_autgroup(A,k2_group_1(A)) = k6_partfun1(u1_struct_0(A)) ) )),
% 50.14/6.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.14/6.94 fof(f84,plain,(
% 50.14/6.94 (?[A]: (((((~v3_struct_0(A)&v1_group_1(A))&v3_group_1(A))&v4_group_1(A))&l1_group_1(A))&(?[B]: (m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))&(~k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),k6_autgroup(A,k2_group_1(A)),B)=B|~k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),B,k6_autgroup(A,k2_group_1(A)))=B)))))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 50.14/6.94 fof(f85,plain,(
% 50.14/6.94 (((((~v3_struct_0(sK0_skl)&v1_group_1(sK0_skl))&v3_group_1(sK0_skl))&v4_group_1(sK0_skl))&l1_group_1(sK0_skl))&(m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))&(~k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),sK1_skl)=sK1_skl|~k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_autgroup(sK0_skl,k2_group_1(sK0_skl)))=sK1_skl)))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f84])).
% 50.14/6.94 fof(f86,plain,(
% 50.14/6.94 ~v3_struct_0(sK0_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f85])).
% 50.14/6.94 fof(f87,plain,(
% 50.14/6.94 v1_group_1(sK0_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f85])).
% 50.14/6.94 fof(f88,plain,(
% 50.14/6.94 v3_group_1(sK0_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f85])).
% 50.14/6.94 fof(f89,plain,(
% 50.14/6.94 v4_group_1(sK0_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f85])).
% 50.14/6.94 fof(f90,plain,(
% 50.14/6.94 l1_group_1(sK0_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f85])).
% 50.14/6.94 fof(f91,plain,(
% 50.14/6.94 m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f85])).
% 50.14/6.94 fof(f92,plain,(
% 50.14/6.94 ~k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),sK1_skl)=sK1_skl|~k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_autgroup(sK0_skl,k2_group_1(sK0_skl)))=sK1_skl),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f85])).
% 50.14/6.94 fof(f97,plain,(
% 50.14/6.94 ![A]: (~v1_fraenkel(A)|(![B]: (~m1_subset_1(B,A)|(v1_relat_1(B)&v1_funct_1(B)))))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 50.14/6.94 fof(f98,plain,(
% 50.14/6.94 ![X0,X1]: (~v1_fraenkel(X0)|~m1_subset_1(X1,X0)|v1_relat_1(X1))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f97])).
% 50.14/6.94 fof(f99,plain,(
% 50.14/6.94 ![X0,X1]: (~v1_fraenkel(X0)|~m1_subset_1(X1,X0)|v1_funct_1(X1))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f97])).
% 50.14/6.94 fof(f102,plain,(
% 50.14/6.94 ![A,B,C]: (~m1_relset_1(C,A,B)|((~v1_funct_1(C)|~v1_partfun1(C,A,B))|(v1_funct_1(C)&v1_funct_2(C,A,B))))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 50.14/6.94 fof(f104,plain,(
% 50.14/6.94 ![X0,X1,X2]: (~m1_relset_1(X0,X1,X2)|~v1_funct_1(X0)|~v1_partfun1(X0,X1,X2)|v1_funct_2(X0,X1,X2))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f102])).
% 50.14/6.94 fof(f111,plain,(
% 50.14/6.94 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))|v1_relat_1(C))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 50.14/6.94 fof(f112,plain,(
% 50.14/6.94 ![C]: ((![A,B]: ~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))|v1_relat_1(C))),
% 50.14/6.94 inference(miniscoping,[status(thm)],[f111])).
% 50.14/6.94 fof(f113,plain,(
% 50.14/6.94 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|v1_relat_1(X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f112])).
% 50.14/6.94 fof(f146,plain,(
% 50.14/6.94 ![A]: ((v3_struct_0(A)|~l1_group_1(A))|m1_subset_1(k2_group_1(A),u1_struct_0(A)))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 50.14/6.94 fof(f147,plain,(
% 50.14/6.94 ![X0]: (v3_struct_0(X0)|~l1_group_1(X0)|m1_subset_1(k2_group_1(X0),u1_struct_0(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f146])).
% 50.14/6.94 fof(f148,plain,(
% 50.14/6.94 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|m1_fraenkel(k4_autgroup(A),u1_struct_0(A),u1_struct_0(A)))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 50.14/6.94 fof(f149,plain,(
% 50.14/6.94 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f148])).
% 50.14/6.94 fof(f150,plain,(
% 50.14/6.94 ![A,B]: ((~v1_relat_1(A)|~v1_relat_1(B))|v1_relat_1(k5_relat_1(A,B)))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 50.14/6.94 fof(f151,plain,(
% 50.14/6.94 ![X0,X1]: (~v1_relat_1(X0)|~v1_relat_1(X1)|v1_relat_1(k5_relat_1(X0,X1)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f150])).
% 50.14/6.94 fof(f152,plain,(
% 50.14/6.94 ![A,B]: ((((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|~m1_subset_1(B,u1_struct_0(A)))|m2_fraenkel(k6_autgroup(A,B),u1_struct_0(A),u1_struct_0(A),k4_autgroup(A)))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 50.14/6.94 fof(f153,plain,(
% 50.14/6.94 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_subset_1(X1,u1_struct_0(X0))|m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f152])).
% 50.14/6.94 fof(f154,plain,(
% 50.14/6.94 (![A]: v1_partfun1(k6_partfun1(A),A,A))&(![A]: m2_relset_1(k6_partfun1(A),A,A))),
% 50.14/6.94 inference(miniscoping,[status(thm)],[f25])).
% 50.14/6.94 fof(f155,plain,(
% 50.14/6.94 ![X0]: (v1_partfun1(k6_partfun1(X0),X0,X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f154])).
% 50.14/6.94 fof(f156,plain,(
% 50.14/6.94 ![X0]: (m2_relset_1(k6_partfun1(X0),X0,X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f154])).
% 50.14/6.94 fof(f164,plain,(
% 50.14/6.94 ![A]: (~l1_group_1(A)|l1_struct_0(A))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 50.14/6.94 fof(f165,plain,(
% 50.14/6.94 ![X0]: (~l1_group_1(X0)|l1_struct_0(X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f164])).
% 50.14/6.94 fof(f166,plain,(
% 50.14/6.94 ![A,B,C]: (~m1_fraenkel(C,A,B)|(~v1_xboole_0(C)&v1_fraenkel(C)))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 50.14/6.94 fof(f167,plain,(
% 50.14/6.94 ![C]: ((![A,B]: ~m1_fraenkel(C,A,B))|(~v1_xboole_0(C)&v1_fraenkel(C)))),
% 50.14/6.94 inference(miniscoping,[status(thm)],[f166])).
% 50.14/6.94 fof(f169,plain,(
% 50.14/6.94 ![X0,X1,X2]: (~m1_fraenkel(X0,X1,X2)|v1_fraenkel(X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f167])).
% 50.14/6.94 fof(f170,plain,(
% 50.14/6.94 ![A,B,C]: ((v1_xboole_0(B)|~m1_fraenkel(C,A,B))|(![D]: (~m2_fraenkel(D,A,B,C)|((v1_funct_1(D)&v1_funct_2(D,A,B))&m2_relset_1(D,A,B)))))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 50.14/6.94 fof(f171,plain,(
% 50.14/6.94 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_fraenkel(X1,X2,X0)|~m2_fraenkel(X3,X2,X0,X1)|v1_funct_1(X3))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f170])).
% 50.14/6.94 fof(f172,plain,(
% 50.14/6.94 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_fraenkel(X1,X2,X0)|~m2_fraenkel(X3,X2,X0,X1)|v1_funct_2(X3,X2,X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f170])).
% 50.14/6.94 fof(f173,plain,(
% 50.14/6.94 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_fraenkel(X1,X2,X0)|~m2_fraenkel(X3,X2,X0,X1)|m2_relset_1(X3,X2,X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f170])).
% 50.14/6.94 fof(f174,plain,(
% 50.14/6.94 ![A,B,C]: (~m2_relset_1(C,A,B)|m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 50.14/6.94 fof(f175,plain,(
% 50.14/6.94 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f174])).
% 50.14/6.94 fof(f176,plain,(
% 50.14/6.94 ![A]: (~l1_group_1(A)|((v1_funct_1(u1_group_1(A))&v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)))&m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 50.14/6.94 fof(f177,plain,(
% 50.14/6.94 ![X0]: (~l1_group_1(X0)|v1_funct_1(u1_group_1(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f176])).
% 50.14/6.94 fof(f179,plain,(
% 50.14/6.94 ![X0]: (~l1_group_1(X0)|m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f176])).
% 50.14/6.94 fof(f180,plain,(
% 50.14/6.94 l1_group_1(sK2_skl)),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f38])).
% 50.14/6.94 fof(f181,plain,(
% 50.14/6.94 l1_group_1(sK2_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f180])).
% 50.14/6.94 fof(f188,plain,(
% 50.14/6.94 ![A]: m1_subset_1(sK6_skl(A),A)),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B,sK6_skl(A))],[f42])).
% 50.14/6.94 fof(f189,plain,(
% 50.14/6.94 ![X0]: (m1_subset_1(sK6_skl(X0),X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f188])).
% 50.14/6.94 fof(f201,plain,(
% 50.14/6.94 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 50.14/6.94 fof(f202,plain,(
% 50.14/6.94 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f201])).
% 50.14/6.94 fof(f204,plain,(
% 50.14/6.94 (![A]: v1_relat_1(k6_relat_1(A)))&(![A]: v1_funct_1(k6_relat_1(A)))),
% 50.14/6.94 inference(miniscoping,[status(thm)],[f49])).
% 50.14/6.94 fof(f206,plain,(
% 50.14/6.94 ![X0]: (v1_funct_1(k6_relat_1(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f204])).
% 50.14/6.94 fof(f217,plain,(
% 50.14/6.94 (~v1_xboole_0(sK9_skl)&v1_fraenkel(sK9_skl))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f52])).
% 50.14/6.94 fof(f219,plain,(
% 50.14/6.94 v1_fraenkel(sK9_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f217])).
% 50.14/6.94 fof(f220,plain,(
% 50.14/6.94 (v1_relat_1(sK10_skl)&v1_funct_1(sK10_skl))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f53])).
% 50.14/6.94 fof(f221,plain,(
% 50.14/6.94 v1_relat_1(sK10_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f220])).
% 50.14/6.94 fof(f228,plain,(
% 50.14/6.94 (l1_group_1(sK12_skl)&v1_group_1(sK12_skl))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f55])).
% 50.14/6.94 fof(f229,plain,(
% 50.14/6.94 l1_group_1(sK12_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f228])).
% 50.14/6.94 fof(f231,plain,(
% 50.14/6.94 (((v1_relat_1(sK13_skl)&v1_funct_1(sK13_skl))&v2_funct_1(sK13_skl))&v1_xboole_0(sK13_skl))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f56])).
% 50.14/6.94 fof(f232,plain,(
% 50.14/6.94 v1_relat_1(sK13_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f231])).
% 50.14/6.94 fof(f242,plain,(
% 50.14/6.94 ![A]: ((((((m1_relset_1(sK16_skl(A),A,A)&v1_relat_1(sK16_skl(A)))&v1_funct_1(sK16_skl(A)))&v2_funct_1(sK16_skl(A)))&v1_funct_2(sK16_skl(A),A,A))&v2_funct_2(sK16_skl(A),A,A))&v3_funct_2(sK16_skl(A),A,A))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(B,sK16_skl(A))],[f59])).
% 50.14/6.94 fof(f243,plain,(
% 50.14/6.94 ![X0]: (m1_relset_1(sK16_skl(X0),X0,X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f242])).
% 50.14/6.94 fof(f245,plain,(
% 50.14/6.94 ![X0]: (v1_funct_1(sK16_skl(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f242])).
% 50.14/6.94 fof(f250,plain,(
% 50.14/6.94 ((l1_group_1(sK17_skl)&~v3_struct_0(sK17_skl))&v1_group_1(sK17_skl))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f60])).
% 50.14/6.94 fof(f251,plain,(
% 50.14/6.94 l1_group_1(sK17_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f250])).
% 50.14/6.94 fof(f260,plain,(
% 50.14/6.94 ((v1_relat_1(sK20_skl)&v1_funct_1(sK20_skl))&v2_funct_1(sK20_skl))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f63])).
% 50.14/6.94 fof(f261,plain,(
% 50.14/6.94 v1_relat_1(sK20_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f260])).
% 50.14/6.94 fof(f264,plain,(
% 50.14/6.94 (((((l1_group_1(sK21_skl)&~v3_struct_0(sK21_skl))&v1_group_1(sK21_skl))&v2_group_1(sK21_skl))&v3_group_1(sK21_skl))&v4_group_1(sK21_skl))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(A,sK21_skl)],[f64])).
% 50.14/6.94 fof(f265,plain,(
% 50.14/6.94 l1_group_1(sK21_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f264])).
% 50.14/6.94 fof(f279,plain,(
% 50.14/6.94 (l1_struct_0(sK23_skl)&~v3_struct_0(sK23_skl))),
% 50.14/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f66])).
% 50.14/6.94 fof(f280,plain,(
% 50.14/6.94 l1_struct_0(sK23_skl)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f279])).
% 50.14/6.94 fof(f286,plain,(
% 50.14/6.94 ![X0]: (k6_partfun1(X0)=k6_relat_1(X0))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f68])).
% 50.14/6.94 fof(f287,plain,(
% 50.14/6.94 ![A,B,C,D,E]: (((((((v1_xboole_0(B)|~v1_funct_1(D))|~v1_funct_2(D,A,B))|~m1_relset_1(D,A,B))|~v1_funct_1(E))|~v1_funct_2(E,B,C))|~m1_relset_1(E,B,C))|k7_funct_2(A,B,C,D,E)=k5_relat_1(D,E))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 50.14/6.94 fof(f288,plain,(
% 50.14/6.94 ![X0,X1,X2,X3,X4]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X2,X0)|~m1_relset_1(X1,X2,X0)|~v1_funct_1(X3)|~v1_funct_2(X3,X0,X4)|~m1_relset_1(X3,X0,X4)|k7_funct_2(X2,X0,X4,X1,X3)=k5_relat_1(X1,X3))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f287])).
% 50.14/6.94 fof(f289,plain,(
% 50.14/6.94 ![A,B,C,D,E,F]: ((~m1_relset_1(E,A,B)|~m1_relset_1(F,C,D))|k7_relset_1(A,B,C,D,E,F)=k5_relat_1(E,F))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 50.14/6.94 fof(f290,plain,(
% 50.14/6.94 ![X0,X1,X2,X3,X4,X5]: (~m1_relset_1(X0,X1,X2)|~m1_relset_1(X3,X4,X5)|k7_relset_1(X1,X2,X4,X5,X0,X3)=k5_relat_1(X0,X3))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f289])).
% 50.14/6.94 fof(f291,plain,(
% 50.14/6.94 ![A,B,C]: ((v1_xboole_0(B)|~m1_fraenkel(C,A,B))|(![D]: (m2_fraenkel(D,A,B,C)<=>m1_subset_1(D,C))))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 50.14/6.94 fof(f292,plain,(
% 50.14/6.94 ![A,B,C]: ((v1_xboole_0(B)|~m1_fraenkel(C,A,B))|(![D]: ((~m2_fraenkel(D,A,B,C)|m1_subset_1(D,C))&(m2_fraenkel(D,A,B,C)|~m1_subset_1(D,C)))))),
% 50.14/6.94 inference(NNF_transformation,[status(thm)],[f291])).
% 50.14/6.94 fof(f293,plain,(
% 50.14/6.94 ![A,B,C]: ((v1_xboole_0(B)|~m1_fraenkel(C,A,B))|((![D]: (~m2_fraenkel(D,A,B,C)|m1_subset_1(D,C)))&(![D]: (m2_fraenkel(D,A,B,C)|~m1_subset_1(D,C)))))),
% 50.14/6.94 inference(miniscoping,[status(thm)],[f292])).
% 50.14/6.94 fof(f294,plain,(
% 50.14/6.94 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_fraenkel(X1,X2,X0)|~m2_fraenkel(X3,X2,X0,X1)|m1_subset_1(X3,X1))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f293])).
% 50.14/6.94 fof(f296,plain,(
% 50.14/6.94 ![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)))),
% 50.14/6.94 inference(NNF_transformation,[status(thm)],[f72])).
% 50.14/6.94 fof(f297,plain,(
% 50.14/6.94 (![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)))),
% 50.14/6.94 inference(miniscoping,[status(thm)],[f296])).
% 50.14/6.94 fof(f298,plain,(
% 50.14/6.94 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f297])).
% 50.14/6.94 fof(f304,plain,(
% 50.14/6.94 ![A,B,C]: (~m2_relset_1(C,A,B)|(k7_relset_1(A,A,A,B,k6_partfun1(A),C)=C&k7_relset_1(A,B,B,B,C,k6_partfun1(B))=C))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 50.14/6.94 fof(f305,plain,(
% 50.14/6.94 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|k7_relset_1(X1,X1,X1,X2,k6_partfun1(X1),X0)=X0)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f304])).
% 50.14/6.94 fof(f306,plain,(
% 50.14/6.94 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|k7_relset_1(X1,X2,X2,X2,X0,k6_partfun1(X2))=X0)),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f304])).
% 50.14/6.94 fof(f307,plain,(
% 50.14/6.94 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|k6_autgroup(A,k2_group_1(A))=k6_partfun1(u1_struct_0(A)))),
% 50.14/6.94 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 50.14/6.94 fof(f308,plain,(
% 50.14/6.94 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|k6_autgroup(X0,k2_group_1(X0))=k6_partfun1(u1_struct_0(X0)))),
% 50.14/6.94 inference(cnf_transformation,[status(thm)],[f307])).
% 50.14/6.94 fof(f329,definition,(
% 50.14/6.94 sQ0_spl <=> (k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),sK1_skl)=sK1_skl)),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f331,plain,(
% 50.14/6.94 ~k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),sK1_skl)=sK1_skl|sQ0_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f329])).
% 50.14/6.94 fof(f332,definition,(
% 50.14/6.94 sQ1_spl <=> (k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_autgroup(sK0_skl,k2_group_1(sK0_skl)))=sK1_skl)),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f334,plain,(
% 50.14/6.94 ~k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_autgroup(sK0_skl,k2_group_1(sK0_skl)))=sK1_skl|sQ1_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f332])).
% 50.14/6.94 fof(f335,plain,(
% 50.14/6.94 ~sQ0_spl|~sQ1_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f92,f329,f332])).
% 50.14/6.94 fof(f345,plain,(
% 50.14/6.94 ![X0]: (v1_funct_1(k6_partfun1(X0)))),
% 50.14/6.94 inference(backward_demodulation,[status(thm)],[f286,f206])).
% 50.14/6.94 fof(f356,definition,(
% 50.14/6.94 sQ4_spl <=> (v1_group_1(sK0_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f358,plain,(
% 50.14/6.94 ~v1_group_1(sK0_skl)|sQ4_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f356])).
% 50.14/6.94 fof(f363,plain,(
% 50.14/6.94 $false|sQ4_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f358,f87])).
% 50.14/6.94 fof(f364,plain,(
% 50.14/6.94 sQ4_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f363])).
% 50.14/6.94 fof(f366,plain,(
% 50.14/6.94 v3_struct_0(sK0_skl)|m1_subset_1(k2_group_1(sK0_skl),u1_struct_0(sK0_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f147,f90])).
% 50.14/6.94 fof(f374,definition,(
% 50.14/6.94 sQ8_spl <=> (v3_struct_0(sK0_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f375,plain,(
% 50.14/6.94 v3_struct_0(sK0_skl)|~sQ8_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f374])).
% 50.14/6.94 fof(f377,definition,(
% 50.14/6.94 sQ9_spl <=> (m1_subset_1(k2_group_1(sK0_skl),u1_struct_0(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f378,plain,(
% 50.14/6.94 m1_subset_1(k2_group_1(sK0_skl),u1_struct_0(sK0_skl))|~sQ9_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f377])).
% 50.14/6.94 fof(f380,plain,(
% 50.14/6.94 sQ8_spl|sQ9_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f366,f374,f377])).
% 50.14/6.94 fof(f381,plain,(
% 50.14/6.94 $false|~sQ8_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f375,f86])).
% 50.14/6.94 fof(f382,plain,(
% 50.14/6.94 ~sQ8_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f381])).
% 50.14/6.94 fof(f384,plain,(
% 50.14/6.94 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f149,f90])).
% 50.14/6.94 fof(f395,definition,(
% 50.14/6.94 sQ13_spl <=> (v3_group_1(sK0_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f397,plain,(
% 50.14/6.94 ~v3_group_1(sK0_skl)|sQ13_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f395])).
% 50.14/6.94 fof(f398,definition,(
% 50.14/6.94 sQ14_spl <=> (v4_group_1(sK0_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f400,plain,(
% 50.14/6.94 ~v4_group_1(sK0_skl)|sQ14_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f398])).
% 50.14/6.94 fof(f401,definition,(
% 50.14/6.94 sQ15_spl <=> (m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f402,plain,(
% 50.14/6.94 m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~sQ15_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f401])).
% 50.14/6.94 fof(f404,plain,(
% 50.14/6.94 sQ8_spl|~sQ4_spl|~sQ13_spl|~sQ14_spl|sQ15_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f384,f374,f356,f395,f398,f401])).
% 50.14/6.94 fof(f406,plain,(
% 50.14/6.94 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|m2_fraenkel(k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))|~sQ9_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f378,f153])).
% 50.14/6.94 fof(f409,definition,(
% 50.14/6.94 sQ16_spl <=> (l1_group_1(sK0_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f411,plain,(
% 50.14/6.94 ~l1_group_1(sK0_skl)|sQ16_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f409])).
% 50.14/6.94 fof(f412,definition,(
% 50.14/6.94 sQ17_spl <=> (m2_fraenkel(k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f413,plain,(
% 50.14/6.94 m2_fraenkel(k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))|~sQ17_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f412])).
% 50.14/6.94 fof(f415,plain,(
% 50.14/6.94 sQ8_spl|~sQ4_spl|~sQ13_spl|~sQ14_spl|~sQ16_spl|sQ17_spl|~sQ9_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f406,f374,f356,f395,f398,f409,f412,f377])).
% 50.14/6.94 fof(f427,plain,(
% 50.14/6.94 $false|sQ14_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f400,f89])).
% 50.14/6.94 fof(f428,plain,(
% 50.14/6.94 sQ14_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f427])).
% 50.14/6.94 fof(f429,plain,(
% 50.14/6.94 $false|sQ13_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f397,f88])).
% 50.14/6.94 fof(f430,plain,(
% 50.14/6.94 sQ13_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f429])).
% 50.14/6.94 fof(f431,plain,(
% 50.14/6.94 $false|sQ16_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f411,f90])).
% 50.14/6.94 fof(f432,plain,(
% 50.14/6.94 sQ16_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f431])).
% 50.14/6.94 fof(f478,plain,(
% 50.14/6.94 v1_xboole_0(u1_struct_0(sK0_skl))|~m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v1_funct_1(sK1_skl)),
% 50.14/6.94 inference(resolution,[status(thm)],[f171,f91])).
% 50.14/6.94 fof(f479,definition,(
% 50.14/6.94 sQ31_spl <=> (v1_xboole_0(u1_struct_0(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f480,plain,(
% 50.14/6.94 v1_xboole_0(u1_struct_0(sK0_skl))|~sQ31_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f479])).
% 50.14/6.94 fof(f486,definition,(
% 50.14/6.94 sQ33_spl <=> (v1_funct_1(sK1_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f489,plain,(
% 50.14/6.94 sQ31_spl|~sQ15_spl|sQ33_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f478,f479,f401,f486])).
% 50.14/6.94 fof(f491,plain,(
% 50.14/6.94 v1_xboole_0(u1_struct_0(sK0_skl))|~m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f172,f91])).
% 50.14/6.94 fof(f496,definition,(
% 50.14/6.94 sQ35_spl <=> (v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f497,plain,(
% 50.14/6.94 v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~sQ35_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f496])).
% 50.14/6.94 fof(f499,plain,(
% 50.14/6.94 sQ31_spl|~sQ15_spl|sQ35_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f491,f479,f401,f496])).
% 50.14/6.94 fof(f517,plain,(
% 50.14/6.94 v1_xboole_0(u1_struct_0(sK0_skl))|~m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|m1_subset_1(k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),k4_autgroup(sK0_skl))|~sQ17_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f294,f413])).
% 50.14/6.94 fof(f519,definition,(
% 50.14/6.94 sQ40_spl <=> (m1_subset_1(k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),k4_autgroup(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f520,plain,(
% 50.14/6.94 m1_subset_1(k6_autgroup(sK0_skl,k2_group_1(sK0_skl)),k4_autgroup(sK0_skl))|~sQ40_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f519])).
% 50.14/6.94 fof(f522,plain,(
% 50.14/6.94 sQ31_spl|~sQ15_spl|sQ40_spl|~sQ17_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f517,f479,f401,f519,f412])).
% 50.14/6.94 fof(f528,plain,(
% 50.14/6.94 v1_xboole_0(u1_struct_0(sK0_skl))|~m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f173,f91])).
% 50.14/6.94 fof(f533,definition,(
% 50.14/6.94 sQ43_spl <=> (m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f534,plain,(
% 50.14/6.94 m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~sQ43_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f533])).
% 50.14/6.94 fof(f536,plain,(
% 50.14/6.94 sQ31_spl|~sQ15_spl|sQ43_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f528,f479,f401,f533])).
% 50.14/6.94 fof(f565,plain,(
% 50.14/6.94 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|k6_autgroup(sK0_skl,k2_group_1(sK0_skl))=k6_partfun1(u1_struct_0(sK0_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f308,f90])).
% 50.14/6.94 fof(f574,definition,(
% 50.14/6.94 sQ51_spl <=> (k6_autgroup(sK0_skl,k2_group_1(sK0_skl))=k6_partfun1(u1_struct_0(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f575,plain,(
% 50.14/6.94 k6_autgroup(sK0_skl,k2_group_1(sK0_skl))=k6_partfun1(u1_struct_0(sK0_skl))|~sQ51_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f574])).
% 50.14/6.94 fof(f577,plain,(
% 50.14/6.94 sQ8_spl|~sQ4_spl|~sQ13_spl|~sQ14_spl|sQ51_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f565,f374,f356,f395,f398,f574])).
% 50.14/6.94 fof(f579,plain,(
% 50.14/6.94 ~k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)=sK1_skl|~sQ51_spl|sQ0_spl),
% 50.14/6.94 inference(backward_demodulation,[status(thm)],[f575,f331])).
% 50.14/6.94 fof(f596,definition,(
% 50.14/6.94 sQ55_spl <=> (v1_funct_1(k6_partfun1(u1_struct_0(sK0_skl))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f656,definition,(
% 50.14/6.94 sQ67_spl <=> (l1_group_1(sK17_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f658,plain,(
% 50.14/6.94 ~l1_group_1(sK17_skl)|sQ67_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f656])).
% 50.14/6.94 fof(f676,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK13_skl,sK13_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f151,f232])).
% 50.14/6.94 fof(f677,plain,(
% 50.14/6.94 ![X0]: (~v1_relat_1(X0)|v1_relat_1(k5_relat_1(sK13_skl,X0)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f151,f232])).
% 50.14/6.94 fof(f678,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK10_skl,sK10_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f151,f221])).
% 50.14/6.94 fof(f679,plain,(
% 50.14/6.94 ![X0]: (~v1_relat_1(X0)|v1_relat_1(k5_relat_1(sK10_skl,X0)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f151,f221])).
% 50.14/6.94 fof(f681,plain,(
% 50.14/6.94 ![X0]: (~v1_relat_1(X0)|v1_relat_1(k5_relat_1(X0,sK13_skl)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f151,f232])).
% 50.14/6.94 fof(f682,plain,(
% 50.14/6.94 ![X0]: (~v1_relat_1(X0)|v1_relat_1(k5_relat_1(X0,sK10_skl)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f151,f221])).
% 50.14/6.94 fof(f686,plain,(
% 50.14/6.94 ![X0]: (~m1_relset_1(k6_partfun1(X0),X0,X0)|~v1_funct_1(k6_partfun1(X0))|v1_funct_2(k6_partfun1(X0),X0,X0))),
% 50.14/6.94 inference(resolution,[status(thm)],[f155,f104])).
% 50.14/6.94 fof(f690,plain,(
% 50.14/6.94 ![X0]: (~m1_relset_1(k6_partfun1(X0),X0,X0)|v1_funct_2(k6_partfun1(X0),X0,X0))),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f686,f345])).
% 50.14/6.94 fof(f691,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK20_skl,sK20_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f261,f151])).
% 50.14/6.94 fof(f692,plain,(
% 50.14/6.94 ![X0]: (~v1_relat_1(X0)|v1_relat_1(k5_relat_1(X0,sK20_skl)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f261,f151])).
% 50.14/6.94 fof(f694,plain,(
% 50.14/6.94 ![X0]: (~v1_relat_1(X0)|v1_relat_1(k5_relat_1(sK20_skl,X0)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f261,f151])).
% 50.14/6.94 fof(f696,plain,(
% 50.14/6.94 l1_struct_0(sK12_skl)),
% 50.14/6.94 inference(resolution,[status(thm)],[f165,f229])).
% 50.14/6.94 fof(f697,plain,(
% 50.14/6.94 l1_struct_0(sK2_skl)),
% 50.14/6.94 inference(resolution,[status(thm)],[f165,f181])).
% 50.14/6.94 fof(f698,plain,(
% 50.14/6.94 l1_struct_0(sK0_skl)),
% 50.14/6.94 inference(resolution,[status(thm)],[f165,f90])).
% 50.14/6.94 fof(f746,plain,(
% 50.14/6.94 v1_fraenkel(k4_autgroup(sK0_skl))|~sQ15_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f169,f402])).
% 50.14/6.94 fof(f748,plain,(
% 50.14/6.94 v1_funct_1(u1_group_1(sK21_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f177,f265])).
% 50.14/6.94 fof(f749,plain,(
% 50.14/6.94 v1_funct_1(u1_group_1(sK17_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f177,f251])).
% 50.14/6.94 fof(f750,plain,(
% 50.14/6.94 v1_funct_1(u1_group_1(sK12_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f177,f229])).
% 50.14/6.94 fof(f751,plain,(
% 50.14/6.94 v1_funct_1(u1_group_1(sK2_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f177,f181])).
% 50.14/6.94 fof(f793,plain,(
% 50.14/6.94 m2_relset_1(u1_group_1(sK21_skl),k2_zfmisc_1(u1_struct_0(sK21_skl),u1_struct_0(sK21_skl)),u1_struct_0(sK21_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f179,f265])).
% 50.14/6.94 fof(f794,plain,(
% 50.14/6.94 m2_relset_1(u1_group_1(sK17_skl),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)),u1_struct_0(sK17_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f179,f251])).
% 50.14/6.94 fof(f795,plain,(
% 50.14/6.94 m2_relset_1(u1_group_1(sK12_skl),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f179,f229])).
% 50.14/6.94 fof(f796,plain,(
% 50.14/6.94 m2_relset_1(u1_group_1(sK2_skl),k2_zfmisc_1(u1_struct_0(sK2_skl),u1_struct_0(sK2_skl)),u1_struct_0(sK2_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f179,f181])).
% 50.14/6.94 fof(f797,plain,(
% 50.14/6.94 m2_relset_1(u1_group_1(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f179,f90])).
% 50.14/6.94 fof(f860,plain,(
% 50.14/6.94 m1_subset_1(u1_group_1(sK0_skl),k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))))),
% 50.14/6.94 inference(resolution,[status(thm)],[f797,f175])).
% 50.14/6.94 fof(f870,plain,(
% 50.14/6.94 ![X0]: (~v1_fraenkel(X0)|v1_relat_1(sK6_skl(X0)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f189,f98])).
% 50.14/6.94 fof(f882,plain,(
% 50.14/6.94 v1_relat_1(u1_group_1(sK0_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f860,f113])).
% 50.14/6.94 fof(f903,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),u1_group_1(sK0_skl)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f882,f151])).
% 50.14/6.94 fof(f1066,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(k5_relat_1(u1_group_1(sK0_skl),u1_group_1(sK0_skl)),k5_relat_1(u1_group_1(sK0_skl),u1_group_1(sK0_skl))))),
% 50.14/6.94 inference(resolution,[status(thm)],[f903,f151])).
% 50.14/6.94 fof(f1156,plain,(
% 50.14/6.94 v3_struct_0(sK0_skl)|~l1_struct_0(sK0_skl)|~sQ31_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f202,f480])).
% 50.14/6.94 fof(f1161,definition,(
% 50.14/6.94 sQ153_spl <=> (l1_struct_0(sK0_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f1163,plain,(
% 50.14/6.94 ~l1_struct_0(sK0_skl)|sQ153_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f1161])).
% 50.14/6.94 fof(f1164,plain,(
% 50.14/6.94 sQ8_spl|~sQ153_spl|~sQ31_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f1156,f374,f1161,f479])).
% 50.14/6.94 fof(f1167,plain,(
% 50.14/6.94 $false|sQ153_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f1163,f698])).
% 50.14/6.94 fof(f1168,plain,(
% 50.14/6.94 sQ153_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f1167])).
% 50.14/6.94 fof(f1171,plain,(
% 50.14/6.94 m1_subset_1(k6_partfun1(u1_struct_0(sK0_skl)),k4_autgroup(sK0_skl))|~sQ51_spl|~sQ40_spl),
% 50.14/6.94 inference(forward_demodulation,[status(thm)],[f575,f520])).
% 50.14/6.94 fof(f1217,definition,(
% 50.14/6.94 sQ160_spl <=> (m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f1219,plain,(
% 50.14/6.94 ~m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ160_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f1217])).
% 50.14/6.94 fof(f1270,definition,(
% 50.14/6.94 sQ172_spl <=> (v1_fraenkel(k4_autgroup(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f1272,plain,(
% 50.14/6.94 ~v1_fraenkel(k4_autgroup(sK0_skl))|sQ172_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f1270])).
% 50.14/6.94 fof(f1275,plain,(
% 50.14/6.94 $false|~sQ15_spl|sQ172_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f1272,f746])).
% 50.14/6.94 fof(f1276,plain,(
% 50.14/6.94 ~sQ15_spl|sQ172_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f1275])).
% 50.14/6.94 fof(f1862,plain,(
% 50.14/6.94 ![X0,X1]: (v1_xboole_0(u1_struct_0(sK0_skl))|~v1_funct_1(sK1_skl)|~m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_funct_1(X0)|~v1_funct_2(X0,u1_struct_0(sK0_skl),X1)|~m1_relset_1(X0,u1_struct_0(sK0_skl),X1)|k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),X1,sK1_skl,X0)=k5_relat_1(sK1_skl,X0)|~sQ35_spl)),
% 50.14/6.94 inference(resolution,[status(thm)],[f288,f497])).
% 50.14/6.94 fof(f1866,plain,(
% 50.14/6.94 ![X0,X1]: (v1_xboole_0(u1_struct_0(sK0_skl))|~v1_funct_1(X0)|~v1_funct_2(X0,X1,u1_struct_0(sK0_skl))|~m1_relset_1(X0,X1,u1_struct_0(sK0_skl))|~v1_funct_1(sK1_skl)|~m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|k7_funct_2(X1,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),X0,sK1_skl)=k5_relat_1(X0,sK1_skl)|~sQ35_spl)),
% 50.14/6.94 inference(resolution,[status(thm)],[f288,f497])).
% 50.14/6.94 fof(f1878,definition,(
% 50.14/6.94 ![X0,X1]: (sQ231_spl <=> (~v1_funct_1(X0)|~v1_funct_2(X0,u1_struct_0(sK0_skl),X1)|~m1_relset_1(X0,u1_struct_0(sK0_skl),X1)|k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),X1,sK1_skl,X0)=k5_relat_1(sK1_skl,X0)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f1879,plain,(
% 50.14/6.94 ![X0,X1]: (~v1_funct_1(X0)|~v1_funct_2(X0,u1_struct_0(sK0_skl),X1)|~m1_relset_1(X0,u1_struct_0(sK0_skl),X1)|k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),X1,sK1_skl,X0)=k5_relat_1(sK1_skl,X0)|~sQ231_spl)),
% 50.14/6.94 inference(component_clause,[status(thm)],[f1878])).
% 50.14/6.94 fof(f1881,plain,(
% 50.14/6.94 sQ31_spl|~sQ33_spl|~sQ160_spl|sQ231_spl|~sQ35_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f1862,f479,f486,f1217,f1878,f496])).
% 50.14/6.94 fof(f1888,definition,(
% 50.14/6.94 ![X0,X1]: (sQ233_spl <=> (~v1_funct_1(X0)|~v1_funct_2(X0,X1,u1_struct_0(sK0_skl))|~m1_relset_1(X0,X1,u1_struct_0(sK0_skl))|k7_funct_2(X1,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),X0,sK1_skl)=k5_relat_1(X0,sK1_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f1889,plain,(
% 50.14/6.94 ![X0,X1]: (~v1_funct_1(X0)|~v1_funct_2(X0,X1,u1_struct_0(sK0_skl))|~m1_relset_1(X0,X1,u1_struct_0(sK0_skl))|k7_funct_2(X1,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),X0,sK1_skl)=k5_relat_1(X0,sK1_skl)|~sQ233_spl)),
% 50.14/6.94 inference(component_clause,[status(thm)],[f1888])).
% 50.14/6.94 fof(f1891,plain,(
% 50.14/6.94 sQ31_spl|sQ233_spl|~sQ33_spl|~sQ160_spl|~sQ35_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f1866,f479,f1888,f486,f1217,f496])).
% 50.14/6.94 fof(f2057,plain,(
% 50.14/6.94 m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~sQ43_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f298,f534])).
% 50.14/6.94 fof(f2060,plain,(
% 50.14/6.94 ![X0]: (m1_relset_1(k6_partfun1(X0),X0,X0))),
% 50.14/6.94 inference(resolution,[status(thm)],[f298,f156])).
% 50.14/6.94 fof(f2061,plain,(
% 50.14/6.94 $false|sQ160_spl|~sQ43_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f2057,f1219])).
% 50.14/6.94 fof(f2062,plain,(
% 50.14/6.94 sQ160_spl|~sQ43_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f2061])).
% 50.14/6.94 fof(f2065,plain,(
% 50.14/6.94 ![X0]: (v1_funct_2(k6_partfun1(X0),X0,X0))),
% 50.14/6.94 inference(backward_subsumption_resolution,[status(thm)],[f690,f2060])).
% 50.14/6.94 fof(f2181,plain,(
% 50.14/6.94 k7_relset_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)=sK1_skl|~sQ43_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f305,f534])).
% 50.14/6.94 fof(f2185,plain,(
% 50.14/6.94 k7_relset_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))=sK1_skl|~sQ43_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f306,f534])).
% 50.14/6.94 fof(f2813,plain,(
% 50.14/6.94 ![X0,X1,X2,X3]: (~m1_relset_1(X0,X1,X2)|k7_relset_1(X1,X2,X3,X3,X0,k6_partfun1(X3))=k5_relat_1(X0,k6_partfun1(X3)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f2060,f290])).
% 50.14/6.94 fof(f2815,plain,(
% 50.14/6.94 ![X0,X1,X2,X3]: (~m1_relset_1(X0,X1,X2)|k7_relset_1(X3,X3,X1,X2,k6_partfun1(X3),X0)=k5_relat_1(k6_partfun1(X3),X0))),
% 50.14/6.94 inference(resolution,[status(thm)],[f2060,f290])).
% 50.14/6.94 fof(f2888,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK13_skl,u1_group_1(sK0_skl)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f677,f882])).
% 50.14/6.94 fof(f2889,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK13_skl,sK20_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f677,f261])).
% 50.14/6.94 fof(f2891,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK13_skl,sK10_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f677,f221])).
% 50.14/6.94 fof(f2920,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK10_skl,u1_group_1(sK0_skl)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f679,f882])).
% 50.14/6.94 fof(f2921,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK10_skl,sK20_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f679,f261])).
% 50.14/6.94 fof(f2922,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK10_skl,sK13_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f679,f232])).
% 50.14/6.94 fof(f3096,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK13_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f681,f882])).
% 50.14/6.94 fof(f3097,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK20_skl,sK13_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f681,f261])).
% 50.14/6.94 fof(f3121,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK10_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f682,f882])).
% 50.14/6.94 fof(f3122,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK20_skl,sK10_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f682,f261])).
% 50.14/6.94 fof(f3140,definition,(
% 50.14/6.94 sQ385_spl <=> (m1_relset_1(k6_partfun1(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3142,plain,(
% 50.14/6.94 ~m1_relset_1(k6_partfun1(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ385_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3140])).
% 50.14/6.94 fof(f3147,definition,(
% 50.14/6.94 sQ387_spl <=> (v1_funct_1(sK16_skl(u1_struct_0(sK0_skl))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3149,plain,(
% 50.14/6.94 ~v1_funct_1(sK16_skl(u1_struct_0(sK0_skl)))|sQ387_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3147])).
% 50.14/6.94 fof(f3156,plain,(
% 50.14/6.94 $false|sQ385_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3142,f2060])).
% 50.14/6.94 fof(f3157,plain,(
% 50.14/6.94 sQ385_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3156])).
% 50.14/6.94 fof(f3201,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK20_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f692,f882])).
% 50.14/6.94 fof(f3227,plain,(
% 50.14/6.94 v1_relat_1(k5_relat_1(sK20_skl,u1_group_1(sK0_skl)))),
% 50.14/6.94 inference(resolution,[status(thm)],[f694,f882])).
% 50.14/6.94 fof(f3241,plain,(
% 50.14/6.94 $false|sQ387_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3149,f245])).
% 50.14/6.94 fof(f3242,plain,(
% 50.14/6.94 sQ387_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3241])).
% 50.14/6.94 fof(f3307,definition,(
% 50.14/6.94 sQ400_spl <=> (v1_relat_1(sK6_skl(sK9_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ400_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3309,plain,(
% 50.14/6.94 ~v1_relat_1(sK6_skl(sK9_skl))|sQ400_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3307])).
% 50.14/6.94 fof(f3362,definition,(
% 50.14/6.94 sQ408_spl <=> (v1_funct_1(u1_group_1(sK21_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3364,plain,(
% 50.14/6.94 ~v1_funct_1(u1_group_1(sK21_skl))|sQ408_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3362])).
% 50.14/6.94 fof(f3365,definition,(
% 50.14/6.94 sQ409_spl <=> (m1_relset_1(u1_group_1(sK21_skl),k2_zfmisc_1(u1_struct_0(sK21_skl),u1_struct_0(sK21_skl)),u1_struct_0(sK21_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3367,plain,(
% 50.14/6.94 ~m1_relset_1(u1_group_1(sK21_skl),k2_zfmisc_1(u1_struct_0(sK21_skl),u1_struct_0(sK21_skl)),u1_struct_0(sK21_skl))|sQ409_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3365])).
% 50.14/6.94 fof(f3431,plain,(
% 50.14/6.94 $false|sQ408_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3364,f748])).
% 50.14/6.94 fof(f3432,plain,(
% 50.14/6.94 sQ408_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3431])).
% 50.14/6.94 fof(f3453,definition,(
% 50.14/6.94 sQ426_spl <=> (v1_funct_1(u1_group_1(sK12_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3455,plain,(
% 50.14/6.94 ~v1_funct_1(u1_group_1(sK12_skl))|sQ426_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3453])).
% 50.14/6.94 fof(f3456,definition,(
% 50.14/6.94 sQ427_spl <=> (m1_relset_1(u1_group_1(sK12_skl),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3458,plain,(
% 50.14/6.94 ~m1_relset_1(u1_group_1(sK12_skl),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl))|sQ427_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3456])).
% 50.14/6.94 fof(f3525,plain,(
% 50.14/6.94 $false|sQ426_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3455,f750])).
% 50.14/6.94 fof(f3526,plain,(
% 50.14/6.94 sQ426_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3525])).
% 50.14/6.94 fof(f3554,definition,(
% 50.14/6.94 sQ447_spl <=> (l1_group_1(sK12_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ447_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3556,plain,(
% 50.14/6.94 ~l1_group_1(sK12_skl)|sQ447_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3554])).
% 50.14/6.94 fof(f3576,plain,(
% 50.14/6.94 $false|sQ447_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3556,f229])).
% 50.14/6.94 fof(f3577,plain,(
% 50.14/6.94 sQ447_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3576])).
% 50.14/6.94 fof(f3611,definition,(
% 50.14/6.94 sQ457_spl <=> (l1_struct_0(sK12_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ457_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3613,plain,(
% 50.14/6.94 ~l1_struct_0(sK12_skl)|sQ457_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3611])).
% 50.14/6.94 fof(f3709,plain,(
% 50.14/6.94 $false|sQ457_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3613,f696])).
% 50.14/6.94 fof(f3710,plain,(
% 50.14/6.94 sQ457_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3709])).
% 50.14/6.94 fof(f3727,definition,(
% 50.14/6.94 sQ460_spl <=> (v1_funct_1(u1_group_1(sK2_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ460_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3729,plain,(
% 50.14/6.94 ~v1_funct_1(u1_group_1(sK2_skl))|sQ460_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3727])).
% 50.14/6.94 fof(f3730,definition,(
% 50.14/6.94 sQ461_spl <=> (m1_relset_1(u1_group_1(sK2_skl),k2_zfmisc_1(u1_struct_0(sK2_skl),u1_struct_0(sK2_skl)),u1_struct_0(sK2_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ461_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f3732,plain,(
% 50.14/6.94 ~m1_relset_1(u1_group_1(sK2_skl),k2_zfmisc_1(u1_struct_0(sK2_skl),u1_struct_0(sK2_skl)),u1_struct_0(sK2_skl))|sQ461_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f3730])).
% 50.14/6.94 fof(f3803,plain,(
% 50.14/6.94 $false|sQ460_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3729,f751])).
% 50.14/6.94 fof(f3804,plain,(
% 50.14/6.94 sQ460_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3803])).
% 50.14/6.94 fof(f3807,plain,(
% 50.14/6.94 m1_relset_1(u1_group_1(sK21_skl),k2_zfmisc_1(u1_struct_0(sK21_skl),u1_struct_0(sK21_skl)),u1_struct_0(sK21_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f793,f298])).
% 50.14/6.94 fof(f3809,plain,(
% 50.14/6.94 $false|sQ409_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3807,f3367])).
% 50.14/6.94 fof(f3810,plain,(
% 50.14/6.94 sQ409_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3809])).
% 50.14/6.94 fof(f3813,plain,(
% 50.14/6.94 m1_relset_1(u1_group_1(sK2_skl),k2_zfmisc_1(u1_struct_0(sK2_skl),u1_struct_0(sK2_skl)),u1_struct_0(sK2_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f796,f298])).
% 50.14/6.94 fof(f3815,plain,(
% 50.14/6.94 $false|sQ461_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3813,f3732])).
% 50.14/6.94 fof(f3816,plain,(
% 50.14/6.94 sQ461_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f3815])).
% 50.14/6.94 fof(f4057,definition,(
% 50.14/6.94 sQ501_spl <=> (l1_struct_0(sK2_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ501_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f4059,plain,(
% 50.14/6.94 ~l1_struct_0(sK2_skl)|sQ501_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f4057])).
% 50.14/6.94 fof(f4179,plain,(
% 50.14/6.94 $false|sQ501_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f4059,f697])).
% 50.14/6.94 fof(f4180,plain,(
% 50.14/6.94 sQ501_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f4179])).
% 50.14/6.94 fof(f4185,plain,(
% 50.14/6.94 v1_relat_1(sK6_skl(sK9_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f870,f219])).
% 50.14/6.94 fof(f4190,plain,(
% 50.14/6.94 $false|sQ400_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f4185,f3309])).
% 50.14/6.94 fof(f4191,plain,(
% 50.14/6.94 sQ400_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f4190])).
% 50.14/6.94 fof(f4276,definition,(
% 50.14/6.94 sQ507_spl <=> (l1_group_1(sK2_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ507_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f4278,plain,(
% 50.14/6.94 ~l1_group_1(sK2_skl)|sQ507_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f4276])).
% 50.14/6.94 fof(f4285,plain,(
% 50.14/6.94 $false|sQ507_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f4278,f181])).
% 50.14/6.94 fof(f4286,plain,(
% 50.14/6.94 sQ507_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f4285])).
% 50.14/6.94 fof(f4319,definition,(
% 50.14/6.94 sQ509_spl <=> (v1_relat_1(k5_relat_1(sK13_skl,sK13_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ509_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f4321,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK13_skl,sK13_skl))|sQ509_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f4319])).
% 50.14/6.94 fof(f4351,plain,(
% 50.14/6.94 $false|sQ509_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f4321,f676])).
% 50.14/6.94 fof(f4352,plain,(
% 50.14/6.94 sQ509_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f4351])).
% 50.14/6.94 fof(f4686,definition,(
% 50.14/6.94 sQ561_spl <=> (v1_relat_1(k5_relat_1(sK10_skl,sK10_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ561_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f4688,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK10_skl,sK10_skl))|sQ561_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f4686])).
% 50.14/6.94 fof(f4726,plain,(
% 50.14/6.94 $false|sQ561_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f4688,f678])).
% 50.14/6.94 fof(f4727,plain,(
% 50.14/6.94 sQ561_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f4726])).
% 50.14/6.94 fof(f4738,definition,(
% 50.14/6.94 sQ571_spl <=> (v1_relat_1(k5_relat_1(sK20_skl,sK20_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ571_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f4740,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK20_skl,sK20_skl))|sQ571_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f4738])).
% 50.14/6.94 fof(f4778,plain,(
% 50.14/6.94 $false|sQ571_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f4740,f691])).
% 50.14/6.94 fof(f4779,plain,(
% 50.14/6.94 sQ571_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f4778])).
% 50.14/6.94 fof(f5254,definition,(
% 50.14/6.94 sQ653_spl <=> (v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK20_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ653_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f5256,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK20_skl))|sQ653_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f5254])).
% 50.14/6.94 fof(f5306,plain,(
% 50.14/6.94 $false|sQ653_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f5256,f3201])).
% 50.14/6.94 fof(f5307,plain,(
% 50.14/6.94 sQ653_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f5306])).
% 50.14/6.94 fof(f5506,definition,(
% 50.14/6.94 sQ687_spl <=> (v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK13_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ687_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f5508,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK13_skl))|sQ687_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f5506])).
% 50.14/6.94 fof(f5562,plain,(
% 50.14/6.94 $false|sQ687_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f5508,f3096])).
% 50.14/6.94 fof(f5563,plain,(
% 50.14/6.94 sQ687_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f5562])).
% 50.14/6.94 fof(f5696,definition,(
% 50.14/6.94 sQ717_spl <=> (v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK10_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ717_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f5698,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(u1_group_1(sK0_skl),sK10_skl))|sQ717_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f5696])).
% 50.14/6.94 fof(f5752,plain,(
% 50.14/6.94 $false|sQ717_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f5698,f3121])).
% 50.14/6.94 fof(f5753,plain,(
% 50.14/6.94 sQ717_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f5752])).
% 50.14/6.94 fof(f5932,definition,(
% 50.14/6.94 sQ745_spl <=> (v1_relat_1(k5_relat_1(sK20_skl,u1_group_1(sK0_skl))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ745_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f5934,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK20_skl,u1_group_1(sK0_skl)))|sQ745_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f5932])).
% 50.14/6.94 fof(f5988,plain,(
% 50.14/6.94 $false|sQ745_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f5934,f3227])).
% 50.14/6.94 fof(f5989,plain,(
% 50.14/6.94 sQ745_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f5988])).
% 50.14/6.94 fof(f6161,definition,(
% 50.14/6.94 sQ783_spl <=> (v1_relat_1(k5_relat_1(sK13_skl,u1_group_1(sK0_skl))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ783_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f6163,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK13_skl,u1_group_1(sK0_skl)))|sQ783_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f6161])).
% 50.14/6.94 fof(f6217,plain,(
% 50.14/6.94 $false|sQ783_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f6163,f2888])).
% 50.14/6.94 fof(f6218,plain,(
% 50.14/6.94 sQ783_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f6217])).
% 50.14/6.94 fof(f6233,definition,(
% 50.14/6.94 sQ797_spl <=> (v1_relat_1(k5_relat_1(sK10_skl,u1_group_1(sK0_skl))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ797_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f6235,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK10_skl,u1_group_1(sK0_skl)))|sQ797_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f6233])).
% 50.14/6.94 fof(f6289,plain,(
% 50.14/6.94 $false|sQ797_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f6235,f2920])).
% 50.14/6.94 fof(f6290,plain,(
% 50.14/6.94 sQ797_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f6289])).
% 50.14/6.94 fof(f6994,plain,(
% 50.14/6.94 ~v1_funct_1(k6_partfun1(u1_struct_0(sK0_skl)))|~m1_relset_1(k6_partfun1(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))=k5_relat_1(sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))|~sQ231_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f1879,f2065])).
% 50.14/6.94 fof(f7003,definition,(
% 50.14/6.94 sQ884_spl <=> (k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))=k5_relat_1(sK1_skl,k6_partfun1(u1_struct_0(sK0_skl))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ884_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f7004,plain,(
% 50.14/6.94 k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))=k5_relat_1(sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))|~sQ884_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f7003])).
% 50.14/6.94 fof(f7006,plain,(
% 50.14/6.94 ~sQ55_spl|~sQ385_spl|sQ884_spl|~sQ231_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f6994,f596,f3140,f7003,f1878])).
% 50.14/6.94 fof(f7024,plain,(
% 50.14/6.94 ~v1_funct_1(k6_partfun1(u1_struct_0(sK0_skl)))|~m1_relset_1(k6_partfun1(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)=k5_relat_1(k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)|~sQ233_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f1889,f2065])).
% 50.14/6.94 fof(f7034,definition,(
% 50.14/6.94 sQ887_spl <=> (k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)=k5_relat_1(k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ887_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f7035,plain,(
% 50.14/6.94 k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)=k5_relat_1(k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)|~sQ887_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f7034])).
% 50.14/6.94 fof(f7037,plain,(
% 50.14/6.94 ~sQ55_spl|~sQ385_spl|sQ887_spl|~sQ233_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f7024,f596,f3140,f7034,f1888])).
% 50.14/6.94 fof(f7057,plain,(
% 50.14/6.94 ~k5_relat_1(k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)=sK1_skl|~sQ887_spl|~sQ51_spl|sQ0_spl),
% 50.14/6.94 inference(backward_demodulation,[status(thm)],[f7035,f579])).
% 50.14/6.94 fof(f7552,definition,(
% 50.14/6.94 sQ924_spl <=> (v1_relat_1(k5_relat_1(sK13_skl,sK20_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ924_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f7554,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK13_skl,sK20_skl))|sQ924_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f7552])).
% 50.14/6.94 fof(f7620,plain,(
% 50.14/6.94 $false|sQ924_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f7554,f2889])).
% 50.14/6.94 fof(f7621,plain,(
% 50.14/6.94 sQ924_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f7620])).
% 50.14/6.94 fof(f8043,definition,(
% 50.14/6.94 sQ1004_spl <=> (v1_relat_1(k5_relat_1(sK13_skl,sK10_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1004_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f8045,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK13_skl,sK10_skl))|sQ1004_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f8043])).
% 50.14/6.94 fof(f8115,plain,(
% 50.14/6.94 $false|sQ1004_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f8045,f2891])).
% 50.14/6.94 fof(f8116,plain,(
% 50.14/6.94 sQ1004_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f8115])).
% 50.14/6.94 fof(f8135,definition,(
% 50.14/6.94 sQ1022_spl <=> (v1_relat_1(k5_relat_1(sK20_skl,sK13_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1022_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f8137,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK20_skl,sK13_skl))|sQ1022_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f8135])).
% 50.14/6.94 fof(f8207,plain,(
% 50.14/6.94 $false|sQ1022_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f8137,f3097])).
% 50.14/6.94 fof(f8208,plain,(
% 50.14/6.94 sQ1022_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f8207])).
% 50.14/6.94 fof(f8227,definition,(
% 50.14/6.94 sQ1040_spl <=> (v1_relat_1(k5_relat_1(sK10_skl,sK13_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1040_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f8229,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK10_skl,sK13_skl))|sQ1040_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f8227])).
% 50.14/6.94 fof(f8299,plain,(
% 50.14/6.94 $false|sQ1040_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f8229,f2922])).
% 50.14/6.94 fof(f8300,plain,(
% 50.14/6.94 sQ1040_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f8299])).
% 50.14/6.94 fof(f8432,definition,(
% 50.14/6.94 sQ1067_spl <=> (v1_relat_1(k5_relat_1(sK10_skl,sK20_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1067_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f8434,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK10_skl,sK20_skl))|sQ1067_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f8432])).
% 50.14/6.94 fof(f8504,plain,(
% 50.14/6.94 $false|sQ1067_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f8434,f2921])).
% 50.14/6.94 fof(f8505,plain,(
% 50.14/6.94 sQ1067_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f8504])).
% 50.14/6.94 fof(f8524,definition,(
% 50.14/6.94 sQ1085_spl <=> (v1_relat_1(k5_relat_1(sK20_skl,sK10_skl)))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1085_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f8526,plain,(
% 50.14/6.94 ~v1_relat_1(k5_relat_1(sK20_skl,sK10_skl))|sQ1085_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f8524])).
% 50.14/6.94 fof(f8596,plain,(
% 50.14/6.94 $false|sQ1085_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f8526,f3122])).
% 50.14/6.94 fof(f8597,plain,(
% 50.14/6.94 sQ1085_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f8596])).
% 50.14/6.94 fof(f9012,definition,(
% 50.14/6.94 sQ1134_spl <=> (sK0_skl=sK0_skl)),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1134_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f9014,plain,(
% 50.14/6.94 ~sK0_skl=sK0_skl|sQ1134_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f9012])).
% 50.14/6.94 fof(f9019,plain,(
% 50.14/6.94 $false|sQ1134_spl),
% 50.14/6.94 inference(trivial_equality_resolution,[status(thm)],[f9014])).
% 50.14/6.94 fof(f9020,plain,(
% 50.14/6.94 sQ1134_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f9019])).
% 50.14/6.94 fof(f10912,definition,(
% 50.14/6.94 sQ1320_spl <=> (v1_funct_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1320_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f10914,plain,(
% 50.14/6.94 ~v1_funct_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))))|sQ1320_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f10912])).
% 50.14/6.94 fof(f10915,definition,(
% 50.14/6.94 sQ1321_spl <=> (m1_relset_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1321_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f10917,plain,(
% 50.14/6.94 ~m1_relset_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))|sQ1321_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f10915])).
% 50.14/6.94 fof(f10922,definition,(
% 50.14/6.94 sQ1323_spl <=> (v1_funct_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1323_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f10924,plain,(
% 50.14/6.94 ~v1_funct_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))))|sQ1323_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f10922])).
% 50.14/6.94 fof(f10926,plain,(
% 50.14/6.94 $false|sQ1323_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f10924,f245])).
% 50.14/6.94 fof(f10927,plain,(
% 50.14/6.94 sQ1323_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f10926])).
% 50.14/6.94 fof(f10928,plain,(
% 50.14/6.94 $false|sQ1321_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f10917,f2060])).
% 50.14/6.94 fof(f10929,plain,(
% 50.14/6.94 sQ1321_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f10928])).
% 50.14/6.94 fof(f10930,plain,(
% 50.14/6.94 $false|sQ1320_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f10914,f345])).
% 50.14/6.94 fof(f10931,plain,(
% 50.14/6.94 sQ1320_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f10930])).
% 50.14/6.94 fof(f12695,definition,(
% 50.14/6.94 sQ1586_spl <=> (l1_struct_0(sK23_skl))),
% 50.14/6.94 introduced(definition,[new_symbols(definition,[sQ1586_spl])],[split_symbol_definition])).
% 50.14/6.94 fof(f12697,plain,(
% 50.14/6.94 ~l1_struct_0(sK23_skl)|sQ1586_spl),
% 50.14/6.94 inference(component_clause,[status(thm)],[f12695])).
% 50.14/6.94 fof(f12736,plain,(
% 50.14/6.94 $false|sQ1586_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f12697,f280])).
% 50.14/6.94 fof(f12737,plain,(
% 50.14/6.94 sQ1586_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f12736])).
% 50.14/6.94 fof(f15509,plain,(
% 50.14/6.94 m1_relset_1(u1_group_1(sK17_skl),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)),u1_struct_0(sK17_skl))),
% 50.14/6.94 inference(resolution,[status(thm)],[f794,f298])).
% 50.14/6.94 fof(f15536,plain,(
% 50.14/6.94 ~v1_fraenkel(k4_autgroup(sK0_skl))|v1_funct_1(k6_partfun1(u1_struct_0(sK0_skl)))|~sQ51_spl|~sQ40_spl),
% 50.14/6.94 inference(resolution,[status(thm)],[f1171,f99])).
% 50.14/6.94 fof(f15542,plain,(
% 50.14/6.94 ~sQ172_spl|sQ55_spl|~sQ51_spl|~sQ40_spl),
% 50.14/6.94 inference(split_clause,[status(thm)],[f15536,f1270,f596,f574,f519])).
% 50.14/6.94 fof(f15661,plain,(
% 50.14/6.94 $false|sQ67_spl),
% 50.14/6.94 inference(forward_subsumption_resolution,[status(thm)],[f658,f251])).
% 50.14/6.94 fof(f15662,plain,(
% 50.14/6.94 sQ67_spl),
% 50.14/6.94 inference(contradiction_clause,[status(thm)],[f15661])).
% 50.14/6.95 fof(f15699,plain,(
% 50.14/6.95 ~k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))=sK1_skl|~sQ51_spl|sQ1_spl),
% 50.14/6.95 inference(forward_demodulation,[status(thm)],[f575,f334])).
% 50.14/6.95 fof(f15700,plain,(
% 50.14/6.95 ~k5_relat_1(sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))=sK1_skl|~sQ884_spl|~sQ51_spl|sQ1_spl),
% 50.14/6.95 inference(forward_demodulation,[status(thm)],[f7004,f15699])).
% 50.14/6.95 fof(f15784,definition,(
% 50.14/6.95 sQ1893_spl <=> (v1_funct_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1893_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15786,plain,(
% 50.14/6.95 ~v1_funct_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))))|sQ1893_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15784])).
% 50.14/6.95 fof(f15787,definition,(
% 50.14/6.95 sQ1894_spl <=> (m1_relset_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1894_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15789,plain,(
% 50.14/6.95 ~m1_relset_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)))|sQ1894_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15787])).
% 50.14/6.95 fof(f15794,definition,(
% 50.14/6.95 sQ1896_spl <=> (v1_funct_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1896_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15796,plain,(
% 50.14/6.95 ~v1_funct_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))))|sQ1896_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15794])).
% 50.14/6.95 fof(f15797,definition,(
% 50.14/6.95 sQ1897_spl <=> (m1_relset_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1897_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15799,plain,(
% 50.14/6.95 ~m1_relset_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)))|sQ1897_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15797])).
% 50.14/6.95 fof(f15805,plain,(
% 50.14/6.95 $false|sQ1897_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15799,f243])).
% 50.14/6.95 fof(f15806,plain,(
% 50.14/6.95 sQ1897_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f15805])).
% 50.14/6.95 fof(f15807,plain,(
% 50.14/6.95 $false|sQ1896_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15796,f245])).
% 50.14/6.95 fof(f15808,plain,(
% 50.14/6.95 sQ1896_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f15807])).
% 50.14/6.95 fof(f15809,plain,(
% 50.14/6.95 $false|sQ1894_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15789,f2060])).
% 50.14/6.95 fof(f15810,plain,(
% 50.14/6.95 sQ1894_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f15809])).
% 50.14/6.95 fof(f15811,plain,(
% 50.14/6.95 $false|sQ1893_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15786,f345])).
% 50.14/6.95 fof(f15812,plain,(
% 50.14/6.95 sQ1893_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f15811])).
% 50.14/6.95 fof(f15857,definition,(
% 50.14/6.95 sQ1908_spl <=> (v1_funct_1(k6_partfun1(u1_struct_0(sK12_skl))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1908_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15859,plain,(
% 50.14/6.95 ~v1_funct_1(k6_partfun1(u1_struct_0(sK12_skl)))|sQ1908_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15857])).
% 50.14/6.95 fof(f15860,definition,(
% 50.14/6.95 sQ1909_spl <=> (m1_relset_1(k6_partfun1(u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1909_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15862,plain,(
% 50.14/6.95 ~m1_relset_1(k6_partfun1(u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))|sQ1909_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15860])).
% 50.14/6.95 fof(f15867,definition,(
% 50.14/6.95 sQ1911_spl <=> (v1_funct_1(sK16_skl(u1_struct_0(sK12_skl))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1911_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15869,plain,(
% 50.14/6.95 ~v1_funct_1(sK16_skl(u1_struct_0(sK12_skl)))|sQ1911_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15867])).
% 50.14/6.95 fof(f15870,definition,(
% 50.14/6.95 sQ1912_spl <=> (m1_relset_1(sK16_skl(u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1912_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15872,plain,(
% 50.14/6.95 ~m1_relset_1(sK16_skl(u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))|sQ1912_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15870])).
% 50.14/6.95 fof(f15877,plain,(
% 50.14/6.95 $false|sQ1912_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15872,f243])).
% 50.14/6.95 fof(f15878,plain,(
% 50.14/6.95 sQ1912_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f15877])).
% 50.14/6.95 fof(f15879,plain,(
% 50.14/6.95 $false|sQ1911_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15869,f245])).
% 50.14/6.95 fof(f15880,plain,(
% 50.14/6.95 sQ1911_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f15879])).
% 50.14/6.95 fof(f15881,plain,(
% 50.14/6.95 $false|sQ1909_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15862,f2060])).
% 50.14/6.95 fof(f15882,plain,(
% 50.14/6.95 sQ1909_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f15881])).
% 50.14/6.95 fof(f15883,plain,(
% 50.14/6.95 $false|sQ1908_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15859,f345])).
% 50.14/6.95 fof(f15884,plain,(
% 50.14/6.95 sQ1908_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f15883])).
% 50.14/6.95 fof(f15964,definition,(
% 50.14/6.95 sQ1914_spl <=> (v1_funct_1(u1_group_1(sK17_skl)))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1914_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15966,plain,(
% 50.14/6.95 ~v1_funct_1(u1_group_1(sK17_skl))|sQ1914_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15964])).
% 50.14/6.95 fof(f15967,definition,(
% 50.14/6.95 sQ1915_spl <=> (m1_relset_1(u1_group_1(sK17_skl),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)),u1_struct_0(sK17_skl)))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ1915_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f15969,plain,(
% 50.14/6.95 ~m1_relset_1(u1_group_1(sK17_skl),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)),u1_struct_0(sK17_skl))|sQ1915_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f15967])).
% 50.14/6.95 fof(f16081,plain,(
% 50.14/6.95 $false|sQ1915_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15969,f15509])).
% 50.14/6.95 fof(f16082,plain,(
% 50.14/6.95 sQ1915_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f16081])).
% 50.14/6.95 fof(f16083,plain,(
% 50.14/6.95 $false|sQ1914_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f15966,f749])).
% 50.14/6.95 fof(f16084,plain,(
% 50.14/6.95 sQ1914_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f16083])).
% 50.14/6.95 fof(f17542,plain,(
% 50.14/6.95 m1_relset_1(u1_group_1(sK12_skl),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl))),
% 50.14/6.95 inference(resolution,[status(thm)],[f795,f298])).
% 50.14/6.95 fof(f17544,plain,(
% 50.14/6.95 $false|sQ427_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f17542,f3458])).
% 50.14/6.95 fof(f17545,plain,(
% 50.14/6.95 sQ427_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f17544])).
% 50.14/6.95 fof(f17590,definition,(
% 50.14/6.95 sQ2069_spl <=> (v1_relat_1(k5_relat_1(k5_relat_1(u1_group_1(sK0_skl),u1_group_1(sK0_skl)),k5_relat_1(u1_group_1(sK0_skl),u1_group_1(sK0_skl)))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ2069_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f17592,plain,(
% 50.14/6.95 ~v1_relat_1(k5_relat_1(k5_relat_1(u1_group_1(sK0_skl),u1_group_1(sK0_skl)),k5_relat_1(u1_group_1(sK0_skl),u1_group_1(sK0_skl))))|sQ2069_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f17590])).
% 50.14/6.95 fof(f17678,plain,(
% 50.14/6.95 $false|sQ2069_spl),
% 50.14/6.95 inference(forward_subsumption_resolution,[status(thm)],[f17592,f1066])).
% 50.14/6.95 fof(f17679,plain,(
% 50.14/6.95 sQ2069_spl),
% 50.14/6.95 inference(contradiction_clause,[status(thm)],[f17678])).
% 50.14/6.95 fof(f19466,plain,(
% 50.14/6.95 ![X0]: (k7_relset_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),X0,X0,sK1_skl,k6_partfun1(X0))=k5_relat_1(sK1_skl,k6_partfun1(X0))|~sQ43_spl)),
% 50.14/6.95 inference(resolution,[status(thm)],[f2813,f2057])).
% 50.14/6.95 fof(f19475,plain,(
% 50.14/6.95 k5_relat_1(sK1_skl,k6_partfun1(u1_struct_0(sK0_skl)))=sK1_skl|~sQ43_spl),
% 50.14/6.95 inference(backward_demodulation,[status(thm)],[f19466,f2185])).
% 50.14/6.95 fof(f19605,definition,(
% 50.14/6.95 sQ2227_spl <=> (v1_funct_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ2227_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f19607,plain,(
% 50.14/6.95 ~v1_funct_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))))|sQ2227_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f19605])).
% 50.14/6.95 fof(f19608,definition,(
% 50.14/6.95 sQ2228_spl <=> (m1_relset_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))))),
% 50.14/6.95 introduced(definition,[new_symbols(definition,[sQ2228_spl])],[split_symbol_definition])).
% 50.14/6.95 fof(f19610,plain,(
% 50.14/6.95 ~m1_relset_1(k6_partfun1(k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)))|sQ2228_spl),
% 50.14/6.95 inference(component_clause,[status(thm)],[f19608])).
% 50.14/6.96 fof(f19615,definition,(
% 50.14/6.96 sQ2230_spl <=> (v1_funct_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)))))),
% 50.14/6.96 introduced(definition,[new_symbols(definition,[sQ2230_spl])],[split_symbol_definition])).
% 50.14/6.96 fof(f19617,plain,(
% 50.14/6.96 ~v1_funct_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))))|sQ2230_spl),
% 50.14/6.96 inference(component_clause,[status(thm)],[f19615])).
% 50.14/6.96 fof(f19618,definition,(
% 50.14/6.96 sQ2231_spl <=> (m1_relset_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))))),
% 50.14/6.96 introduced(definition,[new_symbols(definition,[sQ2231_spl])],[split_symbol_definition])).
% 50.14/6.96 fof(f19620,plain,(
% 50.14/6.96 ~m1_relset_1(sK16_skl(k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)),k2_zfmisc_1(u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)))|sQ2231_spl),
% 50.14/6.96 inference(component_clause,[status(thm)],[f19618])).
% 50.14/6.96 fof(f19622,plain,(
% 50.14/6.96 $false|sQ2231_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19620,f243])).
% 50.14/6.96 fof(f19623,plain,(
% 50.14/6.96 sQ2231_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19622])).
% 50.14/6.96 fof(f19624,plain,(
% 50.14/6.96 $false|sQ2230_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19617,f245])).
% 50.14/6.96 fof(f19625,plain,(
% 50.14/6.96 sQ2230_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19624])).
% 50.14/6.96 fof(f19626,plain,(
% 50.14/6.96 $false|sQ2228_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19610,f2060])).
% 50.14/6.96 fof(f19627,plain,(
% 50.14/6.96 sQ2228_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19626])).
% 50.14/6.96 fof(f19628,plain,(
% 50.14/6.96 $false|sQ2227_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19607,f345])).
% 50.14/6.96 fof(f19629,plain,(
% 50.14/6.96 sQ2227_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19628])).
% 50.14/6.96 fof(f19676,definition,(
% 50.14/6.96 sQ2241_spl <=> (v1_funct_1(k6_partfun1(u1_struct_0(sK17_skl))))),
% 50.14/6.96 introduced(definition,[new_symbols(definition,[sQ2241_spl])],[split_symbol_definition])).
% 50.14/6.96 fof(f19678,plain,(
% 50.14/6.96 ~v1_funct_1(k6_partfun1(u1_struct_0(sK17_skl)))|sQ2241_spl),
% 50.14/6.96 inference(component_clause,[status(thm)],[f19676])).
% 50.14/6.96 fof(f19679,definition,(
% 50.14/6.96 sQ2242_spl <=> (m1_relset_1(k6_partfun1(u1_struct_0(sK17_skl)),u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)))),
% 50.14/6.96 introduced(definition,[new_symbols(definition,[sQ2242_spl])],[split_symbol_definition])).
% 50.14/6.96 fof(f19681,plain,(
% 50.14/6.96 ~m1_relset_1(k6_partfun1(u1_struct_0(sK17_skl)),u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))|sQ2242_spl),
% 50.14/6.96 inference(component_clause,[status(thm)],[f19679])).
% 50.14/6.96 fof(f19686,definition,(
% 50.14/6.96 sQ2244_spl <=> (v1_funct_1(sK16_skl(u1_struct_0(sK17_skl))))),
% 50.14/6.96 introduced(definition,[new_symbols(definition,[sQ2244_spl])],[split_symbol_definition])).
% 50.14/6.96 fof(f19688,plain,(
% 50.14/6.96 ~v1_funct_1(sK16_skl(u1_struct_0(sK17_skl)))|sQ2244_spl),
% 50.14/6.96 inference(component_clause,[status(thm)],[f19686])).
% 50.14/6.96 fof(f19689,definition,(
% 50.14/6.96 sQ2245_spl <=> (m1_relset_1(sK16_skl(u1_struct_0(sK17_skl)),u1_struct_0(sK17_skl),u1_struct_0(sK17_skl)))),
% 50.14/6.96 introduced(definition,[new_symbols(definition,[sQ2245_spl])],[split_symbol_definition])).
% 50.14/6.96 fof(f19691,plain,(
% 50.14/6.96 ~m1_relset_1(sK16_skl(u1_struct_0(sK17_skl)),u1_struct_0(sK17_skl),u1_struct_0(sK17_skl))|sQ2245_spl),
% 50.14/6.96 inference(component_clause,[status(thm)],[f19689])).
% 50.14/6.96 fof(f19693,plain,(
% 50.14/6.96 $false|sQ2245_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19691,f243])).
% 50.14/6.96 fof(f19694,plain,(
% 50.14/6.96 sQ2245_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19693])).
% 50.14/6.96 fof(f19695,plain,(
% 50.14/6.96 $false|sQ2244_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19688,f245])).
% 50.14/6.96 fof(f19696,plain,(
% 50.14/6.96 sQ2244_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19695])).
% 50.14/6.96 fof(f19697,plain,(
% 50.14/6.96 $false|sQ2242_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19681,f2060])).
% 50.14/6.96 fof(f19698,plain,(
% 50.14/6.96 sQ2242_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19697])).
% 50.14/6.96 fof(f19699,plain,(
% 50.14/6.96 $false|sQ2241_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19678,f345])).
% 50.14/6.96 fof(f19700,plain,(
% 50.14/6.96 sQ2241_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19699])).
% 50.14/6.96 fof(f19789,plain,(
% 50.14/6.96 ![X0]: (k7_relset_1(X0,X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k6_partfun1(X0),sK1_skl)=k5_relat_1(k6_partfun1(X0),sK1_skl)|~sQ43_spl)),
% 50.14/6.96 inference(resolution,[status(thm)],[f2815,f2057])).
% 50.14/6.96 fof(f19798,plain,(
% 50.14/6.96 k5_relat_1(k6_partfun1(u1_struct_0(sK0_skl)),sK1_skl)=sK1_skl|~sQ43_spl),
% 50.14/6.96 inference(backward_demodulation,[status(thm)],[f19789,f2181])).
% 50.14/6.96 fof(f19803,plain,(
% 50.14/6.96 $false|~sQ887_spl|~sQ51_spl|sQ0_spl|~sQ43_spl),
% 50.14/6.96 inference(forward_subsumption_resolution,[status(thm)],[f19798,f7057])).
% 50.14/6.96 fof(f19804,plain,(
% 50.14/6.96 ~sQ887_spl|~sQ51_spl|sQ0_spl|~sQ43_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19803])).
% 50.14/6.96 fof(f19805,plain,(
% 50.14/6.96 ~sK1_skl=sK1_skl|~sQ43_spl|~sQ884_spl|~sQ51_spl|sQ1_spl),
% 50.14/6.96 inference(forward_demodulation,[status(thm)],[f19475,f15700])).
% 50.14/6.96 fof(f19806,plain,(
% 50.14/6.96 $false|~sQ43_spl|~sQ884_spl|~sQ51_spl|sQ1_spl),
% 50.14/6.96 inference(trivial_equality_resolution,[status(thm)],[f19805])).
% 50.14/6.96 fof(f19807,plain,(
% 50.14/6.96 ~sQ43_spl|~sQ884_spl|~sQ51_spl|sQ1_spl),
% 50.14/6.96 inference(contradiction_clause,[status(thm)],[f19806])).
% 50.14/6.99 fof(f19808,plain,(
% 50.14/6.99 $false),
% 50.14/6.99 inference(sat_refutation,[status(thm)],[f335,f364,f380,f382,f404,f415,f428,f430,f432,f489,f499,f522,f536,f577,f1164,f1168,f1276,f1881,f1891,f2062,f3157,f3242,f3432,f3526,f3577,f3710,f3804,f3810,f3816,f4180,f4191,f4286,f4352,f4727,f4779,f5307,f5563,f5753,f5989,f6218,f6290,f7006,f7037,f7621,f8116,f8208,f8300,f8505,f8597,f9020,f10927,f10929,f10931,f12737,f15542,f15662,f15806,f15808,f15810,f15812,f15878,f15880,f15882,f15884,f16082,f16084,f17545,f17679,f19623,f19625,f19627,f19629,f19694,f19696,f19698,f19700,f19804,f19807])).
% 50.14/6.99 % SZS output end CNFRefutation for theBenchmark.p
% 39.62/7.06 % Elapsed time: 6.700763 seconds
% 39.62/7.06 % CPU time: 52.758607 seconds
% 39.62/7.06 % Total memory used: 695.884 MB
% 39.62/7.06 % Net memory used: 672.769 MB
%------------------------------------------------------------------------------