%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP041+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 : n018.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 03:53:45 PM UTC 2026
% Result : Theorem 54.44s 7.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP041+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.11/0.51 % Computer : n018.cluster.edu
% 0.11/0.51 % Model : x86_64 x86_64
% 0.11/0.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.51 % Memory : 8046.5625MB
% 0.11/0.51 % OS : Linux 6.8.0-71-generic
% 0.11/0.51 % CPULimit : 300
% 0.11/0.51 % WCLimit : 300
% 0.11/0.51 % DateTime : Mon Sep 21 12:46:44 UTC 2026
% 0.11/0.51 % CPUTime :
% 0.11/0.53 % Drodi V4.1.1
% 54.44/7.50 % Refutation found
% 54.44/7.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 54.44/7.50 % SZS output start CNFRefutation for theBenchmark
% 54.44/7.50 fof(f1,conjecture,(
% 54.44/7.50 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_tsp_2(B,A)& m2_tsp_1(B,A) )=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> ( v3_pre_topc(C,A)=> v3_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) )) )) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f2,negated_conjecture,(
% 54.44/7.50 ~((! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_tsp_2(B,A)& m2_tsp_1(B,A) )=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> ( v3_pre_topc(C,A)=> v3_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) )) )) ))),
% 54.44/7.50 inference(negated_conjecture,[status(cth)],[f1])).
% 54.44/7.50 fof(f50,axiom,(
% 54.44/7.50 (! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f52,axiom,(
% 54.44/7.50 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_tsp_2(B,A)& m2_tsp_1(B,A) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& v5_pre_topc(C,A,B)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( C = k4_tsp_2(A,B)<=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))=> ( D = u1_struct_0(B)=> (! [E] :( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))=> k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E)) = k4_pre_topc(A,B,C,E) ) )) ) )) ) )) )) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f53,axiom,(
% 54.44/7.50 (! [A] :( l1_pre_topc(A)=> (! [B] :( l1_pre_topc(B)=> ( m1_tsp_1(B,A)<=> ( r1_tarski(u1_struct_0(B),u1_struct_0(A))& (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))=> ( v3_pre_topc(C,B)<=> (? [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))& v3_pre_topc(D,A)& C = k3_xboole_0(D,u1_struct_0(B)) ) )) ) )) ) ) )) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f54,axiom,(
% 54.44/7.50 (! [A,B] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A)& ~ v3_struct_0(B)& v2_tsp_2(B,A)& m1_pre_topc(B,A) )=> ( v1_funct_1(k1_tsp_2(A,B))& v1_funct_2(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))& v5_pre_topc(k1_tsp_2(A,B),A,B)& m2_relset_1(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B)) ) ) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f58,axiom,(
% 54.44/7.50 (! [A,B] :( ( ~ v3_struct_0(A)& l1_pre_topc(A)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> m1_subset_1(k3_tex_4(A,B),k1_zfmisc_1(u1_struct_0(A))) ) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f60,axiom,(
% 54.44/7.50 (! [A,B,C,D] :( ( l1_struct_0(A)& l1_struct_0(B)& v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> m1_subset_1(k4_pre_topc(A,B,C,D),k1_zfmisc_1(u1_struct_0(B))) ) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f61,axiom,(
% 54.44/7.50 (! [A,B] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A)& ~ v3_struct_0(B)& v2_tsp_2(B,A)& m1_pre_topc(B,A) )=> ( v1_funct_1(k4_tsp_2(A,B))& v1_funct_2(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))& v5_pre_topc(k4_tsp_2(A,B),A,B)& m2_relset_1(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B)) ) ) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f64,axiom,(
% 54.44/7.50 (! [A] :( l1_pre_topc(A)=> l1_struct_0(A) ) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f69,axiom,(
% 54.44/7.50 (! [A] :( l1_pre_topc(A)=> (! [B] :( m1_tsp_1(B,A)=> l1_pre_topc(B) ) )) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f71,axiom,(
% 54.44/7.50 (! [A] :( l1_pre_topc(A)=> (! [B] :( m2_tsp_1(B,A)=> l1_pre_topc(B) ) )) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f73,axiom,(
% 54.44/7.50 (? [A] : l1_pre_topc(A) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f77,axiom,(
% 54.44/7.50 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.50 fof(f97,axiom,(
% 54.44/7.50 (? [A] :( ~ v1_xboole_0(A)& v1_membered(A)& v2_membered(A)& v3_membered(A)& v4_membered(A)& v5_membered(A) ) )),
% 54.44/7.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f100,axiom,(
% 54.44/7.51 (! [A] :(? [B] :( m1_subset_1(B,k1_zfmisc_1(A))& v1_xboole_0(B) ) ))),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f102,axiom,(
% 54.44/7.51 (? [A] :( l1_struct_0(A)& ~ v3_struct_0(A) ) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f109,axiom,(
% 54.44/7.51 (! [A,B,C,D] :( ( l1_struct_0(A)& l1_struct_0(B)& v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> k4_pre_topc(A,B,C,D) = k9_relat_1(C,D) ) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f110,axiom,(
% 54.44/7.51 (! [A,B] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A)& ~ v3_struct_0(B)& v2_tsp_2(B,A)& m1_pre_topc(B,A) )=> k4_tsp_2(A,B) = k1_tsp_2(A,B) ) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f111,axiom,(
% 54.44/7.51 (! [A,B,C] :( ( m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> k5_subset_1(A,B,C) = k3_xboole_0(B,C) ) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f112,axiom,(
% 54.44/7.51 (! [A] :( l1_pre_topc(A)=> (! [B] :( m1_tsp_1(B,A)<=> m1_pre_topc(B,A) ) )) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f113,axiom,(
% 54.44/7.51 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f114,axiom,(
% 54.44/7.51 (! [A] :( l1_pre_topc(A)=> (! [B] :( m2_tsp_1(B,A)<=> m1_pre_topc(B,A) ) )) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f115,axiom,(
% 54.44/7.51 (! [A,B] : r1_tarski(A,A) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f117,axiom,(
% 54.44/7.51 (! [A] :( l1_pre_topc(A)=> (! [B] :( m1_pre_topc(B,A)=> m1_subset_1(u1_struct_0(B),k1_zfmisc_1(u1_struct_0(A))) ) )) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f120,axiom,(
% 54.44/7.51 (! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f122,axiom,(
% 54.44/7.51 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( v3_pre_topc(B,A)=> k3_tex_4(A,B) = B ) ) )) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f124,axiom,(
% 54.44/7.51 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 54.44/7.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 54.44/7.51 fof(f127,plain,(
% 54.44/7.51 (?[A]: (((~v3_struct_0(A)&v2_pre_topc(A))&l1_pre_topc(A))&(?[B]: (((~v3_struct_0(B)&v2_tsp_2(B,A))&m2_tsp_1(B,A))&(?[C]: (m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))&(v3_pre_topc(C,A)&~v3_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B))))))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 54.44/7.51 fof(f128,plain,(
% 54.44/7.51 (((~v3_struct_0(sK0_skl)&v2_pre_topc(sK0_skl))&l1_pre_topc(sK0_skl))&(((~v3_struct_0(sK1_skl)&v2_tsp_2(sK1_skl,sK0_skl))&m2_tsp_1(sK1_skl,sK0_skl))&(m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))&(v3_pre_topc(sK2_skl,sK0_skl)&~v3_pre_topc(k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),sK2_skl),sK1_skl)))))),
% 54.44/7.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f127])).
% 54.44/7.51 fof(f129,plain,(
% 54.44/7.51 ~v3_struct_0(sK0_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f130,plain,(
% 54.44/7.51 v2_pre_topc(sK0_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f131,plain,(
% 54.44/7.51 l1_pre_topc(sK0_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f132,plain,(
% 54.44/7.51 ~v3_struct_0(sK1_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f133,plain,(
% 54.44/7.51 v2_tsp_2(sK1_skl,sK0_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f134,plain,(
% 54.44/7.51 m2_tsp_1(sK1_skl,sK0_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f135,plain,(
% 54.44/7.51 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f136,plain,(
% 54.44/7.51 v3_pre_topc(sK2_skl,sK0_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f137,plain,(
% 54.44/7.51 ~v3_pre_topc(k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),sK2_skl),sK1_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f128])).
% 54.44/7.51 fof(f318,plain,(
% 54.44/7.51 ![X0,X1]: (k3_xboole_0(X0,X1)=k3_xboole_0(X1,X0))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f50])).
% 54.44/7.51 fof(f321,plain,(
% 54.44/7.51 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: (((v3_struct_0(B)|~v2_tsp_2(B,A))|~m2_tsp_1(B,A))|(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~v5_pre_topc(C,A,B))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(C=k4_tsp_2(A,B)<=>(![D]: (~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))|(~D=u1_struct_0(B)|(![E]: (~m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))|k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E))=k4_pre_topc(A,B,C,E))))))))))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 54.44/7.51 fof(f322,plain,(
% 54.44/7.51 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: (((v3_struct_0(B)|~v2_tsp_2(B,A))|~m2_tsp_1(B,A))|(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~v5_pre_topc(C,A,B))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|((~C=k4_tsp_2(A,B)|(![D]: (~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))|(~D=u1_struct_0(B)|(![E]: (~m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))|k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E))=k4_pre_topc(A,B,C,E)))))))&(C=k4_tsp_2(A,B)|(?[D]: (m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&(D=u1_struct_0(B)&(?[E]: (m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))&~k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E))=k4_pre_topc(A,B,C,E)))))))))))))),
% 54.44/7.51 inference(NNF_transformation,[status(thm)],[f321])).
% 54.44/7.51 fof(f323,plain,(
% 54.44/7.51 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: (((v3_struct_0(B)|~v2_tsp_2(B,A))|~m2_tsp_1(B,A))|(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~v5_pre_topc(C,A,B))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|((~C=k4_tsp_2(A,B)|(![D]: (~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))|(~D=u1_struct_0(B)|(![E]: (~m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))|k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E))=k4_pre_topc(A,B,C,E)))))))&(C=k4_tsp_2(A,B)|(m1_subset_1(sK3_skl(C,B,A),k1_zfmisc_1(u1_struct_0(A)))&(sK3_skl(C,B,A)=u1_struct_0(B)&(m1_subset_1(sK4_skl(C,B,A),k1_zfmisc_1(u1_struct_0(A)))&~k5_subset_1(u1_struct_0(A),sK3_skl(C,B,A),k3_tex_4(A,sK4_skl(C,B,A)))=k4_pre_topc(A,B,C,sK4_skl(C,B,A))))))))))))),
% 54.44/7.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(D,sK3_skl(C,B,A)),skolemize(E,sK4_skl(C,B,A))],[f322])).
% 54.44/7.51 fof(f324,plain,(
% 54.44/7.51 ![X0,X1,X2,X3,X4]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|~m2_tsp_1(X1,X0)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(X2,X0,X1)|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~X2=k4_tsp_2(X0,X1)|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))|~X3=u1_struct_0(X1)|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))|k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4))=k4_pre_topc(X0,X1,X2,X4))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f323])).
% 54.44/7.51 fof(f329,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|(m1_tsp_1(B,A)<=>(r1_tarski(u1_struct_0(B),u1_struct_0(A))&(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|(v3_pre_topc(C,B)<=>(?[D]: ((m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&v3_pre_topc(D,A))&C=k3_xboole_0(D,u1_struct_0(B))))))))))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 54.44/7.51 fof(f330,definition,(
% 54.44/7.51 ![A,B,C,D]: (sP0_prd(D,C,B,A)<=>((m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&v3_pre_topc(D,A))&C=k3_xboole_0(D,u1_struct_0(B))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 54.44/7.51 fof(f331,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|(m1_tsp_1(B,A)<=>(r1_tarski(u1_struct_0(B),u1_struct_0(A))&(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|(v3_pre_topc(C,B)<=>(?[D]: sP0_prd(D,C,B,A))))))))))),
% 54.44/7.51 inference(formula_renaming,[status(thm)],[f329,f330])).
% 54.44/7.51 fof(f332,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|((~m1_tsp_1(B,A)|(r1_tarski(u1_struct_0(B),u1_struct_0(A))&(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|((~v3_pre_topc(C,B)|(?[D]: sP0_prd(D,C,B,A)))&(v3_pre_topc(C,B)|(![D]: ~sP0_prd(D,C,B,A))))))))&(m1_tsp_1(B,A)|(~r1_tarski(u1_struct_0(B),u1_struct_0(A))|(?[C]: (m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))&((~v3_pre_topc(C,B)|(![D]: ~sP0_prd(D,C,B,A)))&(v3_pre_topc(C,B)|(?[D]: sP0_prd(D,C,B,A))))))))))))),
% 54.44/7.51 inference(NNF_transformation,[status(thm)],[f331])).
% 54.44/7.51 fof(f333,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|((~m1_tsp_1(B,A)|(r1_tarski(u1_struct_0(B),u1_struct_0(A))&(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|((~v3_pre_topc(C,B)|sP0_prd(sK5_skl(C,B,A),C,B,A))&(v3_pre_topc(C,B)|(![D]: ~sP0_prd(D,C,B,A))))))))&(m1_tsp_1(B,A)|(~r1_tarski(u1_struct_0(B),u1_struct_0(A))|(m1_subset_1(sK6_skl(B,A),k1_zfmisc_1(u1_struct_0(B)))&((~v3_pre_topc(sK6_skl(B,A),B)|(![D]: ~sP0_prd(D,sK6_skl(B,A),B,A)))&(v3_pre_topc(sK6_skl(B,A),B)|sP0_prd(sK7_skl(B,A),sK6_skl(B,A),B,A))))))))))),
% 54.44/7.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl,sK7_skl]),skolemize(D,sK5_skl(C,B,A)),skolemize(C,sK6_skl(B,A)),skolemize(D,sK7_skl(B,A))],[f332])).
% 54.44/7.51 fof(f336,plain,(
% 54.44/7.51 ![X0,X1,X2,X3]: (~l1_pre_topc(X0)|~l1_pre_topc(X1)|~m1_tsp_1(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|v3_pre_topc(X2,X1)|~sP0_prd(X3,X2,X1,X0))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f333])).
% 54.44/7.51 fof(f340,plain,(
% 54.44/7.51 ![A,B]: ((((((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|v3_struct_0(B))|~v2_tsp_2(B,A))|~m1_pre_topc(B,A))|(((v1_funct_1(k1_tsp_2(A,B))&v1_funct_2(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B)))&v5_pre_topc(k1_tsp_2(A,B),A,B))&m2_relset_1(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 54.44/7.51 fof(f342,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|~m1_pre_topc(X1,X0)|v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f340])).
% 54.44/7.51 fof(f343,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|~m1_pre_topc(X1,X0)|v5_pre_topc(k1_tsp_2(X0,X1),X0,X1))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f340])).
% 54.44/7.51 fof(f344,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|~m1_pre_topc(X1,X0)|m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f340])).
% 54.44/7.51 fof(f345,plain,(
% 54.44/7.51 ![A,B]: (((v3_struct_0(A)|~l1_pre_topc(A))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|m1_subset_1(k3_tex_4(A,B),k1_zfmisc_1(u1_struct_0(A))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 54.44/7.51 fof(f346,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f345])).
% 54.44/7.51 fof(f347,plain,(
% 54.44/7.51 ![A,B,C,D]: (((((~l1_struct_0(A)|~l1_struct_0(B))|~v1_funct_1(C))|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|m1_subset_1(k4_pre_topc(A,B,C,D),k1_zfmisc_1(u1_struct_0(B))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 54.44/7.51 fof(f348,plain,(
% 54.44/7.51 ![A,B,C]: (((((~l1_struct_0(A)|~l1_struct_0(B))|~v1_funct_1(C))|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(![D]: m1_subset_1(k4_pre_topc(A,B,C,D),k1_zfmisc_1(u1_struct_0(B)))))),
% 54.44/7.51 inference(miniscoping,[status(thm)],[f347])).
% 54.44/7.51 fof(f349,plain,(
% 54.44/7.51 ![X0,X1,X2,X3]: (~l1_struct_0(X0)|~l1_struct_0(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f348])).
% 54.44/7.51 fof(f350,plain,(
% 54.44/7.51 ![A,B]: ((((((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|v3_struct_0(B))|~v2_tsp_2(B,A))|~m1_pre_topc(B,A))|(((v1_funct_1(k4_tsp_2(A,B))&v1_funct_2(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B)))&v5_pre_topc(k4_tsp_2(A,B),A,B))&m2_relset_1(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 54.44/7.51 fof(f351,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|~m1_pre_topc(X1,X0)|v1_funct_1(k4_tsp_2(X0,X1)))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f350])).
% 54.44/7.51 fof(f357,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|l1_struct_0(A))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 54.44/7.51 fof(f358,plain,(
% 54.44/7.51 ![X0]: (~l1_pre_topc(X0)|l1_struct_0(X0))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f357])).
% 54.44/7.51 fof(f361,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (~m1_tsp_1(B,A)|l1_pre_topc(B))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 54.44/7.51 fof(f362,plain,(
% 54.44/7.51 ![X0,X1]: (~l1_pre_topc(X0)|~m1_tsp_1(X1,X0)|l1_pre_topc(X1))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f361])).
% 54.44/7.51 fof(f365,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (~m2_tsp_1(B,A)|l1_pre_topc(B))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 54.44/7.51 fof(f366,plain,(
% 54.44/7.51 ![X0,X1]: (~l1_pre_topc(X0)|~m2_tsp_1(X1,X0)|l1_pre_topc(X1))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f365])).
% 54.44/7.51 fof(f367,plain,(
% 54.44/7.51 l1_pre_topc(sK8_skl)),
% 54.44/7.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f73])).
% 54.44/7.51 fof(f368,plain,(
% 54.44/7.51 l1_pre_topc(sK8_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f367])).
% 54.44/7.51 fof(f376,plain,(
% 54.44/7.51 ![A]: m1_subset_1(sK12_skl(A),A)),
% 54.44/7.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(B,sK12_skl(A))],[f77])).
% 54.44/7.51 fof(f377,plain,(
% 54.44/7.51 ![X0]: (m1_subset_1(sK12_skl(X0),X0))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f376])).
% 54.44/7.51 fof(f452,plain,(
% 54.44/7.51 (((((~v1_xboole_0(sK16_skl)&v1_membered(sK16_skl))&v2_membered(sK16_skl))&v3_membered(sK16_skl))&v4_membered(sK16_skl))&v5_membered(sK16_skl))),
% 54.44/7.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f97])).
% 54.44/7.51 fof(f453,plain,(
% 54.44/7.51 ~v1_xboole_0(sK16_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f452])).
% 54.44/7.51 fof(f467,plain,(
% 54.44/7.51 ![A]: (m1_subset_1(sK19_skl(A),k1_zfmisc_1(A))&v1_xboole_0(sK19_skl(A)))),
% 54.44/7.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(B,sK19_skl(A))],[f100])).
% 54.44/7.51 fof(f468,plain,(
% 54.44/7.51 ![X0]: (m1_subset_1(sK19_skl(X0),k1_zfmisc_1(X0)))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f467])).
% 54.44/7.51 fof(f469,plain,(
% 54.44/7.51 ![X0]: (v1_xboole_0(sK19_skl(X0)))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f467])).
% 54.44/7.51 fof(f475,plain,(
% 54.44/7.51 (l1_struct_0(sK21_skl)&~v3_struct_0(sK21_skl))),
% 54.44/7.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(A,sK21_skl)],[f102])).
% 54.44/7.51 fof(f477,plain,(
% 54.44/7.51 ~v3_struct_0(sK21_skl)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f475])).
% 54.44/7.51 fof(f520,plain,(
% 54.44/7.51 ![A,B,C,D]: (((((~l1_struct_0(A)|~l1_struct_0(B))|~v1_funct_1(C))|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|k4_pre_topc(A,B,C,D)=k9_relat_1(C,D))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f109])).
% 54.44/7.51 fof(f521,plain,(
% 54.44/7.51 ![A,B,C]: (((((~l1_struct_0(A)|~l1_struct_0(B))|~v1_funct_1(C))|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(![D]: k4_pre_topc(A,B,C,D)=k9_relat_1(C,D)))),
% 54.44/7.51 inference(miniscoping,[status(thm)],[f520])).
% 54.44/7.51 fof(f522,plain,(
% 54.44/7.51 ![X0,X1,X2,X3]: (~l1_struct_0(X0)|~l1_struct_0(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|k4_pre_topc(X0,X1,X2,X3)=k9_relat_1(X2,X3))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f521])).
% 54.44/7.51 fof(f523,plain,(
% 54.44/7.51 ![A,B]: ((((((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|v3_struct_0(B))|~v2_tsp_2(B,A))|~m1_pre_topc(B,A))|k4_tsp_2(A,B)=k1_tsp_2(A,B))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f110])).
% 54.44/7.51 fof(f524,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|~m1_pre_topc(X1,X0)|k4_tsp_2(X0,X1)=k1_tsp_2(X0,X1))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f523])).
% 54.44/7.51 fof(f525,plain,(
% 54.44/7.51 ![A,B,C]: ((~m1_subset_1(B,k1_zfmisc_1(A))|~m1_subset_1(C,k1_zfmisc_1(A)))|k5_subset_1(A,B,C)=k3_xboole_0(B,C))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f111])).
% 54.44/7.51 fof(f526,plain,(
% 54.44/7.51 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(X1))|k5_subset_1(X1,X0,X2)=k3_xboole_0(X0,X2))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f525])).
% 54.44/7.51 fof(f527,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (m1_tsp_1(B,A)<=>m1_pre_topc(B,A))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f112])).
% 54.44/7.51 fof(f528,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: ((~m1_tsp_1(B,A)|m1_pre_topc(B,A))&(m1_tsp_1(B,A)|~m1_pre_topc(B,A)))))),
% 54.44/7.51 inference(NNF_transformation,[status(thm)],[f527])).
% 54.44/7.51 fof(f529,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|((![B]: (~m1_tsp_1(B,A)|m1_pre_topc(B,A)))&(![B]: (m1_tsp_1(B,A)|~m1_pre_topc(B,A)))))),
% 54.44/7.51 inference(miniscoping,[status(thm)],[f528])).
% 54.44/7.51 fof(f531,plain,(
% 54.44/7.51 ![X0,X1]: (~l1_pre_topc(X0)|m1_tsp_1(X1,X0)|~m1_pre_topc(X1,X0))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f529])).
% 54.44/7.51 fof(f532,plain,(
% 54.44/7.51 ![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)))),
% 54.44/7.51 inference(NNF_transformation,[status(thm)],[f113])).
% 54.44/7.51 fof(f533,plain,(
% 54.44/7.51 (![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)))),
% 54.44/7.51 inference(miniscoping,[status(thm)],[f532])).
% 54.44/7.51 fof(f534,plain,(
% 54.44/7.51 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f533])).
% 54.44/7.51 fof(f536,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (m2_tsp_1(B,A)<=>m1_pre_topc(B,A))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 54.44/7.51 fof(f537,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: ((~m2_tsp_1(B,A)|m1_pre_topc(B,A))&(m2_tsp_1(B,A)|~m1_pre_topc(B,A)))))),
% 54.44/7.51 inference(NNF_transformation,[status(thm)],[f536])).
% 54.44/7.51 fof(f538,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|((![B]: (~m2_tsp_1(B,A)|m1_pre_topc(B,A)))&(![B]: (m2_tsp_1(B,A)|~m1_pre_topc(B,A)))))),
% 54.44/7.51 inference(miniscoping,[status(thm)],[f537])).
% 54.44/7.51 fof(f539,plain,(
% 54.44/7.51 ![X0,X1]: (~l1_pre_topc(X0)|~m2_tsp_1(X1,X0)|m1_pre_topc(X1,X0))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f538])).
% 54.44/7.51 fof(f541,plain,(
% 54.44/7.51 ![A]: r1_tarski(A,A)),
% 54.44/7.51 inference(miniscoping,[status(thm)],[f115])).
% 54.44/7.51 fof(f542,plain,(
% 54.44/7.51 ![X0]: (r1_tarski(X0,X0))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f541])).
% 54.44/7.51 fof(f545,plain,(
% 54.44/7.51 ![A]: (~l1_pre_topc(A)|(![B]: (~m1_pre_topc(B,A)|m1_subset_1(u1_struct_0(B),k1_zfmisc_1(u1_struct_0(A))))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f117])).
% 54.44/7.51 fof(f546,plain,(
% 54.44/7.51 ![X0,X1]: (~l1_pre_topc(X0)|~m1_pre_topc(X1,X0)|m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f545])).
% 54.44/7.51 fof(f550,plain,(
% 54.44/7.51 ![A,B]: ((~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B))&(m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 54.44/7.51 inference(NNF_transformation,[status(thm)],[f120])).
% 54.44/7.51 fof(f551,plain,(
% 54.44/7.51 (![A,B]: (~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B)))&(![A,B]: (m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 54.44/7.51 inference(miniscoping,[status(thm)],[f550])).
% 54.44/7.51 fof(f553,plain,(
% 54.44/7.51 ![X0,X1]: (m1_subset_1(X0,k1_zfmisc_1(X1))|~r1_tarski(X0,X1))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f551])).
% 54.44/7.51 fof(f557,plain,(
% 54.44/7.51 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|(~v3_pre_topc(B,A)|k3_tex_4(A,B)=B))))),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f122])).
% 54.44/7.51 fof(f558,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v3_pre_topc(X1,X0)|k3_tex_4(X0,X1)=X1)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f557])).
% 54.44/7.51 fof(f562,plain,(
% 54.44/7.51 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 54.44/7.51 inference(pre_NNF_transformation,[status(thm)],[f124])).
% 54.44/7.51 fof(f563,plain,(
% 54.44/7.51 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f562])).
% 54.44/7.51 fof(f570,plain,(
% 54.44/7.51 ![A,B,C,D]: ((~sP0_prd(D,C,B,A)|((m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&v3_pre_topc(D,A))&C=k3_xboole_0(D,u1_struct_0(B))))&(sP0_prd(D,C,B,A)|((~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))|~v3_pre_topc(D,A))|~C=k3_xboole_0(D,u1_struct_0(B)))))),
% 54.44/7.51 inference(NNF_transformation,[status(thm)],[f330])).
% 54.44/7.51 fof(f571,plain,(
% 54.44/7.51 (![A,B,C,D]: (~sP0_prd(D,C,B,A)|((m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&v3_pre_topc(D,A))&C=k3_xboole_0(D,u1_struct_0(B)))))&(![A,B,C,D]: (sP0_prd(D,C,B,A)|((~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))|~v3_pre_topc(D,A))|~C=k3_xboole_0(D,u1_struct_0(B)))))),
% 54.44/7.51 inference(miniscoping,[status(thm)],[f570])).
% 54.44/7.51 fof(f575,plain,(
% 54.44/7.51 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2,X3)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X3)))|~v3_pre_topc(X0,X3)|~X1=k3_xboole_0(X0,u1_struct_0(X2)))),
% 54.44/7.51 inference(cnf_transformation,[status(thm)],[f571])).
% 54.44/7.51 fof(f576,plain,(
% 54.44/7.51 ![X0,X1,X2]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|~m2_tsp_1(X1,X0)|~v1_funct_1(k4_tsp_2(X0,X1))|~v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)|~m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))|k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X2))=k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2))),
% 54.44/7.51 inference(destructive_equality_resolution,[status(thm)],[f324])).
% 54.44/7.51 fof(f577,plain,(
% 54.44/7.51 ![X0,X1,X2]: (sP0_prd(X0,k3_xboole_0(X0,u1_struct_0(X1)),X1,X2)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X2)))|~v3_pre_topc(X0,X2))),
% 54.44/7.51 inference(destructive_equality_resolution,[status(thm)],[f575])).
% 54.44/7.51 fof(f578,plain,(
% 54.44/7.51 ~l1_pre_topc(sK0_skl)|l1_pre_topc(sK1_skl)),
% 54.44/7.51 inference(resolution,[status(thm)],[f366,f134])).
% 54.44/7.51 fof(f579,definition,(
% 54.44/7.51 sQ0_spl <=> (l1_pre_topc(sK0_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f581,plain,(
% 54.44/7.51 ~l1_pre_topc(sK0_skl)|sQ0_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f579])).
% 54.44/7.51 fof(f582,definition,(
% 54.44/7.51 sQ1_spl <=> (l1_pre_topc(sK1_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f583,plain,(
% 54.44/7.51 l1_pre_topc(sK1_skl)|~sQ1_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f582])).
% 54.44/7.51 fof(f585,plain,(
% 54.44/7.51 ~sQ0_spl|sQ1_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f578,f579,f582])).
% 54.44/7.51 fof(f586,plain,(
% 54.44/7.51 $false|sQ0_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f581,f131])).
% 54.44/7.51 fof(f587,plain,(
% 54.44/7.51 sQ0_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f586])).
% 54.44/7.51 fof(f594,definition,(
% 54.44/7.51 sQ3_spl <=> (v3_struct_0(sK0_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f595,plain,(
% 54.44/7.51 v3_struct_0(sK0_skl)|~sQ3_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f594])).
% 54.44/7.51 fof(f603,definition,(
% 54.44/7.51 sQ4_spl <=> (v2_tsp_2(sK1_skl,sK0_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f605,plain,(
% 54.44/7.51 ~v2_tsp_2(sK1_skl,sK0_skl)|sQ4_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f603])).
% 54.44/7.51 fof(f610,plain,(
% 54.44/7.51 $false|~sQ3_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f595,f129])).
% 54.44/7.51 fof(f611,plain,(
% 54.44/7.51 ~sQ3_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f610])).
% 54.44/7.51 fof(f612,plain,(
% 54.44/7.51 $false|sQ4_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f605,f133])).
% 54.44/7.51 fof(f613,plain,(
% 54.44/7.51 sQ4_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f612])).
% 54.44/7.51 fof(f618,definition,(
% 54.44/7.51 sQ7_spl <=> (v3_struct_0(sK1_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f619,plain,(
% 54.44/7.51 v3_struct_0(sK1_skl)|~sQ7_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f618])).
% 54.44/7.51 fof(f629,plain,(
% 54.44/7.51 $false|~sQ7_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f619,f132])).
% 54.44/7.51 fof(f630,plain,(
% 54.44/7.51 ~sQ7_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f629])).
% 54.44/7.51 fof(f641,definition,(
% 54.44/7.51 sQ9_spl <=> (v2_pre_topc(sK0_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f643,plain,(
% 54.44/7.51 ~v2_pre_topc(sK0_skl)|sQ9_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f641])).
% 54.44/7.51 fof(f661,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|k4_tsp_2(X0,X1)=k1_tsp_2(X0,X1)|~l1_pre_topc(X0)|~m2_tsp_1(X1,X0))),
% 54.44/7.51 inference(resolution,[status(thm)],[f524,f539])).
% 54.44/7.51 fof(f662,plain,(
% 54.44/7.51 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~v2_tsp_2(X1,X0)|k4_tsp_2(X0,X1)=k1_tsp_2(X0,X1)|~m2_tsp_1(X1,X0))),
% 54.44/7.51 inference(duplicate_literals_removal,[status(thm)],[f661])).
% 54.44/7.51 fof(f663,plain,(
% 54.44/7.51 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK1_skl)|~v2_tsp_2(sK1_skl,sK0_skl)|k4_tsp_2(sK0_skl,sK1_skl)=k1_tsp_2(sK0_skl,sK1_skl)),
% 54.44/7.51 inference(resolution,[status(thm)],[f662,f134])).
% 54.44/7.51 fof(f664,definition,(
% 54.44/7.51 sQ12_spl <=> (k4_tsp_2(sK0_skl,sK1_skl)=k1_tsp_2(sK0_skl,sK1_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f665,plain,(
% 54.44/7.51 k4_tsp_2(sK0_skl,sK1_skl)=k1_tsp_2(sK0_skl,sK1_skl)|~sQ12_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f664])).
% 54.44/7.51 fof(f667,plain,(
% 54.44/7.51 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|sQ12_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f663,f594,f641,f579,f618,f603,f664])).
% 54.44/7.51 fof(f668,plain,(
% 54.44/7.51 $false|sQ9_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f643,f130])).
% 54.44/7.51 fof(f669,plain,(
% 54.44/7.51 sQ9_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f668])).
% 54.44/7.51 fof(f670,plain,(
% 54.44/7.51 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK1_skl)|~v2_tsp_2(sK1_skl,sK0_skl)|~m1_pre_topc(sK1_skl,sK0_skl)|v5_pre_topc(k4_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl)|~sQ12_spl),
% 54.44/7.51 inference(paramodulation,[status(thm)],[f665,f343])).
% 54.44/7.51 fof(f671,definition,(
% 54.44/7.51 sQ13_spl <=> (m1_pre_topc(sK1_skl,sK0_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f672,plain,(
% 54.44/7.51 m1_pre_topc(sK1_skl,sK0_skl)|~sQ13_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f671])).
% 54.44/7.51 fof(f673,plain,(
% 54.44/7.51 ~m1_pre_topc(sK1_skl,sK0_skl)|sQ13_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f671])).
% 54.44/7.51 fof(f674,definition,(
% 54.44/7.51 sQ14_spl <=> (v5_pre_topc(k4_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f677,plain,(
% 54.44/7.51 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ13_spl|sQ14_spl|~sQ12_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f670,f594,f641,f579,f618,f603,f671,f674,f664])).
% 54.44/7.51 fof(f678,plain,(
% 54.44/7.51 ~l1_pre_topc(sK0_skl)|~m2_tsp_1(sK1_skl,sK0_skl)|sQ13_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f673,f539])).
% 54.44/7.51 fof(f679,definition,(
% 54.44/7.51 sQ15_spl <=> (m2_tsp_1(sK1_skl,sK0_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f681,plain,(
% 54.44/7.51 ~m2_tsp_1(sK1_skl,sK0_skl)|sQ15_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f679])).
% 54.44/7.51 fof(f682,plain,(
% 54.44/7.51 ~sQ0_spl|~sQ15_spl|sQ13_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f678,f579,f679,f671])).
% 54.44/7.51 fof(f683,plain,(
% 54.44/7.51 $false|sQ15_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f681,f134])).
% 54.44/7.51 fof(f684,plain,(
% 54.44/7.51 sQ15_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f683])).
% 54.44/7.51 fof(f695,plain,(
% 54.44/7.51 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK1_skl)|~v2_tsp_2(sK1_skl,sK0_skl)|~m1_pre_topc(sK1_skl,sK0_skl)|v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~sQ12_spl),
% 54.44/7.51 inference(paramodulation,[status(thm)],[f665,f342])).
% 54.44/7.51 fof(f696,definition,(
% 54.44/7.51 sQ16_spl <=> (v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f699,plain,(
% 54.44/7.51 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ13_spl|sQ16_spl|~sQ12_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f695,f594,f641,f579,f618,f603,f671,f696,f664])).
% 54.44/7.51 fof(f700,plain,(
% 54.44/7.51 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK1_skl)|~v2_tsp_2(sK1_skl,sK0_skl)|~m1_pre_topc(sK1_skl,sK0_skl)|m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~sQ12_spl),
% 54.44/7.51 inference(paramodulation,[status(thm)],[f665,f344])).
% 54.44/7.51 fof(f701,definition,(
% 54.44/7.51 sQ17_spl <=> (m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f702,plain,(
% 54.44/7.51 m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~sQ17_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f701])).
% 54.44/7.51 fof(f704,plain,(
% 54.44/7.51 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ13_spl|sQ17_spl|~sQ12_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f700,f594,f641,f579,f618,f603,f671,f701,f664])).
% 54.44/7.51 fof(f705,plain,(
% 54.44/7.51 ![X0,X1,X2,X3,X4]: (~l1_struct_0(X0)|~l1_struct_0(X1)|~v1_funct_2(k4_tsp_2(X2,X3),u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(k4_tsp_2(X2,X3),u1_struct_0(X0),u1_struct_0(X1))|k4_pre_topc(X0,X1,k4_tsp_2(X2,X3),X4)=k9_relat_1(k4_tsp_2(X2,X3),X4)|v3_struct_0(X2)|~v2_pre_topc(X2)|~l1_pre_topc(X2)|v3_struct_0(X3)|~v2_tsp_2(X3,X2)|~m1_pre_topc(X3,X2))),
% 54.44/7.51 inference(resolution,[status(thm)],[f522,f351])).
% 54.44/7.51 fof(f709,plain,(
% 54.44/7.51 ![X0,X1,X2,X3,X4]: (~l1_struct_0(X0)|~l1_struct_0(X1)|~v1_funct_2(k4_tsp_2(X2,X3),u1_struct_0(X0),u1_struct_0(X1))|k4_pre_topc(X0,X1,k4_tsp_2(X2,X3),X4)=k9_relat_1(k4_tsp_2(X2,X3),X4)|v3_struct_0(X2)|~v2_pre_topc(X2)|~l1_pre_topc(X2)|v3_struct_0(X3)|~v2_tsp_2(X3,X2)|~m1_pre_topc(X3,X2)|~m2_relset_1(k4_tsp_2(X2,X3),u1_struct_0(X0),u1_struct_0(X1)))),
% 54.44/7.51 inference(resolution,[status(thm)],[f705,f534])).
% 54.44/7.51 fof(f710,plain,(
% 54.44/7.51 ![X0,X1,X2]: (~l1_struct_0(X0)|~l1_struct_0(X1)|~v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(X0),u1_struct_0(X1))|k4_pre_topc(X0,X1,k4_tsp_2(sK0_skl,sK1_skl),X2)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X2)|v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK1_skl)|~m1_pre_topc(sK1_skl,sK0_skl)|~m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(X0),u1_struct_0(X1)))),
% 54.44/7.51 inference(resolution,[status(thm)],[f709,f133])).
% 54.44/7.51 fof(f711,definition,(
% 54.44/7.51 ![X0,X1,X2]: (sQ18_spl <=> (~l1_struct_0(X0)|~l1_struct_0(X1)|~v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(X0),u1_struct_0(X1))|k4_pre_topc(X0,X1,k4_tsp_2(sK0_skl,sK1_skl),X2)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X2)|~m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(X0),u1_struct_0(X1))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f712,plain,(
% 54.44/7.51 ![X0,X1,X2]: (~l1_struct_0(X0)|~l1_struct_0(X1)|~v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(X0),u1_struct_0(X1))|k4_pre_topc(X0,X1,k4_tsp_2(sK0_skl,sK1_skl),X2)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X2)|~m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(X0),u1_struct_0(X1))|~sQ18_spl)),
% 54.44/7.51 inference(component_clause,[status(thm)],[f711])).
% 54.44/7.51 fof(f714,plain,(
% 54.44/7.51 sQ18_spl|sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ13_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f710,f711,f594,f641,f579,f618,f671])).
% 54.44/7.51 fof(f715,plain,(
% 54.44/7.51 ![X0]: (~l1_struct_0(sK0_skl)|~l1_struct_0(sK1_skl)|~v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),X0)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X0)|~sQ18_spl|~sQ17_spl)),
% 54.44/7.51 inference(resolution,[status(thm)],[f712,f702])).
% 54.44/7.51 fof(f717,definition,(
% 54.44/7.51 sQ19_spl <=> (l1_struct_0(sK0_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f719,plain,(
% 54.44/7.51 ~l1_struct_0(sK0_skl)|sQ19_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f717])).
% 54.44/7.51 fof(f720,definition,(
% 54.44/7.51 sQ20_spl <=> (l1_struct_0(sK1_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f722,plain,(
% 54.44/7.51 ~l1_struct_0(sK1_skl)|sQ20_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f720])).
% 54.44/7.51 fof(f723,definition,(
% 54.44/7.51 ![X0]: (sQ21_spl <=> (k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),X0)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X0)))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f724,plain,(
% 54.44/7.51 ![X0]: (k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),X0)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X0)|~sQ21_spl)),
% 54.44/7.51 inference(component_clause,[status(thm)],[f723])).
% 54.44/7.51 fof(f726,plain,(
% 54.44/7.51 ~sQ19_spl|~sQ20_spl|~sQ16_spl|sQ21_spl|~sQ18_spl|~sQ17_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f715,f717,f720,f696,f723,f711,f701])).
% 54.44/7.51 fof(f750,definition,(
% 54.44/7.51 sQ26_spl <=> (v1_funct_1(k4_tsp_2(sK0_skl,sK1_skl)))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f757,definition,(
% 54.44/7.51 sQ28_spl <=> (m1_subset_1(u1_struct_0(sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f758,plain,(
% 54.44/7.51 m1_subset_1(u1_struct_0(sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ28_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f757])).
% 54.44/7.51 fof(f759,plain,(
% 54.44/7.51 ~m1_subset_1(u1_struct_0(sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ28_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f757])).
% 54.44/7.51 fof(f766,plain,(
% 54.44/7.51 ~v3_pre_topc(k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),sK2_skl),sK1_skl)|~sQ21_spl),
% 54.44/7.51 inference(backward_demodulation,[status(thm)],[f724,f137])).
% 54.44/7.51 fof(f768,plain,(
% 54.44/7.51 ![X0]: (~l1_struct_0(sK0_skl)|~l1_struct_0(sK1_skl)|~v1_funct_1(k4_tsp_2(sK0_skl,sK1_skl))|~v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|m1_subset_1(k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X0),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~sQ21_spl)),
% 54.44/7.51 inference(paramodulation,[status(thm)],[f724,f349])).
% 54.44/7.51 fof(f772,definition,(
% 54.44/7.51 sQ30_spl <=> (m1_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f774,plain,(
% 54.44/7.51 ~m1_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ30_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f772])).
% 54.44/7.51 fof(f776,definition,(
% 54.44/7.51 ![X0]: (sQ31_spl <=> (m1_subset_1(k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X0),k1_zfmisc_1(u1_struct_0(sK1_skl)))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f777,plain,(
% 54.44/7.51 ![X0]: (m1_subset_1(k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X0),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~sQ31_spl)),
% 54.44/7.51 inference(component_clause,[status(thm)],[f776])).
% 54.44/7.51 fof(f779,plain,(
% 54.44/7.51 ~sQ19_spl|~sQ20_spl|~sQ26_spl|~sQ16_spl|~sQ30_spl|sQ31_spl|~sQ21_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f768,f717,f720,f750,f696,f772,f776,f723])).
% 54.44/7.51 fof(f780,plain,(
% 54.44/7.51 ~l1_pre_topc(sK1_skl)|sQ20_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f722,f358])).
% 54.44/7.51 fof(f781,plain,(
% 54.44/7.51 $false|~sQ1_spl|sQ20_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f780,f583])).
% 54.44/7.51 fof(f782,plain,(
% 54.44/7.51 ~sQ1_spl|sQ20_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f781])).
% 54.44/7.51 fof(f783,plain,(
% 54.44/7.51 ~l1_pre_topc(sK0_skl)|sQ19_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f719,f358])).
% 54.44/7.51 fof(f784,plain,(
% 54.44/7.51 ~sQ0_spl|sQ19_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f783,f579,f717])).
% 54.44/7.51 fof(f785,plain,(
% 54.44/7.51 ~m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ30_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f774,f534])).
% 54.44/7.51 fof(f786,plain,(
% 54.44/7.51 $false|~sQ17_spl|sQ30_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f785,f702])).
% 54.44/7.51 fof(f787,plain,(
% 54.44/7.51 ~sQ17_spl|sQ30_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f786])).
% 54.44/7.51 fof(f799,plain,(
% 54.44/7.51 ![X0]: (v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK1_skl)|~v2_tsp_2(sK1_skl,sK0_skl)|~v1_funct_1(k4_tsp_2(sK0_skl,sK1_skl))|~v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v5_pre_topc(k4_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl)|~m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_subset_1(u1_struct_0(sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,X0))=k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),X0))),
% 54.44/7.51 inference(resolution,[status(thm)],[f576,f134])).
% 54.44/7.51 fof(f800,definition,(
% 54.44/7.51 ![X0]: (sQ32_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,X0))=k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),X0)))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f801,plain,(
% 54.44/7.51 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,X0))=k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),X0)|~sQ32_spl)),
% 54.44/7.51 inference(component_clause,[status(thm)],[f800])).
% 54.44/7.51 fof(f803,plain,(
% 54.44/7.51 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ26_spl|~sQ16_spl|~sQ14_spl|~sQ17_spl|~sQ28_spl|sQ32_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f799,f594,f641,f579,f618,f603,f750,f696,f674,f701,f757,f800])).
% 54.44/7.51 fof(f804,plain,(
% 54.44/7.51 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,X0))=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),X0)|~sQ21_spl|~sQ32_spl)),
% 54.44/7.51 inference(forward_demodulation,[status(thm)],[f724,f801])).
% 54.44/7.51 fof(f807,plain,(
% 54.44/7.51 ![X0]: (k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,k3_tex_4(sK0_skl,X0)))=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),k3_tex_4(sK0_skl,X0))|v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ21_spl|~sQ32_spl)),
% 54.44/7.51 inference(resolution,[status(thm)],[f804,f346])).
% 54.44/7.51 fof(f823,definition,(
% 54.44/7.51 ![X0]: (sQ35_spl <=> (k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,k3_tex_4(sK0_skl,X0)))=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),k3_tex_4(sK0_skl,X0))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f824,plain,(
% 54.44/7.51 ![X0]: (k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,k3_tex_4(sK0_skl,X0)))=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),k3_tex_4(sK0_skl,X0))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ35_spl)),
% 54.44/7.51 inference(component_clause,[status(thm)],[f823])).
% 54.44/7.51 fof(f826,plain,(
% 54.44/7.51 sQ35_spl|sQ3_spl|~sQ0_spl|~sQ21_spl|~sQ32_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f807,f823,f594,f579,f723,f800])).
% 54.44/7.51 fof(f843,plain,(
% 54.44/7.51 ~l1_pre_topc(sK0_skl)|~m1_pre_topc(sK1_skl,sK0_skl)|sQ28_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f759,f546])).
% 54.44/7.51 fof(f845,plain,(
% 54.44/7.51 ~sQ0_spl|~sQ13_spl|sQ28_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f843,f579,f671,f757])).
% 54.44/7.51 fof(f905,definition,(
% 54.44/7.51 sQ45_spl <=> (m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f907,plain,(
% 54.44/7.51 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ45_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f905])).
% 54.44/7.51 fof(f909,plain,(
% 54.44/7.51 $false|sQ45_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f907,f135])).
% 54.44/7.51 fof(f910,plain,(
% 54.44/7.51 sQ45_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f909])).
% 54.44/7.51 fof(f935,plain,(
% 54.44/7.51 k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,k3_tex_4(sK0_skl,sK2_skl)))=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),k3_tex_4(sK0_skl,sK2_skl))|~sQ35_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f824,f135])).
% 54.44/7.51 fof(f1175,definition,(
% 54.44/7.51 sQ74_spl <=> (m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f1177,plain,(
% 54.44/7.51 ~m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ74_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f1175])).
% 54.44/7.51 fof(f1180,plain,(
% 54.44/7.51 ~r1_tarski(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ74_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f1177,f553])).
% 54.44/7.51 fof(f1185,plain,(
% 54.44/7.51 $false|sQ74_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f1180,f542])).
% 54.44/7.51 fof(f1186,plain,(
% 54.44/7.51 sQ74_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f1185])).
% 54.44/7.51 fof(f1430,plain,(
% 54.44/7.51 ![X0]: (sK19_skl(X0)=k1_xboole_0)),
% 54.44/7.51 inference(resolution,[status(thm)],[f563,f469])).
% 54.44/7.51 fof(f1463,definition,(
% 54.44/7.51 sQ94_spl <=> (m1_subset_1(sK12_skl(k1_zfmisc_1(u1_struct_0(sK0_skl))),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f1465,plain,(
% 54.44/7.51 ~m1_subset_1(sK12_skl(k1_zfmisc_1(u1_struct_0(sK0_skl))),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ94_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f1463])).
% 54.44/7.51 fof(f1467,plain,(
% 54.44/7.51 $false|sQ94_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f1465,f377])).
% 54.44/7.51 fof(f1468,plain,(
% 54.44/7.51 sQ94_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f1467])).
% 54.44/7.51 fof(f1599,plain,(
% 54.44/7.51 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 54.44/7.51 inference(forward_demodulation,[status(thm)],[f1430,f468])).
% 54.44/7.51 fof(f1852,plain,(
% 54.44/7.51 ![X0,X1,X2,X3]: (~l1_pre_topc(X0)|~m1_tsp_1(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|v3_pre_topc(X2,X1)|~sP0_prd(X3,X2,X1,X0))),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f336,f362])).
% 54.44/7.51 fof(f1853,plain,(
% 54.44/7.51 ![X0,X1,X2,X3]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X2)))|v3_pre_topc(X1,X2)|~sP0_prd(X3,X1,X2,X0)|~l1_pre_topc(X0)|~m1_pre_topc(X2,X0))),
% 54.44/7.51 inference(resolution,[status(thm)],[f1852,f531])).
% 54.44/7.51 fof(f1854,plain,(
% 54.44/7.51 ![X0,X1,X2,X3]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X2)))|v3_pre_topc(X1,X2)|~sP0_prd(X3,X1,X2,X0)|~m1_pre_topc(X2,X0))),
% 54.44/7.51 inference(duplicate_literals_removal,[status(thm)],[f1853])).
% 54.44/7.51 fof(f2448,definition,(
% 54.44/7.51 sQ212_spl <=> (m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f2450,plain,(
% 54.44/7.51 ~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ212_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f2448])).
% 54.44/7.51 fof(f2455,plain,(
% 54.44/7.51 $false|sQ212_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f2450,f1599])).
% 54.44/7.51 fof(f2456,plain,(
% 54.44/7.51 sQ212_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f2455])).
% 54.44/7.51 fof(f4634,definition,(
% 54.44/7.51 sQ475_spl <=> (l1_pre_topc(sK8_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f4636,plain,(
% 54.44/7.51 ~l1_pre_topc(sK8_skl)|sQ475_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f4634])).
% 54.44/7.51 fof(f4645,plain,(
% 54.44/7.51 $false|sQ475_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f4636,f368])).
% 54.44/7.51 fof(f4646,plain,(
% 54.44/7.51 sQ475_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f4645])).
% 54.44/7.51 fof(f4731,definition,(
% 54.44/7.51 sQ493_spl <=> (v3_struct_0(sK21_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f4732,plain,(
% 54.44/7.51 v3_struct_0(sK21_skl)|~sQ493_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f4731])).
% 54.44/7.51 fof(f4745,plain,(
% 54.44/7.51 $false|~sQ493_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f4732,f477])).
% 54.44/7.51 fof(f4746,plain,(
% 54.44/7.51 ~sQ493_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f4745])).
% 54.44/7.51 fof(f5076,definition,(
% 54.44/7.51 sQ539_spl <=> (m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ539_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f5078,plain,(
% 54.44/7.51 ~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ539_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f5076])).
% 54.44/7.51 fof(f5111,plain,(
% 54.44/7.51 $false|sQ539_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f5078,f1599])).
% 54.44/7.51 fof(f5112,plain,(
% 54.44/7.51 sQ539_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f5111])).
% 54.44/7.51 fof(f5803,plain,(
% 54.44/7.51 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k5_subset_1(u1_struct_0(sK0_skl),X0,sK2_skl)=k3_xboole_0(X0,sK2_skl))),
% 54.44/7.51 inference(resolution,[status(thm)],[f526,f135])).
% 54.44/7.51 fof(f5935,plain,(
% 54.44/7.51 k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK2_skl)=k3_xboole_0(u1_struct_0(sK1_skl),sK2_skl)|~sQ28_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f5803,f758])).
% 54.44/7.51 fof(f6104,plain,(
% 54.44/7.51 ![X0]: (v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v3_pre_topc(X0,sK0_skl)|k3_tex_4(sK0_skl,X0)=X0)),
% 54.44/7.51 inference(resolution,[status(thm)],[f558,f130])).
% 54.44/7.51 fof(f6125,definition,(
% 54.44/7.51 ![X0]: (sQ667_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v3_pre_topc(X0,sK0_skl)|k3_tex_4(sK0_skl,X0)=X0))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ667_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f6126,plain,(
% 54.44/7.51 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v3_pre_topc(X0,sK0_skl)|k3_tex_4(sK0_skl,X0)=X0|~sQ667_spl)),
% 54.44/7.51 inference(component_clause,[status(thm)],[f6125])).
% 54.44/7.51 fof(f6128,plain,(
% 54.44/7.51 sQ3_spl|~sQ0_spl|sQ667_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f6104,f594,f579,f6125])).
% 54.44/7.51 fof(f6172,plain,(
% 54.44/7.51 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k3_tex_4(sK0_skl,sK2_skl)=sK2_skl|~sQ667_spl),
% 54.44/7.51 inference(resolution,[status(thm)],[f6126,f136])).
% 54.44/7.51 fof(f6193,definition,(
% 54.44/7.51 sQ673_spl <=> (k3_tex_4(sK0_skl,sK2_skl)=sK2_skl)),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ673_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f6194,plain,(
% 54.44/7.51 k3_tex_4(sK0_skl,sK2_skl)=sK2_skl|~sQ673_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f6193])).
% 54.44/7.51 fof(f6196,plain,(
% 54.44/7.51 ~sQ45_spl|sQ673_spl|~sQ667_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f6172,f905,f6193,f6125])).
% 54.44/7.51 fof(f6203,plain,(
% 54.44/7.51 k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,k3_tex_4(sK0_skl,sK2_skl)))=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),sK2_skl)|~sQ673_spl|~sQ35_spl),
% 54.44/7.51 inference(backward_demodulation,[status(thm)],[f6194,f935])).
% 54.44/7.51 fof(f6210,plain,(
% 54.44/7.51 k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),k3_tex_4(sK0_skl,sK2_skl))=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),sK2_skl)|~sQ673_spl|~sQ35_spl),
% 54.44/7.51 inference(forward_demodulation,[status(thm)],[f6194,f6203])).
% 54.44/7.51 fof(f6211,plain,(
% 54.44/7.51 k5_subset_1(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),sK2_skl)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),sK2_skl)|~sQ673_spl|~sQ35_spl),
% 54.44/7.51 inference(forward_demodulation,[status(thm)],[f6194,f6210])).
% 54.44/7.51 fof(f6320,plain,(
% 54.44/7.51 ~v3_pre_topc(k3_xboole_0(u1_struct_0(sK1_skl),sK2_skl),sK1_skl)|~sQ28_spl|~sQ673_spl|~sQ35_spl|~sQ21_spl),
% 54.44/7.51 inference(backward_demodulation,[status(thm)],[f6321,f766])).
% 54.44/7.51 fof(f6321,plain,(
% 54.44/7.51 k3_xboole_0(u1_struct_0(sK1_skl),sK2_skl)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),sK2_skl)|~sQ28_spl|~sQ673_spl|~sQ35_spl),
% 54.44/7.51 inference(forward_demodulation,[status(thm)],[f5935,f6211])).
% 54.44/7.51 fof(f6322,plain,(
% 54.44/7.51 m1_subset_1(k3_xboole_0(u1_struct_0(sK1_skl),sK2_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~sQ31_spl|~sQ28_spl|~sQ673_spl|~sQ35_spl),
% 54.44/7.51 inference(paramodulation,[status(thm)],[f6321,f777])).
% 54.44/7.51 fof(f6328,plain,(
% 54.44/7.51 m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~sQ31_spl|~sQ28_spl|~sQ673_spl|~sQ35_spl),
% 54.44/7.51 inference(paramodulation,[status(thm)],[f318,f6322])).
% 54.44/7.51 fof(f6340,plain,(
% 54.44/7.51 ~v3_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),sK1_skl)|~sQ28_spl|~sQ673_spl|~sQ35_spl|~sQ21_spl),
% 54.44/7.51 inference(paramodulation,[status(thm)],[f318,f6320])).
% 54.44/7.51 fof(f6451,plain,(
% 54.44/7.51 ![X0]: (sP0_prd(sK2_skl,k3_xboole_0(sK2_skl,u1_struct_0(X0)),X0,sK0_skl)|~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 54.44/7.51 inference(resolution,[status(thm)],[f577,f136])).
% 54.44/7.51 fof(f6458,definition,(
% 54.44/7.51 ![X0]: (sQ678_spl <=> (sP0_prd(sK2_skl,k3_xboole_0(sK2_skl,u1_struct_0(X0)),X0,sK0_skl)))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ678_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f6459,plain,(
% 54.44/7.51 ![X0]: (sP0_prd(sK2_skl,k3_xboole_0(sK2_skl,u1_struct_0(X0)),X0,sK0_skl)|~sQ678_spl)),
% 54.44/7.51 inference(component_clause,[status(thm)],[f6458])).
% 54.44/7.51 fof(f6461,plain,(
% 54.44/7.51 sQ678_spl|~sQ45_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f6451,f6458,f905])).
% 54.44/7.51 fof(f6494,definition,(
% 54.44/7.51 sQ681_spl <=> (m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK13_skl(sK0_skl)))))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ681_spl])],[split_symbol_definition])).
% 54.44/7.51 fof(f6496,plain,(
% 54.44/7.51 ~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK13_skl(sK0_skl))))|sQ681_spl),
% 54.44/7.51 inference(component_clause,[status(thm)],[f6494])).
% 54.44/7.51 fof(f6508,plain,(
% 54.44/7.51 $false|sQ681_spl),
% 54.44/7.51 inference(forward_subsumption_resolution,[status(thm)],[f6496,f1599])).
% 54.44/7.51 fof(f6509,plain,(
% 54.44/7.51 sQ681_spl),
% 54.44/7.51 inference(contradiction_clause,[status(thm)],[f6508])).
% 54.44/7.51 fof(f7273,plain,(
% 54.44/7.51 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK1_skl)|~m1_pre_topc(sK1_skl,sK0_skl)|v1_funct_1(k4_tsp_2(sK0_skl,sK1_skl))),
% 54.44/7.51 inference(resolution,[status(thm)],[f351,f133])).
% 54.44/7.51 fof(f7274,plain,(
% 54.44/7.51 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ13_spl|sQ26_spl),
% 54.44/7.51 inference(split_clause,[status(thm)],[f7273,f594,f641,f579,f618,f671,f750])).
% 54.44/7.51 fof(f9385,definition,(
% 54.44/7.51 sQ796_spl <=> (v1_xboole_0(sK16_skl))),
% 54.44/7.51 introduced(definition,[new_symbols(definition,[sQ796_spl])],[split_symbol_definition])).
% 55.15/7.57 fof(f9386,plain,(
% 55.15/7.57 v1_xboole_0(sK16_skl)|~sQ796_spl),
% 55.15/7.57 inference(component_clause,[status(thm)],[f9385])).
% 55.15/7.57 fof(f9389,plain,(
% 55.15/7.57 $false|~sQ796_spl),
% 55.15/7.57 inference(forward_subsumption_resolution,[status(thm)],[f9386,f453])).
% 55.15/7.57 fof(f9390,plain,(
% 55.15/7.57 ~sQ796_spl),
% 55.15/7.57 inference(contradiction_clause,[status(thm)],[f9389])).
% 55.15/7.57 fof(f11807,definition,(
% 55.15/7.57 sQ973_spl <=> (m1_subset_1(sK12_skl(k1_zfmisc_1(u1_struct_0(sK1_skl))),k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 55.15/7.57 introduced(definition,[new_symbols(definition,[sQ973_spl])],[split_symbol_definition])).
% 55.15/7.57 fof(f11809,plain,(
% 55.15/7.57 ~m1_subset_1(sK12_skl(k1_zfmisc_1(u1_struct_0(sK1_skl))),k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ973_spl),
% 55.15/7.57 inference(component_clause,[status(thm)],[f11807])).
% 55.15/7.57 fof(f11810,definition,(
% 55.15/7.57 sQ974_spl <=> (m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 55.15/7.57 introduced(definition,[new_symbols(definition,[sQ974_spl])],[split_symbol_definition])).
% 55.15/7.57 fof(f11812,plain,(
% 55.15/7.57 ~m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ974_spl),
% 55.15/7.57 inference(component_clause,[status(thm)],[f11810])).
% 55.15/7.57 fof(f11817,plain,(
% 55.15/7.57 $false|~sQ31_spl|~sQ28_spl|~sQ673_spl|~sQ35_spl|sQ974_spl),
% 55.15/7.57 inference(forward_subsumption_resolution,[status(thm)],[f11812,f6328])).
% 55.15/7.57 fof(f11818,plain,(
% 55.15/7.57 ~sQ31_spl|~sQ28_spl|~sQ673_spl|~sQ35_spl|sQ974_spl),
% 55.15/7.57 inference(contradiction_clause,[status(thm)],[f11817])).
% 55.15/7.57 fof(f11819,plain,(
% 55.15/7.57 $false|sQ973_spl),
% 55.15/7.57 inference(forward_subsumption_resolution,[status(thm)],[f11809,f377])).
% 55.15/7.57 fof(f11820,plain,(
% 55.15/7.57 sQ973_spl),
% 55.15/7.57 inference(contradiction_clause,[status(thm)],[f11819])).
% 55.15/7.57 fof(f12122,plain,(
% 55.15/7.57 ![X0]: (~l1_pre_topc(sK0_skl)|~m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(X0)),k1_zfmisc_1(u1_struct_0(X0)))|v3_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(X0)),X0)|~m1_pre_topc(X0,sK0_skl)|~sQ678_spl)),
% 55.15/7.57 inference(resolution,[status(thm)],[f1854,f6459])).
% 55.15/7.57 fof(f12127,definition,(
% 55.15/7.57 ![X0]: (sQ995_spl <=> (~m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(X0)),k1_zfmisc_1(u1_struct_0(X0)))|v3_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(X0)),X0)|~m1_pre_topc(X0,sK0_skl)))),
% 55.15/7.57 introduced(definition,[new_symbols(definition,[sQ995_spl])],[split_symbol_definition])).
% 55.15/7.57 fof(f12128,plain,(
% 55.15/7.57 ![X0]: (~m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(X0)),k1_zfmisc_1(u1_struct_0(X0)))|v3_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(X0)),X0)|~m1_pre_topc(X0,sK0_skl)|~sQ995_spl)),
% 55.15/7.57 inference(component_clause,[status(thm)],[f12127])).
% 55.15/7.57 fof(f12130,plain,(
% 55.15/7.57 ~sQ0_spl|sQ995_spl|~sQ678_spl),
% 55.15/7.57 inference(split_clause,[status(thm)],[f12122,f579,f12127,f6458])).
% 55.15/7.57 fof(f14957,plain,(
% 55.15/7.57 ~m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))|v3_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),sK1_skl)|~sQ995_spl|~sQ13_spl),
% 55.15/7.57 inference(resolution,[status(thm)],[f12128,f672])).
% 55.15/7.57 fof(f14967,definition,(
% 55.15/7.57 sQ1111_spl <=> (v3_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),sK1_skl))),
% 55.15/7.57 introduced(definition,[new_symbols(definition,[sQ1111_spl])],[split_symbol_definition])).
% 55.15/7.57 fof(f14968,plain,(
% 55.15/7.57 v3_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),sK1_skl)|~sQ1111_spl),
% 55.15/7.57 inference(component_clause,[status(thm)],[f14967])).
% 55.15/7.57 fof(f14970,plain,(
% 55.15/7.57 ~sQ974_spl|sQ1111_spl|~sQ995_spl|~sQ13_spl),
% 55.15/7.57 inference(split_clause,[status(thm)],[f14957,f11810,f14967,f12127,f671])).
% 55.15/7.57 fof(f14975,plain,(
% 55.15/7.57 $false|~sQ28_spl|~sQ673_spl|~sQ35_spl|~sQ21_spl|~sQ1111_spl),
% 55.15/7.57 inference(forward_subsumption_resolution,[status(thm)],[f14968,f6340])).
% 55.15/7.57 fof(f14976,plain,(
% 55.15/7.57 ~sQ28_spl|~sQ673_spl|~sQ35_spl|~sQ21_spl|~sQ1111_spl),
% 55.15/7.57 inference(contradiction_clause,[status(thm)],[f14975])).
% 55.15/7.57 fof(f14977,plain,(
% 55.15/7.57 $false),
% 55.15/7.57 inference(sat_refutation,[status(thm)],[f585,f587,f611,f613,f630,f667,f669,f677,f682,f684,f699,f704,f714,f726,f779,f782,f784,f787,f803,f826,f845,f910,f1186,f1468,f2456,f4646,f4746,f5112,f6128,f6196,f6461,f6509,f7274,f9390,f11818,f11820,f12130,f14970,f14976])).
% 55.15/7.57 % SZS output end CNFRefutation for theBenchmark.p
% 1.85/7.71 % Elapsed time: 7.187334 seconds
% 1.85/7.71 % CPU time: 56.106224 seconds
% 1.85/7.71 % Total memory used: 602.846 MB
% 1.85/7.71 % Net memory used: 584.052 MB
%------------------------------------------------------------------------------