%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP620+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 : n008.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:55 PM UTC 2026
% Result : Theorem 0.14s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP620+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.12/0.36 % Computer : n008.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 20 20:18:55 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.14/0.60 % Refutation found
% 0.14/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.60 fof(f1,conjecture,(
% 0.14/0.60 (! [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),k1_autgroup(A))=> m2_fraenkel(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) ) )) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f2,negated_conjecture,(
% 0.14/0.60 ~((! [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),k1_autgroup(A))=> m2_fraenkel(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) ) )) ))),
% 0.14/0.60 inference(negated_conjecture,[status(cth)],[f1])).
% 0.14/0.60 fof(f15,axiom,(
% 0.14/0.60 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_fraenkel(B,u1_struct_0(A),u1_struct_0(A))=> ( B = k1_autgroup(A)<=> ( (! [C] :( m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)=> ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))& v1_group_6(C,A,A)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) ) ))& (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))& v1_group_6(C,A,A)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) )=> ( r2_hidden(C,B)<=> ( v2_funct_1(C)& v3_group_6(C,A,A) ) ) ) )) ) ) )) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f17,axiom,(
% 0.14/0.60 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f22,axiom,(
% 0.14/0.60 (! [A] :( l1_group_1(A)=> l1_struct_0(A) ) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f24,axiom,(
% 0.14/0.60 (! [A,B,C] :( m1_fraenkel(C,A,B)=> ( ~ v1_xboole_0(C)& v1_fraenkel(C) ) ) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f27,axiom,(
% 0.14/0.60 (! [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) ) ) )) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f39,axiom,(
% 0.14/0.60 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f57,axiom,(
% 0.14/0.60 (! [A,B,C] :( ( ~ v1_xboole_0(B)& m1_fraenkel(C,A,B) )=> (! [D] :( m2_fraenkel(D,A,B,C)<=> m1_subset_1(D,C) ) )) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f60,axiom,(
% 0.14/0.60 (! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f61,axiom,(
% 0.14/0.60 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f64,axiom,(
% 0.14/0.60 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( v1_funct_1(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v1_group_6(B,A,A)& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )=> ( r2_hidden(B,k1_autgroup(A))<=> v4_group_6(B,A,A) ) ) )) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f66,axiom,(
% 0.14/0.60 (! [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),k1_autgroup(A))=> ( v1_funct_1(k2_funct_1(B))& v1_funct_2(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A))& v1_group_6(k2_funct_1(B),A,A)& m2_relset_1(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A)) ) ) )) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f68,axiom,(
% 0.14/0.60 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))& v1_group_6(C,B,A)& m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) )=> (! [D] :( ( v1_funct_1(D)& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))& v1_group_6(D,A,B)& m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)) )=> ( ( v4_group_6(C,B,A)& D = k2_funct_1(C) )=> v4_group_6(D,A,B) ) ) )) )) )) )),
% 0.14/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.60 fof(f71,plain,(
% 0.14/0.60 (?[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),k1_autgroup(A))&~m2_fraenkel(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))))))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.60 fof(f72,plain,(
% 0.14/0.60 (((((~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),k1_autgroup(sK0_skl))&~m2_fraenkel(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))))),
% 0.14/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f71])).
% 0.14/0.60 fof(f73,plain,(
% 0.14/0.60 ~v3_struct_0(sK0_skl)),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.60 fof(f74,plain,(
% 0.14/0.60 v1_group_1(sK0_skl)),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.60 fof(f75,plain,(
% 0.14/0.60 v3_group_1(sK0_skl)),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.60 fof(f76,plain,(
% 0.14/0.60 v4_group_1(sK0_skl)),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.60 fof(f77,plain,(
% 0.14/0.60 l1_group_1(sK0_skl)),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.60 fof(f78,plain,(
% 0.14/0.60 m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.60 fof(f79,plain,(
% 0.14/0.60 ~m2_fraenkel(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.60 fof(f121,plain,(
% 0.14/0.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_fraenkel(B,u1_struct_0(A),u1_struct_0(A))|(B=k1_autgroup(A)<=>((![C]: (~m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)|(((v1_funct_1(C)&v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))&v1_group_6(C,A,A))&m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)))))&(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))|~v1_group_6(C,A,A))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)))|(r2_hidden(C,B)<=>(v2_funct_1(C)&v3_group_6(C,A,A))))))))))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.14/0.60 fof(f122,definition,(
% 0.14/0.60 ![A,B,C]: (sP0_prd(C,B,A)<=>(~m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)|(((v1_funct_1(C)&v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))&v1_group_6(C,A,A))&m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)))))),
% 0.14/0.60 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.14/0.60 fof(f123,plain,(
% 0.14/0.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_fraenkel(B,u1_struct_0(A),u1_struct_0(A))|(B=k1_autgroup(A)<=>((![C]: sP0_prd(C,B,A))&(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))|~v1_group_6(C,A,A))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)))|(r2_hidden(C,B)<=>(v2_funct_1(C)&v3_group_6(C,A,A))))))))))),
% 0.14/0.60 inference(formula_renaming,[status(thm)],[f121,f122])).
% 0.14/0.60 fof(f124,plain,(
% 0.14/0.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_fraenkel(B,u1_struct_0(A),u1_struct_0(A))|((~B=k1_autgroup(A)|((![C]: sP0_prd(C,B,A))&(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))|~v1_group_6(C,A,A))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)))|((~r2_hidden(C,B)|(v2_funct_1(C)&v3_group_6(C,A,A)))&(r2_hidden(C,B)|(~v2_funct_1(C)|~v3_group_6(C,A,A))))))))&(B=k1_autgroup(A)|((?[C]: ~sP0_prd(C,B,A))|(?[C]: ((((v1_funct_1(C)&v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))&v1_group_6(C,A,A))&m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)))&((~r2_hidden(C,B)|(~v2_funct_1(C)|~v3_group_6(C,A,A)))&(r2_hidden(C,B)|(v2_funct_1(C)&v3_group_6(C,A,A))))))))))))),
% 0.14/0.60 inference(NNF_transformation,[status(thm)],[f123])).
% 0.14/0.60 fof(f125,plain,(
% 0.14/0.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_fraenkel(B,u1_struct_0(A),u1_struct_0(A))|((~B=k1_autgroup(A)|((![C]: sP0_prd(C,B,A))&(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))|~v1_group_6(C,A,A))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)))|((~r2_hidden(C,B)|(v2_funct_1(C)&v3_group_6(C,A,A)))&(r2_hidden(C,B)|(~v2_funct_1(C)|~v3_group_6(C,A,A))))))))&(B=k1_autgroup(A)|(~sP0_prd(sK2_skl(B,A),B,A)|((((v1_funct_1(sK3_skl(B,A))&v1_funct_2(sK3_skl(B,A),u1_struct_0(A),u1_struct_0(A)))&v1_group_6(sK3_skl(B,A),A,A))&m2_relset_1(sK3_skl(B,A),u1_struct_0(A),u1_struct_0(A)))&((~r2_hidden(sK3_skl(B,A),B)|(~v2_funct_1(sK3_skl(B,A))|~v3_group_6(sK3_skl(B,A),A,A)))&(r2_hidden(sK3_skl(B,A),B)|(v2_funct_1(sK3_skl(B,A))&v3_group_6(sK3_skl(B,A),A,A)))))))))))),
% 0.14/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(C,sK2_skl(B,A)),skolemize(C,sK3_skl(B,A))],[f124])).
% 0.14/0.60 fof(f126,plain,(
% 0.14/0.60 ![X0,X1,X2]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))|~X1=k1_autgroup(X0)|sP0_prd(X2,X1,X0))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.60 fof(f140,plain,(
% 0.14/0.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A)))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.14/0.60 fof(f141,plain,(
% 0.14/0.60 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f140])).
% 0.14/0.60 fof(f145,plain,(
% 0.14/0.60 ![A]: (~l1_group_1(A)|l1_struct_0(A))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.14/0.60 fof(f146,plain,(
% 0.14/0.60 ![X0]: (~l1_group_1(X0)|l1_struct_0(X0))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f145])).
% 0.14/0.60 fof(f147,plain,(
% 0.14/0.60 ![A,B,C]: (~m1_fraenkel(C,A,B)|(~v1_xboole_0(C)&v1_fraenkel(C)))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.14/0.60 fof(f148,plain,(
% 0.14/0.60 ![C]: ((![A,B]: ~m1_fraenkel(C,A,B))|(~v1_xboole_0(C)&v1_fraenkel(C)))),
% 0.14/0.60 inference(miniscoping,[status(thm)],[f147])).
% 0.14/0.60 fof(f149,plain,(
% 0.14/0.60 ![X0,X1,X2]: (~m1_fraenkel(X0,X1,X2)|~v1_xboole_0(X0))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f148])).
% 0.14/0.60 fof(f151,plain,(
% 0.14/0.60 ![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)))))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.14/0.60 fof(f153,plain,(
% 0.14/0.60 ![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))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f151])).
% 0.14/0.60 fof(f154,plain,(
% 0.14/0.60 ![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))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f151])).
% 0.14/0.60 fof(f179,plain,(
% 0.14/0.60 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.14/0.60 fof(f180,plain,(
% 0.14/0.60 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f179])).
% 0.14/0.60 fof(f247,plain,(
% 0.14/0.60 ![A,B,C]: ((v1_xboole_0(B)|~m1_fraenkel(C,A,B))|(![D]: (m2_fraenkel(D,A,B,C)<=>m1_subset_1(D,C))))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.14/0.60 fof(f248,plain,(
% 0.14/0.60 ![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)))))),
% 0.14/0.60 inference(NNF_transformation,[status(thm)],[f247])).
% 0.14/0.60 fof(f249,plain,(
% 0.14/0.60 ![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)))))),
% 0.14/0.60 inference(miniscoping,[status(thm)],[f248])).
% 0.14/0.60 fof(f250,plain,(
% 0.14/0.60 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_fraenkel(X1,X2,X0)|~m2_fraenkel(X3,X2,X0,X1)|m1_subset_1(X3,X1))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f249])).
% 0.14/0.60 fof(f251,plain,(
% 0.14/0.60 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_fraenkel(X1,X2,X0)|m2_fraenkel(X3,X2,X0,X1)|~m1_subset_1(X3,X1))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f249])).
% 0.14/0.60 fof(f258,plain,(
% 0.14/0.60 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 0.14/0.60 fof(f259,plain,(
% 0.14/0.60 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f258])).
% 0.14/0.60 fof(f260,plain,(
% 0.14/0.60 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.14/0.60 fof(f261,plain,(
% 0.14/0.60 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f260])).
% 0.14/0.60 fof(f269,plain,(
% 0.14/0.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: ((((~v1_funct_1(B)|~v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))|~v1_group_6(B,A,A))|~m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)))|(r2_hidden(B,k1_autgroup(A))<=>v4_group_6(B,A,A)))))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.14/0.60 fof(f270,plain,(
% 0.14/0.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: ((((~v1_funct_1(B)|~v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))|~v1_group_6(B,A,A))|~m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)))|((~r2_hidden(B,k1_autgroup(A))|v4_group_6(B,A,A))&(r2_hidden(B,k1_autgroup(A))|~v4_group_6(B,A,A))))))),
% 0.14/0.60 inference(NNF_transformation,[status(thm)],[f269])).
% 0.14/0.60 fof(f271,plain,(
% 0.14/0.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v1_group_6(X1,X0,X0)|~m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|~r2_hidden(X1,k1_autgroup(X0))|v4_group_6(X1,X0,X0))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f270])).
% 0.14/0.60 fof(f272,plain,(
% 0.14/0.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v1_group_6(X1,X0,X0)|~m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|r2_hidden(X1,k1_autgroup(X0))|~v4_group_6(X1,X0,X0))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f270])).
% 0.14/0.60 fof(f276,plain,(
% 0.14/0.60 ![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),k1_autgroup(A))|(((v1_funct_1(k2_funct_1(B))&v1_funct_2(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A)))&v1_group_6(k2_funct_1(B),A,A))&m2_relset_1(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A))))))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 0.14/0.60 fof(f277,plain,(
% 0.14/0.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))|v1_funct_1(k2_funct_1(X1)))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f276])).
% 0.14/0.60 fof(f278,plain,(
% 0.14/0.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))|v1_funct_2(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0)))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f276])).
% 0.14/0.60 fof(f279,plain,(
% 0.14/0.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))|v1_group_6(k2_funct_1(X1),X0,X0))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f276])).
% 0.14/0.60 fof(f280,plain,(
% 0.14/0.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))|m2_relset_1(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0)))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f276])).
% 0.14/0.60 fof(f283,plain,(
% 0.14/0.60 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: ((((v3_struct_0(B)|~v3_group_1(B))|~v4_group_1(B))|~l1_group_1(B))|(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)))|~v1_group_6(C,B,A))|~m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)))|(![D]: ((((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(A),u1_struct_0(B)))|~v1_group_6(D,A,B))|~m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)))|((~v4_group_6(C,B,A)|~D=k2_funct_1(C))|v4_group_6(D,A,B)))))))))),
% 0.14/0.60 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.14/0.60 fof(f284,plain,(
% 0.14/0.60 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(X1)|~v3_group_1(X1)|~v4_group_1(X1)|~l1_group_1(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))|~v1_group_6(X2,X1,X0)|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v1_funct_1(X3)|~v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))|~v1_group_6(X3,X0,X1)|~m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))|~v4_group_6(X2,X1,X0)|~X3=k2_funct_1(X2)|v4_group_6(X3,X0,X1))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f283])).
% 0.14/0.60 fof(f291,plain,(
% 0.14/0.60 ![A,B,C]: ((~sP0_prd(C,B,A)|(~m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)|(((v1_funct_1(C)&v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))&v1_group_6(C,A,A))&m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)))))&(sP0_prd(C,B,A)|(m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)&(((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))|~v1_group_6(C,A,A))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))))))),
% 0.14/0.60 inference(NNF_transformation,[status(thm)],[f122])).
% 0.14/0.60 fof(f292,plain,(
% 0.14/0.60 (![A,B,C]: (~sP0_prd(C,B,A)|(~m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)|(((v1_funct_1(C)&v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))&v1_group_6(C,A,A))&m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))))))&(![A,B,C]: (sP0_prd(C,B,A)|(m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)&(((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)))|~v1_group_6(C,A,A))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))))))),
% 0.14/0.60 inference(miniscoping,[status(thm)],[f291])).
% 0.14/0.60 fof(f293,plain,(
% 0.14/0.60 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~m2_fraenkel(X0,u1_struct_0(X2),u1_struct_0(X2),X1)|v1_funct_1(X0))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f292])).
% 0.14/0.60 fof(f295,plain,(
% 0.14/0.60 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~m2_fraenkel(X0,u1_struct_0(X2),u1_struct_0(X2),X1)|v1_group_6(X0,X2,X2))),
% 0.14/0.60 inference(cnf_transformation,[status(thm)],[f292])).
% 0.14/0.60 fof(f301,plain,(
% 0.14/0.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))|sP0_prd(X1,k1_autgroup(X0),X0))),
% 0.14/0.60 inference(destructive_equality_resolution,[status(thm)],[f126])).
% 0.14/0.60 fof(f308,plain,(
% 0.14/0.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|sP0_prd(X1,k1_autgroup(X0),X0))),
% 0.14/0.60 inference(backward_subsumption_resolution,[status(thm)],[f301,f141])).
% 0.14/0.60 fof(f309,plain,(
% 0.14/0.60 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(X1)|~v3_group_1(X1)|~v4_group_1(X1)|~l1_group_1(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))|~v1_group_6(X2,X1,X0)|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v1_funct_1(k2_funct_1(X2))|~v1_funct_2(k2_funct_1(X2),u1_struct_0(X0),u1_struct_0(X1))|~v1_group_6(k2_funct_1(X2),X0,X1)|~m2_relset_1(k2_funct_1(X2),u1_struct_0(X0),u1_struct_0(X1))|~v4_group_6(X2,X1,X0)|v4_group_6(k2_funct_1(X2),X0,X1))),
% 0.14/0.60 inference(destructive_equality_resolution,[status(thm)],[f284])).
% 0.14/0.60 fof(f311,plain,(
% 0.14/0.60 ![X0,X1]: (v1_xboole_0(u1_struct_0(X0))|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))|v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0))),
% 0.14/0.60 inference(resolution,[status(thm)],[f153,f141])).
% 0.14/0.60 fof(f312,plain,(
% 0.14/0.60 ![X0,X1]: (v1_xboole_0(u1_struct_0(X0))|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))|m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0))),
% 0.14/0.60 inference(resolution,[status(thm)],[f154,f141])).
% 0.14/0.60 fof(f313,plain,(
% 0.14/0.60 ![X0]: (v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_1(k2_funct_1(X0)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f277,f75])).
% 0.14/0.60 fof(f316,plain,(
% 0.14/0.60 ![X0]: (~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_1(k2_funct_1(X0)))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f313,f73])).
% 0.14/0.60 fof(f319,plain,(
% 0.14/0.60 ![X0]: (v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f278,f75])).
% 0.14/0.60 fof(f322,plain,(
% 0.14/0.60 ![X0]: (~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f319,f73])).
% 0.14/0.60 fof(f333,plain,(
% 0.14/0.60 ![X0]: (~v1_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_1(k2_funct_1(X0)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f316,f76])).
% 0.14/0.60 fof(f335,plain,(
% 0.14/0.60 ![X0]: (~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_1(k2_funct_1(X0)))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f333,f74])).
% 0.14/0.60 fof(f337,plain,(
% 0.14/0.60 ![X0]: (~v1_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f322,f76])).
% 0.14/0.60 fof(f339,plain,(
% 0.14/0.60 ![X0]: (~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f337,f74])).
% 0.14/0.60 fof(f341,plain,(
% 0.14/0.60 ![X0]: (~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_1(k2_funct_1(X0)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f335,f77])).
% 0.14/0.60 fof(f342,plain,(
% 0.14/0.60 ![X0]: (~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f339,f77])).
% 0.14/0.60 fof(f343,plain,(
% 0.14/0.60 ![X0]: (v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_group_6(k2_funct_1(X0),sK0_skl,sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f279,f75])).
% 0.14/0.60 fof(f345,plain,(
% 0.14/0.60 ![X0]: (~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_group_6(k2_funct_1(X0),sK0_skl,sK0_skl))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f343,f73])).
% 0.14/0.60 fof(f347,plain,(
% 0.14/0.60 ![X0]: (v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f280,f75])).
% 0.14/0.60 fof(f349,plain,(
% 0.14/0.60 ![X0]: (~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f347,f73])).
% 0.14/0.60 fof(f355,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f311,f75])).
% 0.14/0.60 fof(f357,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f355,f73])).
% 0.14/0.60 fof(f359,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f312,f75])).
% 0.14/0.60 fof(f361,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f359,f73])).
% 0.14/0.60 fof(f381,plain,(
% 0.14/0.60 v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f342,f78])).
% 0.14/0.60 fof(f382,plain,(
% 0.14/0.60 ![X0]: (~v1_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_group_6(k2_funct_1(X0),sK0_skl,sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f345,f76])).
% 0.14/0.60 fof(f384,plain,(
% 0.14/0.60 ![X0]: (~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_group_6(k2_funct_1(X0),sK0_skl,sK0_skl))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f382,f74])).
% 0.14/0.60 fof(f386,plain,(
% 0.14/0.60 ![X0]: (~v1_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f349,f76])).
% 0.14/0.60 fof(f388,plain,(
% 0.14/0.60 ![X0]: (~l1_group_1(sK0_skl)|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f386,f74])).
% 0.14/0.60 fof(f395,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_1(sK0_skl)|~l1_group_1(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f357,f76])).
% 0.14/0.60 fof(f397,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~l1_group_1(sK0_skl))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f395,f74])).
% 0.14/0.60 fof(f399,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_1(sK0_skl)|~l1_group_1(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f361,f76])).
% 0.14/0.60 fof(f401,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~l1_group_1(sK0_skl))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f399,f74])).
% 0.14/0.60 fof(f403,plain,(
% 0.14/0.60 ![X0]: (~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(k2_funct_1(X0),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f388,f77])).
% 0.14/0.60 fof(f440,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|~m1_fraenkel(k1_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|m1_subset_1(sK1_skl,k1_autgroup(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f250,f78])).
% 0.14/0.60 fof(f447,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_funct_2(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f397,f77])).
% 0.14/0.60 fof(f448,plain,(
% 0.14/0.60 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|m2_relset_1(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.14/0.60 inference(resolution,[status(thm)],[f401,f77])).
% 0.14/0.60 fof(f449,plain,(
% 0.14/0.60 m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f403,f78])).
% 0.14/0.60 fof(f450,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|m1_subset_1(sK1_skl,k1_autgroup(sK0_skl))|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)),
% 0.14/0.60 inference(resolution,[status(thm)],[f440,f141])).
% 0.14/0.60 fof(f451,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|m1_subset_1(sK1_skl,k1_autgroup(sK0_skl))|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f450,f73])).
% 0.14/0.60 fof(f452,plain,(
% 0.14/0.60 ![X0]: (~m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|v1_group_6(k2_funct_1(X0),sK0_skl,sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f384,f77])).
% 0.14/0.60 fof(f458,plain,(
% 0.14/0.60 ~sP0_prd(sK1_skl,k1_autgroup(sK0_skl),sK0_skl)|v1_funct_1(sK1_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f293,f78])).
% 0.14/0.60 fof(f460,plain,(
% 0.14/0.60 ~sP0_prd(sK1_skl,k1_autgroup(sK0_skl),sK0_skl)|v1_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f295,f78])).
% 0.14/0.60 fof(f489,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f447,f78])).
% 0.14/0.60 fof(f491,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f448,f78])).
% 0.14/0.60 fof(f493,plain,(
% 0.14/0.60 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f449,f309])).
% 0.14/0.60 fof(f494,plain,(
% 0.14/0.60 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(duplicate_literals_removal,[status(thm)],[f493])).
% 0.14/0.60 fof(f495,plain,(
% 0.14/0.60 ~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f494,f73])).
% 0.14/0.60 fof(f496,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|m1_subset_1(sK1_skl,k1_autgroup(sK0_skl))|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f451,f75])).
% 0.14/0.60 fof(f499,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|m1_subset_1(sK1_skl,k1_autgroup(sK0_skl))|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f496,f74])).
% 0.14/0.60 fof(f502,plain,(
% 0.14/0.60 v1_funct_1(sK1_skl)|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)),
% 0.14/0.60 inference(resolution,[status(thm)],[f458,f308])).
% 0.14/0.60 fof(f503,plain,(
% 0.14/0.60 v1_funct_1(sK1_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f502,f73])).
% 0.14/0.60 fof(f532,plain,(
% 0.14/0.60 v1_group_6(sK1_skl,sK0_skl,sK0_skl)|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)),
% 0.14/0.60 inference(resolution,[status(thm)],[f460,f308])).
% 0.14/0.60 fof(f533,plain,(
% 0.14/0.60 v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f532,f73])).
% 0.14/0.60 fof(f572,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|m1_subset_1(sK1_skl,k1_autgroup(sK0_skl))|~v4_group_1(sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f499,f77])).
% 0.14/0.60 fof(f573,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|m1_subset_1(sK1_skl,k1_autgroup(sK0_skl))),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f572,f76])).
% 0.14/0.60 fof(f574,plain,(
% 0.14/0.60 v1_funct_1(sK1_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f503,f75])).
% 0.14/0.60 fof(f577,plain,(
% 0.14/0.60 ~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(backward_subsumption_resolution,[status(thm)],[f495,f578])).
% 0.14/0.60 fof(f578,plain,(
% 0.14/0.60 v1_funct_1(sK1_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f574,f74])).
% 0.14/0.60 fof(f581,plain,(
% 0.14/0.60 ~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f577,f75])).
% 0.14/0.60 fof(f582,plain,(
% 0.14/0.60 v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f533,f75])).
% 0.14/0.60 fof(f585,plain,(
% 0.14/0.60 ~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_2(sK1_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))|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(backward_subsumption_resolution,[status(thm)],[f581,f586])).
% 0.14/0.60 fof(f586,plain,(
% 0.14/0.60 v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f582,f74])).
% 0.14/0.60 fof(f589,plain,(
% 0.14/0.60 ~l1_group_1(sK0_skl)|~v1_funct_2(sK1_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))|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f585,f76])).
% 0.14/0.60 fof(f590,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|r2_hidden(sK1_skl,k1_autgroup(sK0_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f573,f261])).
% 0.14/0.60 fof(f598,plain,(
% 0.14/0.60 v1_funct_1(sK1_skl)|~v4_group_1(sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f578,f77])).
% 0.14/0.60 fof(f599,plain,(
% 0.14/0.60 v1_funct_1(sK1_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f598,f76])).
% 0.14/0.60 fof(f600,plain,(
% 0.14/0.60 v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~v4_group_1(sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f586,f77])).
% 0.14/0.60 fof(f601,plain,(
% 0.14/0.60 v1_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f600,f76])).
% 0.14/0.60 fof(f602,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f590,f271])).
% 0.14/0.60 fof(f608,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f602,f73])).
% 0.14/0.60 fof(f634,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f608,f75])).
% 0.14/0.60 fof(f637,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f634,f74])).
% 0.14/0.60 fof(f646,plain,(
% 0.14/0.60 v1_funct_1(k2_funct_1(sK1_skl))),
% 0.14/0.60 inference(resolution,[status(thm)],[f341,f78])).
% 0.14/0.60 fof(f648,plain,(
% 0.14/0.60 ~l1_group_1(sK0_skl)|~v1_funct_2(sK1_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))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(backward_subsumption_resolution,[status(thm)],[f589,f646])).
% 0.14/0.60 fof(f649,plain,(
% 0.14/0.60 ~v1_funct_2(sK1_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))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.60 inference(forward_subsumption_resolution,[status(thm)],[f648,f77])).
% 0.14/0.60 fof(f650,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v4_group_1(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.60 inference(resolution,[status(thm)],[f637,f77])).
% 0.14/0.60 fof(f651,plain,(
% 0.14/0.60 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v1_group_6(sK1_skl,sK0_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.61 inference(forward_subsumption_resolution,[status(thm)],[f650,f76])).
% 0.14/0.61 fof(f654,plain,(
% 0.14/0.61 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_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))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.61 inference(resolution,[status(thm)],[f651,f601])).
% 0.14/0.61 fof(f655,plain,(
% 0.14/0.61 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_funct_2(sK1_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))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.61 inference(forward_subsumption_resolution,[status(thm)],[f654,f599])).
% 0.14/0.61 fof(f662,plain,(
% 0.14/0.61 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v1_xboole_0(u1_struct_0(sK0_skl))),
% 0.14/0.61 inference(resolution,[status(thm)],[f655,f491])).
% 0.14/0.61 fof(f664,plain,(
% 0.14/0.61 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.61 inference(duplicate_literals_removal,[status(thm)],[f662])).
% 0.14/0.61 fof(f665,plain,(
% 0.14/0.61 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|v4_group_6(sK1_skl,sK0_skl,sK0_skl)),
% 0.14/0.61 inference(forward_subsumption_resolution,[status(thm)],[f664,f489])).
% 0.14/0.61 fof(f687,plain,(
% 0.14/0.61 l1_struct_0(sK0_skl)),
% 0.14/0.61 inference(resolution,[status(thm)],[f146,f77])).
% 0.14/0.61 fof(f692,plain,(
% 0.14/0.61 v1_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.61 inference(resolution,[status(thm)],[f452,f78])).
% 0.14/0.61 fof(f694,plain,(
% 0.14/0.61 ~v1_funct_2(sK1_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))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.61 inference(backward_subsumption_resolution,[status(thm)],[f649,f692])).
% 0.14/0.61 fof(f695,plain,(
% 0.14/0.61 ~v1_funct_2(sK1_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))|~v4_group_6(sK1_skl,sK0_skl,sK0_skl)|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.61 inference(forward_subsumption_resolution,[status(thm)],[f694,f381])).
% 0.14/0.61 fof(f701,plain,(
% 0.14/0.61 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)|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))|~v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.61 inference(resolution,[status(thm)],[f692,f272])).
% 0.14/0.61 fof(f711,plain,(
% 0.14/0.61 ~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))|~v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)),
% 0.14/0.61 inference(forward_subsumption_resolution,[status(thm)],[f701,f73])).
% 0.14/0.61 fof(f712,plain,(
% 0.14/0.61 ~v1_funct_2(sK1_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))|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))),
% 0.14/0.61 inference(resolution,[status(thm)],[f695,f665])).
% 0.14/0.61 fof(f713,plain,(
% 0.14/0.61 ~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))),
% 0.14/0.61 inference(forward_subsumption_resolution,[status(thm)],[f712,f489])).
% 0.14/0.61 fof(f714,plain,(
% 0.14/0.61 v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|v1_xboole_0(u1_struct_0(sK0_skl))),
% 0.14/0.61 inference(resolution,[status(thm)],[f713,f491])).
% 0.14/0.61 fof(f716,plain,(
% 0.14/0.61 v4_group_6(k2_funct_1(sK1_skl),sK0_skl,sK0_skl)|v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))),
% 0.14/0.61 inference(duplicate_literals_removal,[status(thm)],[f714])).
% 0.14/0.61 fof(f717,plain,(
% 0.14/0.61 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.61 inference(resolution,[status(thm)],[f716,f711])).
% 0.14/0.61 fof(f720,plain,(
% 0.14/0.61 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f717,f74])).
% 0.14/0.62 fof(f723,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.62 inference(resolution,[status(thm)],[f720,f77])).
% 0.14/0.62 fof(f724,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v4_group_1(sK0_skl)|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f723,f75])).
% 0.14/0.62 fof(f739,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_funct_1(k2_funct_1(sK1_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.62 inference(resolution,[status(thm)],[f724,f76])).
% 0.14/0.62 fof(f740,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f739,f646])).
% 0.14/0.62 fof(f753,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|~v1_funct_2(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.62 inference(resolution,[status(thm)],[f740,f449])).
% 0.14/0.62 fof(f754,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|r2_hidden(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f753,f381])).
% 0.14/0.62 fof(f782,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|m1_subset_1(k2_funct_1(sK1_skl),k1_autgroup(sK0_skl))),
% 0.14/0.62 inference(resolution,[status(thm)],[f754,f259])).
% 0.14/0.62 fof(f793,plain,(
% 0.14/0.62 ![X0,X1]: (v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(k1_autgroup(sK0_skl))|v1_xboole_0(X0)|~m1_fraenkel(k1_autgroup(sK0_skl),X1,X0)|m2_fraenkel(k2_funct_1(sK1_skl),X1,X0,k1_autgroup(sK0_skl)))),
% 0.14/0.62 inference(resolution,[status(thm)],[f782,f251])).
% 0.14/0.62 fof(f795,plain,(
% 0.14/0.62 ![X0,X1]: (v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(X0)|~m1_fraenkel(k1_autgroup(sK0_skl),X1,X0)|m2_fraenkel(k2_funct_1(sK1_skl),X1,X0,k1_autgroup(sK0_skl)))),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f793,f149])).
% 0.14/0.62 fof(f983,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v1_xboole_0(u1_struct_0(sK0_skl))|m2_fraenkel(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|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)),
% 0.14/0.62 inference(resolution,[status(thm)],[f795,f141])).
% 0.14/0.62 fof(f984,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|m2_fraenkel(k2_funct_1(sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|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)),
% 0.14/0.62 inference(duplicate_literals_removal,[status(thm)],[f983])).
% 0.14/0.62 fof(f985,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|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)),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f984,f79])).
% 0.14/0.62 fof(f986,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.62 inference(resolution,[status(thm)],[f985,f75])).
% 0.14/0.62 fof(f989,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|~v1_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f986,f73])).
% 0.14/0.62 fof(f993,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|~v1_group_1(sK0_skl)|~l1_group_1(sK0_skl)),
% 0.14/0.62 inference(resolution,[status(thm)],[f989,f76])).
% 0.14/0.62 fof(f995,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))|~l1_group_1(sK0_skl)),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f993,f74])).
% 0.14/0.62 fof(f997,plain,(
% 0.14/0.62 v1_xboole_0(u1_struct_0(sK0_skl))),
% 0.14/0.62 inference(resolution,[status(thm)],[f995,f77])).
% 0.14/0.62 fof(f998,plain,(
% 0.14/0.62 v3_struct_0(sK0_skl)|~l1_struct_0(sK0_skl)),
% 0.14/0.62 inference(resolution,[status(thm)],[f997,f180])).
% 0.14/0.62 fof(f1003,plain,(
% 0.14/0.62 ~l1_struct_0(sK0_skl)),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f998,f73])).
% 0.14/0.62 fof(f1004,plain,(
% 0.14/0.62 $false),
% 0.14/0.62 inference(backward_subsumption_resolution,[status(thm)],[f687,f1003])).
% 0.14/0.62 % SZS output end CNFRefutation for theBenchmark.p
% 1.30/0.64 % Elapsed time: 0.261004 seconds
% 1.30/0.64 % CPU time: 1.729979 seconds
% 1.30/0.64 % Total memory used: 121.265 MB
% 1.30/0.64 % Net memory used: 120.233 MB
%------------------------------------------------------------------------------