%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP042+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:46 PM UTC 2026
% Result : Theorem 13.39s 2.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP042+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n011.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 12:44:26 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 13.39/2.19 % Refutation found
% 13.39/2.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.39/2.19 % SZS output start CNFRefutation for theBenchmark
% 13.39/2.19 fof(f1,conjecture,(
% 13.39/2.19 (! [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)))=> ( v4_pre_topc(C,A)=> v4_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) )) )) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f2,negated_conjecture,(
% 13.39/2.19 ~((! [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)))=> ( v4_pre_topc(C,A)=> v4_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) )) )) ))),
% 13.39/2.19 inference(negated_conjecture,[status(cth)],[f1])).
% 13.39/2.19 fof(f50,axiom,(
% 13.39/2.19 (! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f52,axiom,(
% 13.39/2.19 (! [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) ) )) ) )) ) )) )) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f53,axiom,(
% 13.39/2.19 (! [A] :( l1_pre_topc(A)=> (! [B] :( l1_pre_topc(B)=> ( m2_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)))=> ( v4_pre_topc(C,B)<=> (? [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))& v4_pre_topc(D,A)& C = k3_xboole_0(D,u1_struct_0(B)) ) )) ) )) ) ) )) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f54,axiom,(
% 13.39/2.19 (! [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)) ) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f58,axiom,(
% 13.39/2.19 (! [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))) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f60,axiom,(
% 13.39/2.19 (! [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))) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f61,axiom,(
% 13.39/2.19 (! [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)) ) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f64,axiom,(
% 13.39/2.19 (! [A] :( l1_pre_topc(A)=> l1_struct_0(A) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f70,axiom,(
% 13.39/2.19 (! [A] :( l1_pre_topc(A)=> (! [B] :( m2_tsp_1(B,A)=> l1_pre_topc(B) ) )) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f72,axiom,(
% 13.39/2.19 (? [A] : l1_pre_topc(A) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f76,axiom,(
% 13.39/2.19 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f98,axiom,(
% 13.39/2.19 (! [A] :(? [B] :( m1_subset_1(B,k1_zfmisc_1(A))& v1_xboole_0(B) ) ))),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f100,axiom,(
% 13.39/2.19 (? [A] :( l1_struct_0(A)& ~ v3_struct_0(A) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f107,axiom,(
% 13.39/2.19 (! [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) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f108,axiom,(
% 13.39/2.19 (! [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) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f109,axiom,(
% 13.39/2.19 (! [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) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f110,axiom,(
% 13.39/2.19 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f111,axiom,(
% 13.39/2.19 (! [A] :( l1_pre_topc(A)=> (! [B] :( m2_tsp_1(B,A)<=> m1_pre_topc(B,A) ) )) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f112,axiom,(
% 13.39/2.19 (! [A,B] : r1_tarski(A,A) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f114,axiom,(
% 13.39/2.19 (! [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))) ) )) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f117,axiom,(
% 13.39/2.19 (! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f120,axiom,(
% 13.39/2.19 (! [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)))=> ( v4_pre_topc(B,A)=> k3_tex_4(A,B) = B ) ) )) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f121,axiom,(
% 13.39/2.19 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 13.39/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.39/2.19 fof(f124,plain,(
% 13.39/2.19 (?[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)))&(v4_pre_topc(C,A)&~v4_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B))))))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 13.39/2.19 fof(f125,plain,(
% 13.39/2.19 (((~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)))&(v4_pre_topc(sK2_skl,sK0_skl)&~v4_pre_topc(k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),sK2_skl),sK1_skl)))))),
% 13.39/2.19 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)],[f124])).
% 13.39/2.19 fof(f126,plain,(
% 13.39/2.19 ~v3_struct_0(sK0_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f127,plain,(
% 13.39/2.19 v2_pre_topc(sK0_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f128,plain,(
% 13.39/2.19 l1_pre_topc(sK0_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f129,plain,(
% 13.39/2.19 ~v3_struct_0(sK1_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f130,plain,(
% 13.39/2.19 v2_tsp_2(sK1_skl,sK0_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f131,plain,(
% 13.39/2.19 m2_tsp_1(sK1_skl,sK0_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f132,plain,(
% 13.39/2.19 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f133,plain,(
% 13.39/2.19 v4_pre_topc(sK2_skl,sK0_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f134,plain,(
% 13.39/2.19 ~v4_pre_topc(k4_pre_topc(sK0_skl,sK1_skl,k4_tsp_2(sK0_skl,sK1_skl),sK2_skl),sK1_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f125])).
% 13.39/2.19 fof(f315,plain,(
% 13.39/2.19 ![X0,X1]: (k3_xboole_0(X0,X1)=k3_xboole_0(X1,X0))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f50])).
% 13.39/2.19 fof(f318,plain,(
% 13.39/2.19 ![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))))))))))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 13.39/2.19 fof(f319,plain,(
% 13.39/2.19 ![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)))))))))))))),
% 13.39/2.19 inference(NNF_transformation,[status(thm)],[f318])).
% 13.39/2.19 fof(f320,plain,(
% 13.39/2.19 ![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))))))))))))),
% 13.39/2.19 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))],[f319])).
% 13.39/2.19 fof(f321,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f320])).
% 13.39/2.19 fof(f326,plain,(
% 13.39/2.19 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|(m2_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)))|(v4_pre_topc(C,B)<=>(?[D]: ((m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&v4_pre_topc(D,A))&C=k3_xboole_0(D,u1_struct_0(B))))))))))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 13.39/2.19 fof(f327,definition,(
% 13.39/2.19 ![A,B,C,D]: (sP0_prd(D,C,B,A)<=>((m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&v4_pre_topc(D,A))&C=k3_xboole_0(D,u1_struct_0(B))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 13.39/2.19 fof(f328,plain,(
% 13.39/2.19 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|(m2_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)))|(v4_pre_topc(C,B)<=>(?[D]: sP0_prd(D,C,B,A))))))))))),
% 13.39/2.19 inference(formula_renaming,[status(thm)],[f326,f327])).
% 13.39/2.19 fof(f329,plain,(
% 13.39/2.19 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|((~m2_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)))|((~v4_pre_topc(C,B)|(?[D]: sP0_prd(D,C,B,A)))&(v4_pre_topc(C,B)|(![D]: ~sP0_prd(D,C,B,A))))))))&(m2_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)))&((~v4_pre_topc(C,B)|(![D]: ~sP0_prd(D,C,B,A)))&(v4_pre_topc(C,B)|(?[D]: sP0_prd(D,C,B,A))))))))))))),
% 13.39/2.19 inference(NNF_transformation,[status(thm)],[f328])).
% 13.39/2.19 fof(f330,plain,(
% 13.39/2.19 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|((~m2_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)))|((~v4_pre_topc(C,B)|sP0_prd(sK5_skl(C,B,A),C,B,A))&(v4_pre_topc(C,B)|(![D]: ~sP0_prd(D,C,B,A))))))))&(m2_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)))&((~v4_pre_topc(sK6_skl(B,A),B)|(![D]: ~sP0_prd(D,sK6_skl(B,A),B,A)))&(v4_pre_topc(sK6_skl(B,A),B)|sP0_prd(sK7_skl(B,A),sK6_skl(B,A),B,A))))))))))),
% 13.39/2.19 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))],[f329])).
% 13.39/2.19 fof(f333,plain,(
% 13.39/2.19 ![X0,X1,X2,X3]: (~l1_pre_topc(X0)|~l1_pre_topc(X1)|~m2_tsp_1(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|v4_pre_topc(X2,X1)|~sP0_prd(X3,X2,X1,X0))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f330])).
% 13.39/2.19 fof(f337,plain,(
% 13.39/2.19 ![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))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 13.39/2.19 fof(f339,plain,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f337])).
% 13.39/2.19 fof(f340,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f337])).
% 13.39/2.19 fof(f341,plain,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f337])).
% 13.39/2.19 fof(f342,plain,(
% 13.39/2.19 ![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))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 13.39/2.19 fof(f343,plain,(
% 13.39/2.19 ![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))))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f342])).
% 13.39/2.19 fof(f344,plain,(
% 13.39/2.19 ![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))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 13.39/2.19 fof(f345,plain,(
% 13.39/2.19 ![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)))))),
% 13.39/2.19 inference(miniscoping,[status(thm)],[f344])).
% 13.39/2.19 fof(f346,plain,(
% 13.39/2.19 ![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))))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f345])).
% 13.39/2.19 fof(f347,plain,(
% 13.39/2.19 ![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))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 13.39/2.19 fof(f348,plain,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f347])).
% 13.39/2.19 fof(f354,plain,(
% 13.39/2.19 ![A]: (~l1_pre_topc(A)|l1_struct_0(A))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 13.39/2.19 fof(f355,plain,(
% 13.39/2.19 ![X0]: (~l1_pre_topc(X0)|l1_struct_0(X0))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f354])).
% 13.39/2.19 fof(f360,plain,(
% 13.39/2.19 ![A]: (~l1_pre_topc(A)|(![B]: (~m2_tsp_1(B,A)|l1_pre_topc(B))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 13.39/2.19 fof(f361,plain,(
% 13.39/2.19 ![X0,X1]: (~l1_pre_topc(X0)|~m2_tsp_1(X1,X0)|l1_pre_topc(X1))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f360])).
% 13.39/2.19 fof(f362,plain,(
% 13.39/2.19 l1_pre_topc(sK8_skl)),
% 13.39/2.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f72])).
% 13.39/2.19 fof(f363,plain,(
% 13.39/2.19 l1_pre_topc(sK8_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f362])).
% 13.39/2.19 fof(f371,plain,(
% 13.39/2.19 ![A]: m1_subset_1(sK12_skl(A),A)),
% 13.39/2.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(B,sK12_skl(A))],[f76])).
% 13.39/2.19 fof(f372,plain,(
% 13.39/2.19 ![X0]: (m1_subset_1(sK12_skl(X0),X0))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f371])).
% 13.39/2.19 fof(f459,plain,(
% 13.39/2.19 ![A]: (m1_subset_1(sK18_skl(A),k1_zfmisc_1(A))&v1_xboole_0(sK18_skl(A)))),
% 13.39/2.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(B,sK18_skl(A))],[f98])).
% 13.39/2.19 fof(f460,plain,(
% 13.39/2.19 ![X0]: (m1_subset_1(sK18_skl(X0),k1_zfmisc_1(X0)))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f459])).
% 13.39/2.19 fof(f461,plain,(
% 13.39/2.19 ![X0]: (v1_xboole_0(sK18_skl(X0)))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f459])).
% 13.39/2.19 fof(f467,plain,(
% 13.39/2.19 (l1_struct_0(sK20_skl)&~v3_struct_0(sK20_skl))),
% 13.39/2.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f100])).
% 13.39/2.19 fof(f469,plain,(
% 13.39/2.19 ~v3_struct_0(sK20_skl)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f467])).
% 13.39/2.19 fof(f512,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 13.39/2.19 fof(f513,plain,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 inference(miniscoping,[status(thm)],[f512])).
% 13.39/2.19 fof(f514,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f513])).
% 13.39/2.19 fof(f515,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f108])).
% 13.39/2.19 fof(f516,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f515])).
% 13.39/2.19 fof(f517,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f109])).
% 13.39/2.19 fof(f518,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f517])).
% 13.39/2.19 fof(f519,plain,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 inference(NNF_transformation,[status(thm)],[f110])).
% 13.39/2.19 fof(f520,plain,(
% 13.39/2.19 (![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)))),
% 13.39/2.19 inference(miniscoping,[status(thm)],[f519])).
% 13.39/2.19 fof(f521,plain,(
% 13.39/2.19 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f520])).
% 13.39/2.19 fof(f523,plain,(
% 13.39/2.19 ![A]: (~l1_pre_topc(A)|(![B]: (m2_tsp_1(B,A)<=>m1_pre_topc(B,A))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f111])).
% 13.39/2.19 fof(f524,plain,(
% 13.39/2.19 ![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)))))),
% 13.39/2.19 inference(NNF_transformation,[status(thm)],[f523])).
% 13.39/2.19 fof(f525,plain,(
% 13.39/2.19 ![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)))))),
% 13.39/2.19 inference(miniscoping,[status(thm)],[f524])).
% 13.39/2.19 fof(f526,plain,(
% 13.39/2.19 ![X0,X1]: (~l1_pre_topc(X0)|~m2_tsp_1(X1,X0)|m1_pre_topc(X1,X0))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f525])).
% 13.39/2.19 fof(f528,plain,(
% 13.39/2.19 ![A]: r1_tarski(A,A)),
% 13.39/2.19 inference(miniscoping,[status(thm)],[f112])).
% 13.39/2.19 fof(f529,plain,(
% 13.39/2.19 ![X0]: (r1_tarski(X0,X0))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f528])).
% 13.39/2.19 fof(f532,plain,(
% 13.39/2.19 ![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))))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 13.39/2.19 fof(f533,plain,(
% 13.39/2.19 ![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))))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f532])).
% 13.39/2.19 fof(f537,plain,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 inference(NNF_transformation,[status(thm)],[f117])).
% 13.39/2.19 fof(f538,plain,(
% 13.39/2.19 (![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)))),
% 13.39/2.19 inference(miniscoping,[status(thm)],[f537])).
% 13.39/2.19 fof(f540,plain,(
% 13.39/2.19 ![X0,X1]: (m1_subset_1(X0,k1_zfmisc_1(X1))|~r1_tarski(X0,X1))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f538])).
% 13.39/2.19 fof(f547,plain,(
% 13.39/2.19 ![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)))|(~v4_pre_topc(B,A)|k3_tex_4(A,B)=B))))),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 13.39/2.19 fof(f548,plain,(
% 13.39/2.19 ![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)))|~v4_pre_topc(X1,X0)|k3_tex_4(X0,X1)=X1)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f547])).
% 13.39/2.19 fof(f549,plain,(
% 13.39/2.19 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 13.39/2.19 inference(pre_NNF_transformation,[status(thm)],[f121])).
% 13.39/2.19 fof(f550,plain,(
% 13.39/2.19 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f549])).
% 13.39/2.19 fof(f557,plain,(
% 13.39/2.19 ![A,B,C,D]: ((~sP0_prd(D,C,B,A)|((m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&v4_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)))|~v4_pre_topc(D,A))|~C=k3_xboole_0(D,u1_struct_0(B)))))),
% 13.39/2.19 inference(NNF_transformation,[status(thm)],[f327])).
% 13.39/2.19 fof(f558,plain,(
% 13.39/2.19 (![A,B,C,D]: (~sP0_prd(D,C,B,A)|((m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))&v4_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)))|~v4_pre_topc(D,A))|~C=k3_xboole_0(D,u1_struct_0(B)))))),
% 13.39/2.19 inference(miniscoping,[status(thm)],[f557])).
% 13.39/2.19 fof(f562,plain,(
% 13.39/2.19 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2,X3)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X3)))|~v4_pre_topc(X0,X3)|~X1=k3_xboole_0(X0,u1_struct_0(X2)))),
% 13.39/2.19 inference(cnf_transformation,[status(thm)],[f558])).
% 13.39/2.19 fof(f563,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(destructive_equality_resolution,[status(thm)],[f321])).
% 13.39/2.19 fof(f564,plain,(
% 13.39/2.19 ![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)))|~v4_pre_topc(X0,X2))),
% 13.39/2.19 inference(destructive_equality_resolution,[status(thm)],[f562])).
% 13.39/2.19 fof(f565,plain,(
% 13.39/2.19 ~l1_pre_topc(sK0_skl)|l1_pre_topc(sK1_skl)),
% 13.39/2.19 inference(resolution,[status(thm)],[f361,f131])).
% 13.39/2.19 fof(f566,definition,(
% 13.39/2.19 sQ0_spl <=> (l1_pre_topc(sK0_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f568,plain,(
% 13.39/2.19 ~l1_pre_topc(sK0_skl)|sQ0_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f566])).
% 13.39/2.19 fof(f569,definition,(
% 13.39/2.19 sQ1_spl <=> (l1_pre_topc(sK1_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f570,plain,(
% 13.39/2.19 l1_pre_topc(sK1_skl)|~sQ1_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f569])).
% 13.39/2.19 fof(f572,plain,(
% 13.39/2.19 ~sQ0_spl|sQ1_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f565,f566,f569])).
% 13.39/2.19 fof(f573,plain,(
% 13.39/2.19 $false|sQ0_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f568,f128])).
% 13.39/2.19 fof(f574,plain,(
% 13.39/2.19 sQ0_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f573])).
% 13.39/2.19 fof(f581,definition,(
% 13.39/2.19 sQ3_spl <=> (v3_struct_0(sK0_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f582,plain,(
% 13.39/2.19 v3_struct_0(sK0_skl)|~sQ3_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f581])).
% 13.39/2.19 fof(f590,definition,(
% 13.39/2.19 sQ4_spl <=> (v2_tsp_2(sK1_skl,sK0_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f592,plain,(
% 13.39/2.19 ~v2_tsp_2(sK1_skl,sK0_skl)|sQ4_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f590])).
% 13.39/2.19 fof(f597,plain,(
% 13.39/2.19 $false|~sQ3_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f582,f126])).
% 13.39/2.19 fof(f598,plain,(
% 13.39/2.19 ~sQ3_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f597])).
% 13.39/2.19 fof(f599,plain,(
% 13.39/2.19 $false|sQ4_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f592,f130])).
% 13.39/2.19 fof(f600,plain,(
% 13.39/2.19 sQ4_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f599])).
% 13.39/2.19 fof(f605,definition,(
% 13.39/2.19 sQ7_spl <=> (v3_struct_0(sK1_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f606,plain,(
% 13.39/2.19 v3_struct_0(sK1_skl)|~sQ7_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f605])).
% 13.39/2.19 fof(f616,plain,(
% 13.39/2.19 $false|~sQ7_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f606,f129])).
% 13.39/2.19 fof(f617,plain,(
% 13.39/2.19 ~sQ7_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f616])).
% 13.39/2.19 fof(f626,definition,(
% 13.39/2.19 sQ9_spl <=> (v2_pre_topc(sK0_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f628,plain,(
% 13.39/2.19 ~v2_pre_topc(sK0_skl)|sQ9_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f626])).
% 13.39/2.19 fof(f646,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(resolution,[status(thm)],[f516,f526])).
% 13.39/2.19 fof(f647,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(duplicate_literals_removal,[status(thm)],[f646])).
% 13.39/2.19 fof(f648,plain,(
% 13.39/2.19 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)),
% 13.39/2.19 inference(resolution,[status(thm)],[f647,f131])).
% 13.39/2.19 fof(f649,definition,(
% 13.39/2.19 sQ12_spl <=> (k4_tsp_2(sK0_skl,sK1_skl)=k1_tsp_2(sK0_skl,sK1_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f650,plain,(
% 13.39/2.19 k4_tsp_2(sK0_skl,sK1_skl)=k1_tsp_2(sK0_skl,sK1_skl)|~sQ12_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f649])).
% 13.39/2.19 fof(f652,plain,(
% 13.39/2.19 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|sQ12_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f648,f581,f626,f566,f605,f590,f649])).
% 13.39/2.19 fof(f653,plain,(
% 13.39/2.19 $false|sQ9_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f628,f127])).
% 13.39/2.19 fof(f654,plain,(
% 13.39/2.19 sQ9_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f653])).
% 13.39/2.19 fof(f655,plain,(
% 13.39/2.19 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),
% 13.39/2.19 inference(paramodulation,[status(thm)],[f650,f340])).
% 13.39/2.19 fof(f656,definition,(
% 13.39/2.19 sQ13_spl <=> (m1_pre_topc(sK1_skl,sK0_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f658,plain,(
% 13.39/2.19 ~m1_pre_topc(sK1_skl,sK0_skl)|sQ13_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f656])).
% 13.39/2.19 fof(f659,definition,(
% 13.39/2.19 sQ14_spl <=> (v5_pre_topc(k4_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f662,plain,(
% 13.39/2.19 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ13_spl|sQ14_spl|~sQ12_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f655,f581,f626,f566,f605,f590,f656,f659,f649])).
% 13.39/2.19 fof(f663,plain,(
% 13.39/2.19 ~l1_pre_topc(sK0_skl)|~m2_tsp_1(sK1_skl,sK0_skl)|sQ13_spl),
% 13.39/2.19 inference(resolution,[status(thm)],[f658,f526])).
% 13.39/2.19 fof(f664,definition,(
% 13.39/2.19 sQ15_spl <=> (m2_tsp_1(sK1_skl,sK0_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f666,plain,(
% 13.39/2.19 ~m2_tsp_1(sK1_skl,sK0_skl)|sQ15_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f664])).
% 13.39/2.19 fof(f667,plain,(
% 13.39/2.19 ~sQ0_spl|~sQ15_spl|sQ13_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f663,f566,f664,f656])).
% 13.39/2.19 fof(f668,plain,(
% 13.39/2.19 $false|sQ15_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f666,f131])).
% 13.39/2.19 fof(f669,plain,(
% 13.39/2.19 sQ15_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f668])).
% 13.39/2.19 fof(f680,plain,(
% 13.39/2.19 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),
% 13.39/2.19 inference(paramodulation,[status(thm)],[f650,f339])).
% 13.39/2.19 fof(f681,definition,(
% 13.39/2.19 sQ16_spl <=> (v1_funct_2(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f684,plain,(
% 13.39/2.19 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ13_spl|sQ16_spl|~sQ12_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f680,f581,f626,f566,f605,f590,f656,f681,f649])).
% 13.39/2.19 fof(f685,plain,(
% 13.39/2.19 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),
% 13.39/2.19 inference(paramodulation,[status(thm)],[f650,f341])).
% 13.39/2.19 fof(f686,definition,(
% 13.39/2.19 sQ17_spl <=> (m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f687,plain,(
% 13.39/2.19 m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~sQ17_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f686])).
% 13.39/2.19 fof(f689,plain,(
% 13.39/2.19 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ13_spl|sQ17_spl|~sQ12_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f685,f581,f626,f566,f605,f590,f656,f686,f649])).
% 13.39/2.19 fof(f690,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(resolution,[status(thm)],[f514,f348])).
% 13.39/2.19 fof(f694,plain,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 inference(resolution,[status(thm)],[f690,f521])).
% 13.39/2.19 fof(f695,plain,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 inference(resolution,[status(thm)],[f694,f130])).
% 13.39/2.19 fof(f696,definition,(
% 13.39/2.19 ![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))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f697,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(component_clause,[status(thm)],[f696])).
% 13.39/2.19 fof(f699,plain,(
% 13.39/2.19 sQ18_spl|sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ13_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f695,f696,f581,f626,f566,f605,f656])).
% 13.39/2.19 fof(f700,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(resolution,[status(thm)],[f697,f687])).
% 13.39/2.19 fof(f702,definition,(
% 13.39/2.19 sQ19_spl <=> (l1_struct_0(sK0_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f704,plain,(
% 13.39/2.19 ~l1_struct_0(sK0_skl)|sQ19_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f702])).
% 13.39/2.19 fof(f705,definition,(
% 13.39/2.19 sQ20_spl <=> (l1_struct_0(sK1_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f707,plain,(
% 13.39/2.19 ~l1_struct_0(sK1_skl)|sQ20_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f705])).
% 13.39/2.19 fof(f708,definition,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f709,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(component_clause,[status(thm)],[f708])).
% 13.39/2.19 fof(f711,plain,(
% 13.39/2.19 ~sQ19_spl|~sQ20_spl|~sQ16_spl|sQ21_spl|~sQ18_spl|~sQ17_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f700,f702,f705,f681,f708,f696,f686])).
% 13.39/2.19 fof(f735,definition,(
% 13.39/2.19 sQ26_spl <=> (v1_funct_1(k4_tsp_2(sK0_skl,sK1_skl)))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f737,plain,(
% 13.39/2.19 ~v1_funct_1(k4_tsp_2(sK0_skl,sK1_skl))|sQ26_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f735])).
% 13.39/2.19 fof(f742,definition,(
% 13.39/2.19 sQ28_spl <=> (m1_subset_1(u1_struct_0(sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f743,plain,(
% 13.39/2.19 m1_subset_1(u1_struct_0(sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ28_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f742])).
% 13.39/2.19 fof(f744,plain,(
% 13.39/2.19 ~m1_subset_1(u1_struct_0(sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ28_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f742])).
% 13.39/2.19 fof(f746,plain,(
% 13.39/2.19 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)|sQ26_spl),
% 13.39/2.19 inference(resolution,[status(thm)],[f737,f348])).
% 13.39/2.19 fof(f747,plain,(
% 13.39/2.19 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ13_spl|sQ26_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f746,f581,f626,f566,f605,f590,f656,f735])).
% 13.39/2.19 fof(f751,plain,(
% 13.39/2.19 ~v4_pre_topc(k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),sK2_skl),sK1_skl)|~sQ21_spl),
% 13.39/2.19 inference(backward_demodulation,[status(thm)],[f709,f134])).
% 13.39/2.19 fof(f753,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(paramodulation,[status(thm)],[f709,f346])).
% 13.39/2.19 fof(f757,definition,(
% 13.39/2.19 sQ30_spl <=> (m1_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f759,plain,(
% 13.39/2.19 ~m1_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ30_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f757])).
% 13.39/2.19 fof(f761,definition,(
% 13.39/2.19 ![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)))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f762,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(component_clause,[status(thm)],[f761])).
% 13.39/2.19 fof(f764,plain,(
% 13.39/2.19 ~sQ19_spl|~sQ20_spl|~sQ26_spl|~sQ16_spl|~sQ30_spl|sQ31_spl|~sQ21_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f753,f702,f705,f735,f681,f757,f761,f708])).
% 13.39/2.19 fof(f765,plain,(
% 13.39/2.19 ~l1_pre_topc(sK1_skl)|sQ20_spl),
% 13.39/2.19 inference(resolution,[status(thm)],[f707,f355])).
% 13.39/2.19 fof(f766,plain,(
% 13.39/2.19 $false|~sQ1_spl|sQ20_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f765,f570])).
% 13.39/2.19 fof(f767,plain,(
% 13.39/2.19 ~sQ1_spl|sQ20_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f766])).
% 13.39/2.19 fof(f768,plain,(
% 13.39/2.19 ~l1_pre_topc(sK0_skl)|sQ19_spl),
% 13.39/2.19 inference(resolution,[status(thm)],[f704,f355])).
% 13.39/2.19 fof(f769,plain,(
% 13.39/2.19 ~sQ0_spl|sQ19_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f768,f566,f702])).
% 13.39/2.19 fof(f770,plain,(
% 13.39/2.19 ~m2_relset_1(k4_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ30_spl),
% 13.39/2.19 inference(resolution,[status(thm)],[f759,f521])).
% 13.39/2.19 fof(f771,plain,(
% 13.39/2.19 $false|~sQ17_spl|sQ30_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f770,f687])).
% 13.39/2.19 fof(f772,plain,(
% 13.39/2.19 ~sQ17_spl|sQ30_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f771])).
% 13.39/2.19 fof(f784,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(resolution,[status(thm)],[f563,f131])).
% 13.39/2.19 fof(f785,definition,(
% 13.39/2.19 ![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)))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f786,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(component_clause,[status(thm)],[f785])).
% 13.39/2.19 fof(f788,plain,(
% 13.39/2.19 sQ3_spl|~sQ9_spl|~sQ0_spl|sQ7_spl|~sQ4_spl|~sQ26_spl|~sQ16_spl|~sQ14_spl|~sQ17_spl|~sQ28_spl|sQ32_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f784,f581,f626,f566,f605,f590,f735,f681,f659,f686,f742,f785])).
% 13.39/2.19 fof(f789,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(forward_demodulation,[status(thm)],[f709,f786])).
% 13.39/2.19 fof(f792,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(resolution,[status(thm)],[f789,f343])).
% 13.39/2.19 fof(f808,definition,(
% 13.39/2.19 ![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)))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f809,plain,(
% 13.39/2.19 ![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)),
% 13.39/2.19 inference(component_clause,[status(thm)],[f808])).
% 13.39/2.19 fof(f811,plain,(
% 13.39/2.19 sQ35_spl|sQ3_spl|~sQ0_spl|~sQ21_spl|~sQ32_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f792,f808,f581,f566,f708,f785])).
% 13.39/2.19 fof(f828,plain,(
% 13.39/2.19 ~l1_pre_topc(sK0_skl)|~m1_pre_topc(sK1_skl,sK0_skl)|sQ28_spl),
% 13.39/2.19 inference(resolution,[status(thm)],[f744,f533])).
% 13.39/2.19 fof(f830,plain,(
% 13.39/2.19 ~sQ0_spl|~sQ13_spl|sQ28_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f828,f566,f656,f742])).
% 13.39/2.19 fof(f894,definition,(
% 13.39/2.19 sQ45_spl <=> (m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f896,plain,(
% 13.39/2.19 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ45_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f894])).
% 13.39/2.19 fof(f898,plain,(
% 13.39/2.19 $false|sQ45_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f896,f132])).
% 13.39/2.19 fof(f899,plain,(
% 13.39/2.19 sQ45_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f898])).
% 13.39/2.19 fof(f924,plain,(
% 13.39/2.19 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),
% 13.39/2.19 inference(resolution,[status(thm)],[f809,f132])).
% 13.39/2.19 fof(f1162,definition,(
% 13.39/2.19 sQ74_spl <=> (m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f1164,plain,(
% 13.39/2.19 ~m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ74_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f1162])).
% 13.39/2.19 fof(f1167,plain,(
% 13.39/2.19 ~r1_tarski(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ74_spl),
% 13.39/2.19 inference(resolution,[status(thm)],[f1164,f540])).
% 13.39/2.19 fof(f1172,plain,(
% 13.39/2.19 $false|sQ74_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f1167,f529])).
% 13.39/2.19 fof(f1173,plain,(
% 13.39/2.19 sQ74_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f1172])).
% 13.39/2.19 fof(f1415,plain,(
% 13.39/2.19 ![X0]: (sK18_skl(X0)=k1_xboole_0)),
% 13.39/2.19 inference(resolution,[status(thm)],[f550,f461])).
% 13.39/2.19 fof(f1448,definition,(
% 13.39/2.19 sQ94_spl <=> (m1_subset_1(sK12_skl(k1_zfmisc_1(u1_struct_0(sK0_skl))),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f1450,plain,(
% 13.39/2.19 ~m1_subset_1(sK12_skl(k1_zfmisc_1(u1_struct_0(sK0_skl))),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ94_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f1448])).
% 13.39/2.19 fof(f1452,plain,(
% 13.39/2.19 $false|sQ94_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f1450,f372])).
% 13.39/2.19 fof(f1453,plain,(
% 13.39/2.19 sQ94_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f1452])).
% 13.39/2.19 fof(f1584,plain,(
% 13.39/2.19 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 13.39/2.19 inference(forward_demodulation,[status(thm)],[f1415,f460])).
% 13.39/2.19 fof(f1811,plain,(
% 13.39/2.19 ![X0,X1,X2,X3]: (~l1_pre_topc(X0)|~m2_tsp_1(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|v4_pre_topc(X2,X1)|~sP0_prd(X3,X2,X1,X0))),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f333,f361])).
% 13.39/2.19 fof(f1812,plain,(
% 13.39/2.19 ![X0,X1]: (~l1_pre_topc(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v4_pre_topc(X0,sK1_skl)|~sP0_prd(X1,X0,sK1_skl,sK0_skl))),
% 13.39/2.19 inference(resolution,[status(thm)],[f1811,f131])).
% 13.39/2.19 fof(f1813,definition,(
% 13.39/2.19 ![X0,X1]: (sQ121_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v4_pre_topc(X0,sK1_skl)|~sP0_prd(X1,X0,sK1_skl,sK0_skl)))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f1814,plain,(
% 13.39/2.19 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v4_pre_topc(X0,sK1_skl)|~sP0_prd(X1,X0,sK1_skl,sK0_skl)|~sQ121_spl)),
% 13.39/2.19 inference(component_clause,[status(thm)],[f1813])).
% 13.39/2.19 fof(f1816,plain,(
% 13.39/2.19 ~sQ0_spl|sQ121_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f1812,f566,f1813])).
% 13.39/2.19 fof(f2084,definition,(
% 13.39/2.19 sQ174_spl <=> (l1_pre_topc(sK8_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f2086,plain,(
% 13.39/2.19 ~l1_pre_topc(sK8_skl)|sQ174_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f2084])).
% 13.39/2.19 fof(f2157,plain,(
% 13.39/2.19 $false|sQ174_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f2086,f363])).
% 13.39/2.19 fof(f2158,plain,(
% 13.39/2.19 sQ174_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f2157])).
% 13.39/2.19 fof(f2801,definition,(
% 13.39/2.19 sQ291_spl <=> (m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ291_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f2803,plain,(
% 13.39/2.19 ~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ291_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f2801])).
% 13.39/2.19 fof(f2808,plain,(
% 13.39/2.19 $false|sQ291_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f2803,f1584])).
% 13.39/2.19 fof(f2809,plain,(
% 13.39/2.19 sQ291_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f2808])).
% 13.39/2.19 fof(f4683,definition,(
% 13.39/2.19 sQ519_spl <=> (v3_struct_0(sK20_skl))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f4684,plain,(
% 13.39/2.19 v3_struct_0(sK20_skl)|~sQ519_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f4683])).
% 13.39/2.19 fof(f4697,plain,(
% 13.39/2.19 $false|~sQ519_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f4684,f469])).
% 13.39/2.19 fof(f4698,plain,(
% 13.39/2.19 ~sQ519_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f4697])).
% 13.39/2.19 fof(f5433,definition,(
% 13.39/2.19 sQ612_spl <=> (m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f5435,plain,(
% 13.39/2.19 ~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ612_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f5433])).
% 13.39/2.19 fof(f5468,plain,(
% 13.39/2.19 $false|sQ612_spl),
% 13.39/2.19 inference(forward_subsumption_resolution,[status(thm)],[f5435,f1584])).
% 13.39/2.19 fof(f5469,plain,(
% 13.39/2.19 sQ612_spl),
% 13.39/2.19 inference(contradiction_clause,[status(thm)],[f5468])).
% 13.39/2.19 fof(f5600,plain,(
% 13.39/2.19 ![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))),
% 13.39/2.19 inference(resolution,[status(thm)],[f518,f132])).
% 13.39/2.19 fof(f5719,plain,(
% 13.39/2.19 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),
% 13.39/2.19 inference(resolution,[status(thm)],[f5600,f743])).
% 13.39/2.19 fof(f5907,plain,(
% 13.39/2.19 ![X0]: (v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v4_pre_topc(X0,sK0_skl)|k3_tex_4(sK0_skl,X0)=X0)),
% 13.39/2.19 inference(resolution,[status(thm)],[f548,f127])).
% 13.39/2.19 fof(f5920,definition,(
% 13.39/2.19 ![X0]: (sQ644_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v4_pre_topc(X0,sK0_skl)|k3_tex_4(sK0_skl,X0)=X0))),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f5921,plain,(
% 13.39/2.19 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v4_pre_topc(X0,sK0_skl)|k3_tex_4(sK0_skl,X0)=X0|~sQ644_spl)),
% 13.39/2.19 inference(component_clause,[status(thm)],[f5920])).
% 13.39/2.19 fof(f5923,plain,(
% 13.39/2.19 sQ3_spl|~sQ0_spl|sQ644_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f5907,f581,f566,f5920])).
% 13.39/2.19 fof(f5970,plain,(
% 13.39/2.19 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k3_tex_4(sK0_skl,sK2_skl)=sK2_skl|~sQ644_spl),
% 13.39/2.19 inference(resolution,[status(thm)],[f5921,f133])).
% 13.39/2.19 fof(f5995,definition,(
% 13.39/2.19 sQ651_spl <=> (k3_tex_4(sK0_skl,sK2_skl)=sK2_skl)),
% 13.39/2.19 introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition])).
% 13.39/2.19 fof(f5996,plain,(
% 13.39/2.19 k3_tex_4(sK0_skl,sK2_skl)=sK2_skl|~sQ651_spl),
% 13.39/2.19 inference(component_clause,[status(thm)],[f5995])).
% 13.39/2.19 fof(f5998,plain,(
% 13.39/2.19 ~sQ45_spl|sQ651_spl|~sQ644_spl),
% 13.39/2.19 inference(split_clause,[status(thm)],[f5970,f894,f5995,f5920])).
% 13.39/2.19 fof(f6003,plain,(
% 13.39/2.19 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)|~sQ651_spl|~sQ35_spl),
% 13.39/2.19 inference(backward_demodulation,[status(thm)],[f5996,f924])).
% 13.39/2.19 fof(f6010,plain,(
% 13.39/2.19 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)|~sQ651_spl|~sQ35_spl),
% 13.39/2.19 inference(forward_demodulation,[status(thm)],[f5996,f6003])).
% 13.39/2.19 fof(f6011,plain,(
% 12.04/2.23 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)|~sQ651_spl|~sQ35_spl),
% 12.04/2.23 inference(forward_demodulation,[status(thm)],[f5996,f6010])).
% 12.04/2.23 fof(f6012,plain,(
% 12.04/2.23 k3_xboole_0(u1_struct_0(sK1_skl),sK2_skl)=k9_relat_1(k4_tsp_2(sK0_skl,sK1_skl),sK2_skl)|~sQ28_spl|~sQ651_spl|~sQ35_spl),
% 12.04/2.23 inference(forward_demodulation,[status(thm)],[f5719,f6011])).
% 12.04/2.23 fof(f6017,plain,(
% 12.04/2.23 ~v4_pre_topc(k3_xboole_0(u1_struct_0(sK1_skl),sK2_skl),sK1_skl)|~sQ28_spl|~sQ651_spl|~sQ35_spl|~sQ21_spl),
% 12.04/2.23 inference(backward_demodulation,[status(thm)],[f6012,f751])).
% 12.04/2.23 fof(f6018,plain,(
% 12.04/2.23 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|~sQ651_spl|~sQ35_spl),
% 12.04/2.23 inference(paramodulation,[status(thm)],[f6012,f762])).
% 12.04/2.23 fof(f6024,plain,(
% 12.04/2.23 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|~sQ651_spl|~sQ35_spl),
% 12.04/2.23 inference(paramodulation,[status(thm)],[f315,f6018])).
% 12.04/2.23 fof(f6030,plain,(
% 12.04/2.23 ~v4_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),sK1_skl)|~sQ28_spl|~sQ651_spl|~sQ35_spl|~sQ21_spl),
% 12.04/2.23 inference(paramodulation,[status(thm)],[f315,f6017])).
% 12.04/2.23 fof(f6099,plain,(
% 12.04/2.23 ![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))))),
% 12.04/2.23 inference(resolution,[status(thm)],[f564,f133])).
% 12.04/2.23 fof(f6107,definition,(
% 12.04/2.23 ![X0]: (sQ657_spl <=> (sP0_prd(sK2_skl,k3_xboole_0(sK2_skl,u1_struct_0(X0)),X0,sK0_skl)))),
% 12.04/2.23 introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition])).
% 12.04/2.23 fof(f6108,plain,(
% 12.04/2.23 ![X0]: (sP0_prd(sK2_skl,k3_xboole_0(sK2_skl,u1_struct_0(X0)),X0,sK0_skl)|~sQ657_spl)),
% 12.04/2.23 inference(component_clause,[status(thm)],[f6107])).
% 12.04/2.23 fof(f6110,plain,(
% 12.04/2.23 sQ657_spl|~sQ45_spl),
% 12.04/2.23 inference(split_clause,[status(thm)],[f6099,f6107,f894])).
% 12.04/2.23 fof(f6306,plain,(
% 12.04/2.23 ~m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))|v4_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),sK1_skl)|~sQ657_spl|~sQ121_spl),
% 12.04/2.23 inference(resolution,[status(thm)],[f6108,f1814])).
% 12.04/2.23 fof(f6317,definition,(
% 12.04/2.23 sQ676_spl <=> (m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 12.04/2.23 introduced(definition,[new_symbols(definition,[sQ676_spl])],[split_symbol_definition])).
% 12.04/2.23 fof(f6319,plain,(
% 12.04/2.23 ~m1_subset_1(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ676_spl),
% 12.04/2.23 inference(component_clause,[status(thm)],[f6317])).
% 12.04/2.23 fof(f6320,definition,(
% 12.04/2.23 sQ677_spl <=> (v4_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),sK1_skl))),
% 12.04/2.23 introduced(definition,[new_symbols(definition,[sQ677_spl])],[split_symbol_definition])).
% 12.04/2.23 fof(f6321,plain,(
% 12.04/2.23 v4_pre_topc(k3_xboole_0(sK2_skl,u1_struct_0(sK1_skl)),sK1_skl)|~sQ677_spl),
% 12.04/2.23 inference(component_clause,[status(thm)],[f6320])).
% 12.04/2.23 fof(f6323,plain,(
% 12.04/2.23 ~sQ676_spl|sQ677_spl|~sQ657_spl|~sQ121_spl),
% 12.04/2.23 inference(split_clause,[status(thm)],[f6306,f6317,f6320,f6107,f1813])).
% 12.04/2.23 fof(f6324,plain,(
% 12.04/2.23 $false|~sQ31_spl|~sQ28_spl|~sQ651_spl|~sQ35_spl|sQ676_spl),
% 12.04/2.23 inference(forward_subsumption_resolution,[status(thm)],[f6319,f6024])).
% 12.04/2.23 fof(f6325,plain,(
% 12.04/2.23 ~sQ31_spl|~sQ28_spl|~sQ651_spl|~sQ35_spl|sQ676_spl),
% 12.04/2.23 inference(contradiction_clause,[status(thm)],[f6324])).
% 12.04/2.23 fof(f6326,plain,(
% 12.04/2.23 $false|~sQ28_spl|~sQ651_spl|~sQ35_spl|~sQ21_spl|~sQ677_spl),
% 12.04/2.23 inference(forward_subsumption_resolution,[status(thm)],[f6321,f6030])).
% 12.04/2.23 fof(f6327,plain,(
% 12.04/2.23 ~sQ28_spl|~sQ651_spl|~sQ35_spl|~sQ21_spl|~sQ677_spl),
% 12.04/2.23 inference(contradiction_clause,[status(thm)],[f6326])).
% 12.04/2.23 fof(f6328,plain,(
% 12.04/2.23 $false),
% 12.04/2.23 inference(sat_refutation,[status(thm)],[f572,f574,f598,f600,f617,f652,f654,f662,f667,f669,f684,f689,f699,f711,f747,f764,f767,f769,f772,f788,f811,f830,f899,f1173,f1453,f1816,f2158,f2809,f4698,f5469,f5923,f5998,f6110,f6323,f6325,f6327])).
% 12.04/2.23 % SZS output end CNFRefutation for theBenchmark.p
% 12.04/2.25 % Elapsed time: 1.868592 seconds
% 12.04/2.25 % CPU time: 14.430157 seconds
% 12.04/2.25 % Total memory used: 319.151 MB
% 12.04/2.25 % Net memory used: 311.215 MB
%------------------------------------------------------------------------------