%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP023+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 : n006.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:41 PM UTC 2026
% Result : Theorem 1.11s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP023+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n006.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 12:38:12 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 1.11/0.87 % Refutation found
% 1.11/0.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.11/0.87 % SZS output start CNFRefutation for theBenchmark
% 1.11/0.87 fof(f1,conjecture,(
% 1.11/0.87 (! [A] :( l1_pre_topc(A)=> (! [B] :( l1_pre_topc(B)=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))=> ( ( g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) = g1_pre_topc(u1_struct_0(B),u1_pre_topc(B))& C = D& v1_tsp_2(C,A) )=> v1_tsp_2(D,B) ) ) )) )) )) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f2,negated_conjecture,(
% 1.11/0.87 ~((! [A] :( l1_pre_topc(A)=> (! [B] :( l1_pre_topc(B)=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))=> ( ( g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) = g1_pre_topc(u1_struct_0(B),u1_pre_topc(B))& C = D& v1_tsp_2(C,A) )=> v1_tsp_2(D,B) ) ) )) )) )) ))),
% 1.11/0.87 inference(negated_conjecture,[status(cth)],[f1])).
% 1.11/0.87 fof(f21,axiom,(
% 1.11/0.87 (! [A] :( l1_pre_topc(A)=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( v1_tsp_2(B,A)<=> ( v1_tsp_1(B,A)& (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> ( ( v1_tsp_1(C,A)& r1_tarski(B,C) )=> B = C ) ) )) ) ) )) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f22,axiom,(
% 1.11/0.87 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> ( v1_pre_topc(g1_pre_topc(A,B))& l1_pre_topc(g1_pre_topc(A,B)) ) ) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f28,axiom,(
% 1.11/0.87 (! [A] :( l1_pre_topc(A)=> m1_subset_1(u1_pre_topc(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) ) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f30,axiom,(
% 1.11/0.87 (? [A] : l1_pre_topc(A) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f32,axiom,(
% 1.11/0.87 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f33,axiom,(
% 1.11/0.87 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f35,axiom,(
% 1.11/0.87 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> (! [C,D] :( g1_pre_topc(A,B) = g1_pre_topc(C,D)=> ( A = C& B = D ) ) )) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f36,axiom,(
% 1.11/0.87 (? [A] :( ~ v1_xboole_0(A)& v1_membered(A)& v2_membered(A)& v3_membered(A)& v4_membered(A)& v5_membered(A) ) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f37,axiom,(
% 1.11/0.87 (? [A] :( l1_pre_topc(A)& v1_pre_topc(A) ) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f38,axiom,(
% 1.11/0.87 (! [A] :( ~ v1_xboole_0(A)=> (? [B] :( m1_subset_1(B,k1_zfmisc_1(A))& ~ v1_xboole_0(B) ) )) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f39,axiom,(
% 1.11/0.87 (! [A] :(? [B] :( m1_subset_1(B,k1_zfmisc_1(A))& v1_xboole_0(B) ) ))),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f47,axiom,(
% 1.11/0.87 (! [A] :( l1_pre_topc(A)=> (! [B] :( l1_pre_topc(B)=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))=> ( ( g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) = g1_pre_topc(u1_struct_0(B),u1_pre_topc(B))& C = D& v1_tsp_1(C,A) )=> v1_tsp_1(D,B) ) ) )) )) )) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f48,axiom,(
% 1.11/0.87 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 1.11/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.11/0.87 fof(f51,plain,(
% 1.11/0.87 (?[A]: (l1_pre_topc(A)&(?[B]: (l1_pre_topc(B)&(?[C]: (m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))&(?[D]: (m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))&(((g1_pre_topc(u1_struct_0(A),u1_pre_topc(A))=g1_pre_topc(u1_struct_0(B),u1_pre_topc(B))&C=D)&v1_tsp_2(C,A))&~v1_tsp_2(D,B))))))))))),
% 1.11/0.87 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 1.11/0.87 fof(f52,plain,(
% 1.11/0.87 (l1_pre_topc(sK0_skl)&(l1_pre_topc(sK1_skl)&(m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))&(m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))&(((g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))&sK2_skl=sK3_skl)&v1_tsp_2(sK2_skl,sK0_skl))&~v1_tsp_2(sK3_skl,sK1_skl))))))),
% 1.11/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f51])).
% 1.11/0.87 fof(f53,plain,(
% 1.11/0.87 l1_pre_topc(sK0_skl)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f52])).
% 1.11/0.87 fof(f54,plain,(
% 1.11/0.87 l1_pre_topc(sK1_skl)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f52])).
% 1.11/0.87 fof(f55,plain,(
% 1.11/0.87 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f52])).
% 1.11/0.87 fof(f56,plain,(
% 1.11/0.87 m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f52])).
% 1.11/0.87 fof(f57,plain,(
% 1.11/0.87 g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f52])).
% 1.11/0.87 fof(f58,plain,(
% 1.11/0.87 sK2_skl=sK3_skl),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f52])).
% 1.11/0.87 fof(f59,plain,(
% 1.11/0.87 v1_tsp_2(sK2_skl,sK0_skl)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f52])).
% 1.11/0.87 fof(f60,plain,(
% 1.11/0.87 ~v1_tsp_2(sK3_skl,sK1_skl)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f52])).
% 1.11/0.87 fof(f121,plain,(
% 1.11/0.87 ![A]: (~l1_pre_topc(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|(v1_tsp_2(B,A)<=>(v1_tsp_1(B,A)&(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))|((~v1_tsp_1(C,A)|~r1_tarski(B,C))|B=C))))))))),
% 1.11/0.87 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 1.11/0.87 fof(f122,plain,(
% 1.11/0.87 ![A]: (~l1_pre_topc(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|((~v1_tsp_2(B,A)|(v1_tsp_1(B,A)&(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))|((~v1_tsp_1(C,A)|~r1_tarski(B,C))|B=C)))))&(v1_tsp_2(B,A)|(~v1_tsp_1(B,A)|(?[C]: (m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))&((v1_tsp_1(C,A)&r1_tarski(B,C))&~B=C)))))))))),
% 1.11/0.87 inference(NNF_transformation,[status(thm)],[f121])).
% 1.11/0.87 fof(f123,plain,(
% 1.11/0.87 ![A]: (~l1_pre_topc(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|((~v1_tsp_2(B,A)|(v1_tsp_1(B,A)&(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))|((~v1_tsp_1(C,A)|~r1_tarski(B,C))|B=C)))))&(v1_tsp_2(B,A)|(~v1_tsp_1(B,A)|(m1_subset_1(sK4_skl(B,A),k1_zfmisc_1(u1_struct_0(A)))&((v1_tsp_1(sK4_skl(B,A),A)&r1_tarski(B,sK4_skl(B,A)))&~B=sK4_skl(B,A)))))))))),
% 1.11/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(C,sK4_skl(B,A))],[f122])).
% 1.11/0.87 fof(f124,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v1_tsp_2(X1,X0)|v1_tsp_1(X1,X0))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f123])).
% 1.11/0.87 fof(f125,plain,(
% 1.11/0.87 ![X0,X1,X2]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v1_tsp_2(X1,X0)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))|~v1_tsp_1(X2,X0)|~r1_tarski(X1,X2)|X1=X2)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f123])).
% 1.11/0.87 fof(f126,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f123])).
% 1.11/0.87 fof(f127,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|v1_tsp_1(sK4_skl(X1,X0),X0))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f123])).
% 1.11/0.87 fof(f128,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|r1_tarski(X1,sK4_skl(X1,X0)))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f123])).
% 1.11/0.87 fof(f129,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~X1=sK4_skl(X1,X0))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f123])).
% 1.11/0.87 fof(f130,plain,(
% 1.11/0.87 ![A,B]: (~m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))|(v1_pre_topc(g1_pre_topc(A,B))&l1_pre_topc(g1_pre_topc(A,B))))),
% 1.11/0.87 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 1.11/0.87 fof(f132,plain,(
% 1.11/0.87 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1)))|l1_pre_topc(g1_pre_topc(X1,X0)))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f130])).
% 1.11/0.87 fof(f135,plain,(
% 1.11/0.87 ![A]: (~l1_pre_topc(A)|m1_subset_1(u1_pre_topc(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))))),
% 1.11/0.87 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 1.11/0.87 fof(f136,plain,(
% 1.11/0.87 ![X0]: (~l1_pre_topc(X0)|m1_subset_1(u1_pre_topc(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f135])).
% 1.11/0.87 fof(f137,plain,(
% 1.11/0.87 l1_pre_topc(sK5_skl)),
% 1.11/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f30])).
% 1.11/0.87 fof(f138,plain,(
% 1.11/0.87 l1_pre_topc(sK5_skl)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f137])).
% 1.11/0.87 fof(f141,plain,(
% 1.11/0.87 ![A]: m1_subset_1(sK7_skl(A),A)),
% 1.11/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f32])).
% 1.11/0.87 fof(f142,plain,(
% 1.11/0.87 ![X0]: (m1_subset_1(sK7_skl(X0),X0))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f141])).
% 1.11/0.87 fof(f143,plain,(
% 1.11/0.87 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f33])).
% 1.11/0.87 fof(f150,plain,(
% 1.11/0.87 ![A,B]: (~m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))|(![C,D]: (~g1_pre_topc(A,B)=g1_pre_topc(C,D)|(A=C&B=D))))),
% 1.11/0.87 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 1.11/0.87 fof(f151,plain,(
% 1.11/0.87 ![X0,X1,X2,X3]: (~m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1)))|~g1_pre_topc(X1,X0)=g1_pre_topc(X2,X3)|X1=X2)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f150])).
% 1.11/0.87 fof(f152,plain,(
% 1.11/0.87 ![X0,X1,X2,X3]: (~m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1)))|~g1_pre_topc(X1,X0)=g1_pre_topc(X2,X3)|X0=X3)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f150])).
% 1.11/0.87 fof(f153,plain,(
% 1.11/0.87 (((((~v1_xboole_0(sK8_skl)&v1_membered(sK8_skl))&v2_membered(sK8_skl))&v3_membered(sK8_skl))&v4_membered(sK8_skl))&v5_membered(sK8_skl))),
% 1.11/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f36])).
% 1.11/0.87 fof(f154,plain,(
% 1.11/0.87 ~v1_xboole_0(sK8_skl)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f153])).
% 1.11/0.87 fof(f160,plain,(
% 1.11/0.87 (l1_pre_topc(sK9_skl)&v1_pre_topc(sK9_skl))),
% 1.11/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f37])).
% 1.11/0.87 fof(f161,plain,(
% 1.11/0.87 l1_pre_topc(sK9_skl)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f160])).
% 1.11/0.87 fof(f163,plain,(
% 1.11/0.87 ![A]: (v1_xboole_0(A)|(?[B]: (m1_subset_1(B,k1_zfmisc_1(A))&~v1_xboole_0(B))))),
% 1.11/0.87 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 1.11/0.87 fof(f164,plain,(
% 1.11/0.87 ![A]: (v1_xboole_0(A)|(m1_subset_1(sK10_skl(A),k1_zfmisc_1(A))&~v1_xboole_0(sK10_skl(A))))),
% 1.11/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B,sK10_skl(A))],[f163])).
% 1.11/0.87 fof(f165,plain,(
% 1.11/0.87 ![X0]: (v1_xboole_0(X0)|m1_subset_1(sK10_skl(X0),k1_zfmisc_1(X0)))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f164])).
% 1.11/0.87 fof(f167,plain,(
% 1.11/0.87 ![A]: (m1_subset_1(sK11_skl(A),k1_zfmisc_1(A))&v1_xboole_0(sK11_skl(A)))),
% 1.11/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(B,sK11_skl(A))],[f39])).
% 1.11/0.87 fof(f168,plain,(
% 1.11/0.87 ![X0]: (m1_subset_1(sK11_skl(X0),k1_zfmisc_1(X0)))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f167])).
% 1.11/0.87 fof(f169,plain,(
% 1.11/0.87 ![X0]: (v1_xboole_0(sK11_skl(X0)))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f167])).
% 1.11/0.87 fof(f196,plain,(
% 1.11/0.87 ![A]: (~l1_pre_topc(A)|(![B]: (~l1_pre_topc(B)|(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))|(![D]: (~m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))|(((~g1_pre_topc(u1_struct_0(A),u1_pre_topc(A))=g1_pre_topc(u1_struct_0(B),u1_pre_topc(B))|~C=D)|~v1_tsp_1(C,A))|v1_tsp_1(D,B)))))))))),
% 1.11/0.87 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 1.11/0.87 fof(f197,plain,(
% 1.11/0.87 ![X0,X1,X2,X3]: (~l1_pre_topc(X0)|~l1_pre_topc(X1)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))|~m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))|~X2=X3|~v1_tsp_1(X2,X0)|v1_tsp_1(X3,X1))),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f196])).
% 1.11/0.87 fof(f198,plain,(
% 1.11/0.87 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 1.11/0.87 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 1.11/0.87 fof(f199,plain,(
% 1.11/0.87 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 1.11/0.87 inference(cnf_transformation,[status(thm)],[f198])).
% 1.11/0.87 fof(f206,plain,(
% 1.11/0.87 ![X0,X1,X2]: (~l1_pre_topc(X0)|~l1_pre_topc(X1)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))|~v1_tsp_1(X2,X0)|v1_tsp_1(X2,X1))),
% 1.11/0.87 inference(destructive_equality_resolution,[status(thm)],[f197])).
% 1.11/0.87 fof(f207,plain,(
% 1.11/0.87 m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 1.11/0.87 inference(backward_demodulation,[status(thm)],[f58,f55])).
% 1.11/0.87 fof(f208,plain,(
% 1.11/0.87 v1_tsp_2(sK3_skl,sK0_skl)),
% 1.11/0.87 inference(forward_demodulation,[status(thm)],[f58,f59])).
% 1.11/0.87 fof(f209,plain,(
% 1.11/0.87 ~l1_pre_topc(sK0_skl)|~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|v1_tsp_1(sK3_skl,sK0_skl)),
% 1.11/0.87 inference(resolution,[status(thm)],[f124,f208])).
% 1.11/0.87 fof(f210,definition,(
% 1.11/0.87 sQ0_spl <=> (l1_pre_topc(sK0_skl))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f212,plain,(
% 1.11/0.87 ~l1_pre_topc(sK0_skl)|sQ0_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f210])).
% 1.11/0.87 fof(f213,definition,(
% 1.11/0.87 sQ1_spl <=> (m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f215,plain,(
% 1.11/0.87 ~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ1_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f213])).
% 1.11/0.87 fof(f216,definition,(
% 1.11/0.87 sQ2_spl <=> (v1_tsp_1(sK3_skl,sK0_skl))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f217,plain,(
% 1.11/0.87 v1_tsp_1(sK3_skl,sK0_skl)|~sQ2_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f216])).
% 1.11/0.87 fof(f219,plain,(
% 1.11/0.87 ~sQ0_spl|~sQ1_spl|sQ2_spl),
% 1.11/0.87 inference(split_clause,[status(thm)],[f209,f210,f213,f216])).
% 1.11/0.87 fof(f220,plain,(
% 1.11/0.87 ![X0]: (~l1_pre_topc(X0)|l1_pre_topc(g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))))),
% 1.11/0.87 inference(resolution,[status(thm)],[f136,f132])).
% 1.11/0.87 fof(f221,plain,(
% 1.11/0.87 ![X0,X1,X2]: (~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(X1,X2)|u1_struct_0(X0)=X1|~l1_pre_topc(X0))),
% 1.11/0.87 inference(resolution,[status(thm)],[f151,f136])).
% 1.11/0.87 fof(f222,plain,(
% 1.11/0.87 ![X0,X1,X2]: (~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(X1,X2)|u1_pre_topc(X0)=X2|~l1_pre_topc(X0))),
% 1.11/0.87 inference(resolution,[status(thm)],[f152,f136])).
% 1.11/0.87 fof(f232,plain,(
% 1.11/0.87 $false|sQ0_spl),
% 1.11/0.87 inference(forward_subsumption_resolution,[status(thm)],[f212,f53])).
% 1.11/0.87 fof(f233,plain,(
% 1.11/0.87 sQ0_spl),
% 1.11/0.87 inference(contradiction_clause,[status(thm)],[f232])).
% 1.11/0.87 fof(f234,plain,(
% 1.11/0.87 $false|sQ1_spl),
% 1.11/0.87 inference(forward_subsumption_resolution,[status(thm)],[f215,f207])).
% 1.11/0.87 fof(f235,plain,(
% 1.11/0.87 sQ1_spl),
% 1.11/0.87 inference(contradiction_clause,[status(thm)],[f234])).
% 1.11/0.87 fof(f238,plain,(
% 1.11/0.87 ![X0,X1]: (~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(X0,X1)|u1_struct_0(sK1_skl)=X0)),
% 1.11/0.87 inference(resolution,[status(thm)],[f221,f54])).
% 1.11/0.87 fof(f243,plain,(
% 1.11/0.87 ![X0,X1]: (~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(X0,X1)|u1_pre_topc(sK1_skl)=X1)),
% 1.11/0.87 inference(resolution,[status(thm)],[f222,f54])).
% 1.11/0.87 fof(f249,plain,(
% 1.11/0.87 ![X0]: (~l1_pre_topc(sK0_skl)|~l1_pre_topc(X0)|~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(X0)))|~g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))=g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))|v1_tsp_1(sK3_skl,X0)|~sQ2_spl)),
% 1.11/0.87 inference(resolution,[status(thm)],[f217,f206])).
% 1.11/0.87 fof(f250,definition,(
% 1.11/0.87 ![X0]: (sQ4_spl <=> (~l1_pre_topc(X0)|~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(X0)))|~g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))=g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))|v1_tsp_1(sK3_skl,X0)))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f251,plain,(
% 1.11/0.87 ![X0]: (~l1_pre_topc(X0)|~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(X0)))|~g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))=g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))|v1_tsp_1(sK3_skl,X0)|~sQ4_spl)),
% 1.11/0.87 inference(component_clause,[status(thm)],[f250])).
% 1.11/0.87 fof(f253,plain,(
% 1.11/0.87 ~sQ0_spl|sQ4_spl|~sQ1_spl|~sQ2_spl),
% 1.11/0.87 inference(split_clause,[status(thm)],[f249,f210,f250,f213,f216])).
% 1.11/0.87 fof(f254,plain,(
% 1.11/0.87 ![X0]: (~l1_pre_topc(X0)|~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(X0)))|~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))|v1_tsp_1(sK3_skl,X0)|~sQ4_spl)),
% 1.11/0.87 inference(forward_demodulation,[status(thm)],[f57,f251])).
% 1.11/0.87 fof(f285,plain,(
% 1.11/0.87 u1_struct_0(sK1_skl)=u1_struct_0(sK0_skl)),
% 1.11/0.87 inference(resolution,[status(thm)],[f238,f57])).
% 1.11/0.87 fof(f288,definition,(
% 1.11/0.87 sQ6_spl <=> (g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl)))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f290,plain,(
% 1.11/0.87 ~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))|sQ6_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f288])).
% 1.11/0.87 fof(f295,plain,(
% 1.11/0.87 $false|sQ6_spl),
% 1.11/0.87 inference(trivial_equality_resolution,[status(thm)],[f290])).
% 1.11/0.87 fof(f296,plain,(
% 1.11/0.87 sQ6_spl),
% 1.11/0.87 inference(contradiction_clause,[status(thm)],[f295])).
% 1.11/0.87 fof(f300,plain,(
% 1.11/0.87 g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK0_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))),
% 1.11/0.87 inference(backward_demodulation,[status(thm)],[f285,f57])).
% 1.11/0.87 fof(f358,plain,(
% 1.11/0.87 u1_pre_topc(sK1_skl)=u1_pre_topc(sK0_skl)),
% 1.11/0.87 inference(resolution,[status(thm)],[f243,f300])).
% 1.11/0.87 fof(f405,plain,(
% 1.11/0.87 ~l1_pre_topc(sK1_skl)|~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))|v1_tsp_1(sK3_skl,sK1_skl)|~sQ4_spl),
% 1.11/0.87 inference(resolution,[status(thm)],[f254,f56])).
% 1.11/0.87 fof(f407,definition,(
% 1.11/0.87 sQ22_spl <=> (l1_pre_topc(sK1_skl))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f409,plain,(
% 1.11/0.87 ~l1_pre_topc(sK1_skl)|sQ22_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f407])).
% 1.11/0.87 fof(f410,definition,(
% 1.11/0.87 sQ23_spl <=> (v1_tsp_1(sK3_skl,sK1_skl))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f411,plain,(
% 1.11/0.87 v1_tsp_1(sK3_skl,sK1_skl)|~sQ23_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f410])).
% 1.11/0.87 fof(f413,plain,(
% 1.11/0.87 ~sQ22_spl|~sQ6_spl|sQ23_spl|~sQ4_spl),
% 1.11/0.87 inference(split_clause,[status(thm)],[f405,f407,f288,f410,f250])).
% 1.11/0.87 fof(f414,definition,(
% 1.11/0.87 sQ24_spl <=> (m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f416,plain,(
% 1.11/0.87 ~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ24_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f414])).
% 1.11/0.87 fof(f417,definition,(
% 1.11/0.87 sQ25_spl <=> (g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl)))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f419,plain,(
% 1.11/0.87 ~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))|sQ25_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f417])).
% 1.11/0.87 fof(f421,plain,(
% 1.11/0.87 $false|sQ22_spl),
% 1.11/0.87 inference(forward_subsumption_resolution,[status(thm)],[f409,f54])).
% 1.11/0.87 fof(f422,plain,(
% 1.11/0.87 sQ22_spl),
% 1.11/0.87 inference(contradiction_clause,[status(thm)],[f421])).
% 1.11/0.87 fof(f429,plain,(
% 1.11/0.87 $false|sQ24_spl),
% 1.11/0.87 inference(forward_subsumption_resolution,[status(thm)],[f416,f56])).
% 1.11/0.87 fof(f430,plain,(
% 1.11/0.87 sQ24_spl),
% 1.11/0.87 inference(contradiction_clause,[status(thm)],[f429])).
% 1.11/0.87 fof(f488,plain,(
% 1.11/0.87 ![X0]: (~l1_pre_topc(sK0_skl)|~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v1_tsp_1(X0,sK0_skl)|~r1_tarski(sK3_skl,X0)|sK3_skl=X0)),
% 1.11/0.87 inference(resolution,[status(thm)],[f125,f208])).
% 1.11/0.87 fof(f489,definition,(
% 1.11/0.87 ![X0]: (sQ27_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v1_tsp_1(X0,sK0_skl)|~r1_tarski(sK3_skl,X0)|sK3_skl=X0))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f490,plain,(
% 1.11/0.87 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v1_tsp_1(X0,sK0_skl)|~r1_tarski(sK3_skl,X0)|sK3_skl=X0|~sQ27_spl)),
% 1.11/0.87 inference(component_clause,[status(thm)],[f489])).
% 1.11/0.87 fof(f492,plain,(
% 1.11/0.87 ~sQ0_spl|~sQ1_spl|sQ27_spl),
% 1.11/0.87 inference(split_clause,[status(thm)],[f488,f210,f213,f489])).
% 1.11/0.87 fof(f493,plain,(
% 1.11/0.87 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|~v1_tsp_1(X0,sK0_skl)|~r1_tarski(sK3_skl,X0)|sK3_skl=X0|~sQ27_spl)),
% 1.11/0.87 inference(forward_demodulation,[status(thm)],[f285,f490])).
% 1.11/0.87 fof(f501,plain,(
% 1.11/0.87 ![X0,X1,X2]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~l1_pre_topc(X0)|~l1_pre_topc(X2)|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(X0)))|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(X2)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))|v1_tsp_1(sK4_skl(X1,X0),X2))),
% 1.11/0.87 inference(resolution,[status(thm)],[f127,f206])).
% 1.11/0.87 fof(f502,plain,(
% 1.11/0.87 ![X0,X1,X2]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~l1_pre_topc(X2)|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(X0)))|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(X2)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))|v1_tsp_1(sK4_skl(X1,X0),X2))),
% 1.11/0.87 inference(duplicate_literals_removal,[status(thm)],[f501])).
% 1.11/0.87 fof(f503,plain,(
% 1.11/0.87 ![X0,X1,X2]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~l1_pre_topc(X2)|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(X2)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))|v1_tsp_1(sK4_skl(X1,X0),X2))),
% 1.11/0.87 inference(forward_subsumption_resolution,[status(thm)],[f502,f126])).
% 1.11/0.87 fof(f526,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~l1_pre_topc(sK0_skl)|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))|v1_tsp_1(sK4_skl(X1,X0),sK0_skl))),
% 1.11/0.87 inference(paramodulation,[status(thm)],[f285,f503])).
% 1.11/0.87 fof(f529,definition,(
% 1.11/0.87 ![X0,X1]: (sQ32_spl <=> (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))|v1_tsp_1(sK4_skl(X1,X0),sK0_skl)))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f530,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(sK0_skl),u1_pre_topc(sK0_skl))|v1_tsp_1(sK4_skl(X1,X0),sK0_skl)|~sQ32_spl)),
% 1.11/0.87 inference(component_clause,[status(thm)],[f529])).
% 1.11/0.87 fof(f532,plain,(
% 1.11/0.87 sQ32_spl|~sQ0_spl),
% 1.11/0.87 inference(split_clause,[status(thm)],[f526,f529,f210])).
% 1.11/0.87 fof(f533,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK0_skl))|v1_tsp_1(sK4_skl(X1,X0),sK0_skl)|~sQ32_spl)),
% 1.11/0.87 inference(forward_demodulation,[status(thm)],[f285,f530])).
% 1.11/0.87 fof(f534,plain,(
% 1.11/0.87 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_2(X1,X0)|~v1_tsp_1(X1,X0)|~m1_subset_1(sK4_skl(X1,X0),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))|v1_tsp_1(sK4_skl(X1,X0),sK0_skl)|~sQ32_spl)),
% 1.11/0.87 inference(forward_demodulation,[status(thm)],[f358,f533])).
% 1.11/0.87 fof(f540,definition,(
% 1.11/0.87 sQ33_spl <=> (v1_tsp_2(sK3_skl,sK1_skl))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f541,plain,(
% 1.11/0.87 v1_tsp_2(sK3_skl,sK1_skl)|~sQ33_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f540])).
% 1.11/0.87 fof(f543,definition,(
% 1.11/0.87 sQ34_spl <=> (sK3_skl=sK4_skl(sK3_skl,sK1_skl))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f554,plain,(
% 1.11/0.87 $false|~sQ33_spl),
% 1.11/0.87 inference(forward_subsumption_resolution,[status(thm)],[f541,f60])).
% 1.11/0.87 fof(f555,plain,(
% 1.11/0.87 ~sQ33_spl),
% 1.11/0.87 inference(contradiction_clause,[status(thm)],[f554])).
% 1.11/0.87 fof(f562,plain,(
% 1.11/0.87 ![X0]: (l1_pre_topc(g1_pre_topc(X0,sK7_skl(k1_zfmisc_1(k1_zfmisc_1(X0))))))),
% 1.11/0.87 inference(resolution,[status(thm)],[f142,f132])).
% 1.11/0.87 fof(f666,definition,(
% 1.11/0.87 sQ39_spl <=> (l1_pre_topc(sK9_skl))),
% 1.11/0.87 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 1.11/0.87 fof(f668,plain,(
% 1.11/0.87 ~l1_pre_topc(sK9_skl)|sQ39_spl),
% 1.11/0.87 inference(component_clause,[status(thm)],[f666])).
% 1.11/0.87 fof(f673,plain,(
% 1.11/0.87 $false|sQ39_spl),
% 1.11/0.87 inference(forward_subsumption_resolution,[status(thm)],[f668,f161])).
% 1.11/0.87 fof(f674,plain,(
% 1.11/0.87 sQ39_spl),
% 1.11/0.87 inference(contradiction_clause,[status(thm)],[f673])).
% 1.11/0.87 fof(f678,plain,(
% 1.11/0.87 ![X0]: (v1_xboole_0(k1_zfmisc_1(X0))|l1_pre_topc(g1_pre_topc(X0,sK10_skl(k1_zfmisc_1(X0)))))),
% 1.11/0.87 inference(resolution,[status(thm)],[f165,f132])).
% 1.11/0.87 fof(f683,plain,(
% 1.11/0.87 ![X0]: (l1_pre_topc(g1_pre_topc(X0,sK10_skl(k1_zfmisc_1(X0)))))),
% 1.11/0.87 inference(forward_subsumption_resolution,[status(thm)],[f678,f143])).
% 1.11/0.87 fof(f779,definition,(
% 1.11/0.87 sQ43_spl <=> (sK9_skl=sK9_skl)),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f781,plain,(
% 1.11/0.88 ~sK9_skl=sK9_skl|sQ43_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f779])).
% 1.11/0.88 fof(f786,plain,(
% 1.11/0.88 $false|sQ43_spl),
% 1.11/0.88 inference(trivial_equality_resolution,[status(thm)],[f781])).
% 1.11/0.88 fof(f787,plain,(
% 1.11/0.88 sQ43_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f786])).
% 1.11/0.88 fof(f792,plain,(
% 1.11/0.88 ![X0]: (l1_pre_topc(g1_pre_topc(X0,sK11_skl(k1_zfmisc_1(X0)))))),
% 1.11/0.88 inference(resolution,[status(thm)],[f168,f132])).
% 1.11/0.88 fof(f862,plain,(
% 1.11/0.88 ![X0]: (~l1_pre_topc(sK1_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))|v1_tsp_1(sK4_skl(X0,sK1_skl),sK0_skl)|~l1_pre_topc(sK1_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|~sQ32_spl)),
% 1.11/0.88 inference(resolution,[status(thm)],[f534,f126])).
% 1.11/0.88 fof(f863,definition,(
% 1.11/0.88 ![X0]: (sQ48_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|v1_tsp_1(sK4_skl(X0,sK1_skl),sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f864,plain,(
% 1.11/0.88 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|v1_tsp_1(sK4_skl(X0,sK1_skl),sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|~sQ48_spl)),
% 1.11/0.88 inference(component_clause,[status(thm)],[f863])).
% 1.11/0.88 fof(f866,plain,(
% 1.11/0.88 ~sQ22_spl|sQ48_spl|~sQ6_spl|~sQ32_spl),
% 1.11/0.88 inference(split_clause,[status(thm)],[f862,f407,f863,f288,f529])).
% 1.11/0.88 fof(f867,plain,(
% 1.11/0.88 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|v1_tsp_1(sK4_skl(X0,sK1_skl),sK0_skl)|~sQ48_spl)),
% 1.11/0.88 inference(duplicate_literals_removal,[status(thm)],[f864])).
% 1.11/0.88 fof(f920,definition,(
% 1.11/0.88 sQ50_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK1_skl)))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f921,plain,(
% 1.11/0.88 v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK1_skl))))|~sQ50_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f920])).
% 1.11/0.88 fof(f928,definition,(
% 1.11/0.88 sQ52_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f929,plain,(
% 1.11/0.88 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK1_skl)))|~sQ52_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f928])).
% 1.11/0.88 fof(f936,plain,(
% 1.11/0.88 $false|~sQ50_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f921,f143])).
% 1.11/0.88 fof(f937,plain,(
% 1.11/0.88 ~sQ50_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f936])).
% 1.11/0.88 fof(f938,plain,(
% 1.11/0.88 $false|~sQ52_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f929,f143])).
% 1.11/0.88 fof(f939,plain,(
% 1.11/0.88 ~sQ52_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f938])).
% 1.11/0.88 fof(f941,plain,(
% 1.11/0.88 ![X0]: (sK11_skl(X0)=k1_xboole_0)),
% 1.11/0.88 inference(resolution,[status(thm)],[f199,f169])).
% 1.11/0.88 fof(f1284,definition,(
% 1.11/0.88 sQ71_spl <=> (l1_pre_topc(g1_pre_topc(u1_struct_0(sK5_skl),u1_pre_topc(sK5_skl))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f1286,plain,(
% 1.11/0.88 ~l1_pre_topc(g1_pre_topc(u1_struct_0(sK5_skl),u1_pre_topc(sK5_skl)))|sQ71_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f1284])).
% 1.11/0.88 fof(f1308,definition,(
% 1.11/0.88 sQ77_spl <=> (g1_pre_topc(u1_struct_0(sK5_skl),u1_pre_topc(sK5_skl))=g1_pre_topc(u1_struct_0(sK5_skl),u1_pre_topc(sK5_skl)))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f1310,plain,(
% 1.11/0.88 ~g1_pre_topc(u1_struct_0(sK5_skl),u1_pre_topc(sK5_skl))=g1_pre_topc(u1_struct_0(sK5_skl),u1_pre_topc(sK5_skl))|sQ77_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f1308])).
% 1.11/0.88 fof(f1323,plain,(
% 1.11/0.88 $false|sQ77_spl),
% 1.11/0.88 inference(trivial_equality_resolution,[status(thm)],[f1310])).
% 1.11/0.88 fof(f1324,plain,(
% 1.11/0.88 sQ77_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f1323])).
% 1.11/0.88 fof(f1344,plain,(
% 1.11/0.88 ~l1_pre_topc(sK5_skl)|sQ71_spl),
% 1.11/0.88 inference(resolution,[status(thm)],[f1286,f220])).
% 1.11/0.88 fof(f1345,plain,(
% 1.11/0.88 $false|sQ71_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1344,f138])).
% 1.11/0.88 fof(f1346,plain,(
% 1.11/0.88 sQ71_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f1345])).
% 1.11/0.88 fof(f1685,plain,(
% 1.11/0.88 ~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(sK3_skl,sK1_skl)|v1_tsp_1(sK4_skl(sK3_skl,sK1_skl),sK0_skl)|~sQ48_spl|~sQ23_spl),
% 1.11/0.88 inference(resolution,[status(thm)],[f867,f411])).
% 1.11/0.88 fof(f1690,definition,(
% 1.11/0.88 sQ99_spl <=> (v1_tsp_1(sK4_skl(sK3_skl,sK1_skl),sK0_skl))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f1691,plain,(
% 1.11/0.88 v1_tsp_1(sK4_skl(sK3_skl,sK1_skl),sK0_skl)|~sQ99_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f1690])).
% 1.11/0.88 fof(f1693,plain,(
% 1.11/0.88 ~sQ24_spl|sQ33_spl|sQ99_spl|~sQ48_spl|~sQ23_spl),
% 1.11/0.88 inference(split_clause,[status(thm)],[f1685,f414,f540,f1690,f863,f410])).
% 1.11/0.88 fof(f1845,definition,(
% 1.11/0.88 sQ109_spl <=> (v1_xboole_0(sK8_skl))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f1846,plain,(
% 1.11/0.88 v1_xboole_0(sK8_skl)|~sQ109_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f1845])).
% 1.11/0.88 fof(f1858,plain,(
% 1.11/0.88 $false|~sQ109_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1846,f154])).
% 1.11/0.88 fof(f1859,plain,(
% 1.11/0.88 ~sQ109_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f1858])).
% 1.11/0.88 fof(f3416,plain,(
% 1.11/0.88 ![X0]: (l1_pre_topc(g1_pre_topc(X0,k1_xboole_0)))),
% 1.11/0.88 inference(backward_demodulation,[status(thm)],[f941,f792])).
% 1.11/0.88 fof(f3629,definition,(
% 1.11/0.88 ![X0]: (sQ183_spl <=> (~l1_pre_topc(X0)))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f3630,plain,(
% 1.11/0.88 ![X0]: (~l1_pre_topc(X0)|~sQ183_spl)),
% 1.11/0.88 inference(component_clause,[status(thm)],[f3629])).
% 1.11/0.88 fof(f3799,definition,(
% 1.11/0.88 ![X0]: (sQ194_spl <=> (~l1_pre_topc(g1_pre_topc(X0,k1_xboole_0))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f3800,plain,(
% 1.11/0.88 ![X0]: (~l1_pre_topc(g1_pre_topc(X0,k1_xboole_0))|~sQ194_spl)),
% 1.11/0.88 inference(component_clause,[status(thm)],[f3799])).
% 1.11/0.88 fof(f3920,definition,(
% 1.11/0.88 ![X0]: (sQ205_spl <=> (~l1_pre_topc(g1_pre_topc(X0,sK10_skl(k1_zfmisc_1(X0))))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f3921,plain,(
% 1.11/0.88 ![X0]: (~l1_pre_topc(g1_pre_topc(X0,sK10_skl(k1_zfmisc_1(X0))))|~sQ205_spl)),
% 1.11/0.88 inference(component_clause,[status(thm)],[f3920])).
% 1.11/0.88 fof(f3965,definition,(
% 1.11/0.88 ![X0]: (sQ206_spl <=> (~l1_pre_topc(g1_pre_topc(X0,sK7_skl(k1_zfmisc_1(k1_zfmisc_1(X0)))))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f3966,plain,(
% 1.11/0.88 ![X0]: (~l1_pre_topc(g1_pre_topc(X0,sK7_skl(k1_zfmisc_1(k1_zfmisc_1(X0)))))|~sQ206_spl)),
% 1.11/0.88 inference(component_clause,[status(thm)],[f3965])).
% 1.11/0.88 fof(f4103,definition,(
% 1.11/0.88 sQ227_spl <=> (l1_pre_topc(sK5_skl))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f4105,plain,(
% 1.11/0.88 ~l1_pre_topc(sK5_skl)|sQ227_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f4103])).
% 1.11/0.88 fof(f4110,definition,(
% 1.11/0.88 sQ229_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK5_skl))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f4111,plain,(
% 1.11/0.88 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK5_skl)))|~sQ229_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f4110])).
% 1.11/0.88 fof(f4114,plain,(
% 1.11/0.88 $false|sQ227_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f4105,f138])).
% 1.11/0.88 fof(f4115,plain,(
% 1.11/0.88 sQ227_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f4114])).
% 1.11/0.88 fof(f4122,definition,(
% 1.11/0.88 sQ230_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK5_skl)))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f4123,plain,(
% 1.11/0.88 v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK5_skl))))|~sQ230_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f4122])).
% 1.11/0.88 fof(f4129,plain,(
% 1.11/0.88 $false|~sQ230_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f4123,f143])).
% 1.11/0.88 fof(f4130,plain,(
% 1.11/0.88 ~sQ230_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f4129])).
% 1.11/0.88 fof(f6081,plain,(
% 1.11/0.88 ~m1_subset_1(sK4_skl(sK3_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r1_tarski(sK3_skl,sK4_skl(sK3_skl,sK1_skl))|sK3_skl=sK4_skl(sK3_skl,sK1_skl)|~sQ99_spl|~sQ27_spl),
% 1.11/0.88 inference(resolution,[status(thm)],[f1691,f493])).
% 1.11/0.88 fof(f6096,definition,(
% 1.11/0.88 sQ242_spl <=> (m1_subset_1(sK4_skl(sK3_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f6111,definition,(
% 1.11/0.88 sQ246_spl <=> (r1_tarski(sK3_skl,sK4_skl(sK3_skl,sK1_skl)))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f6114,plain,(
% 1.11/0.88 ~sQ242_spl|~sQ246_spl|sQ34_spl|~sQ99_spl|~sQ27_spl),
% 1.11/0.88 inference(split_clause,[status(thm)],[f6081,f6096,f6111,f543,f1690,f489])).
% 1.11/0.88 fof(f6341,plain,(
% 1.11/0.88 $false|~sQ206_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f3966,f562])).
% 1.11/0.88 fof(f6342,plain,(
% 1.11/0.88 ~sQ206_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f6341])).
% 1.11/0.88 fof(f6343,plain,(
% 1.11/0.88 $false|~sQ205_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f3921,f683])).
% 1.11/0.88 fof(f6344,plain,(
% 1.11/0.88 ~sQ205_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f6343])).
% 1.11/0.88 fof(f6345,plain,(
% 1.11/0.88 $false|~sQ194_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f3800,f3416])).
% 1.11/0.88 fof(f6346,plain,(
% 1.11/0.88 ~sQ194_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f6345])).
% 1.11/0.88 fof(f6458,plain,(
% 1.11/0.88 $false|~sQ183_spl),
% 1.11/0.88 inference(backward_subsumption_resolution,[status(thm)],[f161,f3630])).
% 1.11/0.88 fof(f6467,plain,(
% 1.11/0.88 ~sQ183_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f6458])).
% 1.11/0.88 fof(f6568,plain,(
% 1.11/0.88 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|~X0=sK4_skl(X0,sK1_skl))),
% 1.11/0.88 inference(resolution,[status(thm)],[f129,f54])).
% 1.11/0.88 fof(f6571,plain,(
% 1.11/0.88 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|r1_tarski(X0,sK4_skl(X0,sK1_skl)))),
% 1.11/0.88 inference(resolution,[status(thm)],[f128,f54])).
% 1.11/0.88 fof(f6609,plain,(
% 1.11/0.88 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(X0,sK1_skl)|~v1_tsp_1(X0,sK1_skl)|m1_subset_1(sK4_skl(X0,sK1_skl),k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 1.11/0.88 inference(resolution,[status(thm)],[f126,f54])).
% 1.11/0.88 fof(f6625,plain,(
% 1.11/0.88 ~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK0_skl))|sQ25_spl),
% 1.11/0.88 inference(forward_demodulation,[status(thm)],[f285,f419])).
% 1.11/0.88 fof(f6626,plain,(
% 1.11/0.88 ~g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))=g1_pre_topc(u1_struct_0(sK1_skl),u1_pre_topc(sK1_skl))|sQ25_spl),
% 1.11/0.88 inference(forward_demodulation,[status(thm)],[f358,f6625])).
% 1.11/0.88 fof(f6627,plain,(
% 1.11/0.88 $false|sQ25_spl),
% 1.11/0.88 inference(trivial_equality_resolution,[status(thm)],[f6626])).
% 1.11/0.88 fof(f6628,plain,(
% 1.11/0.88 sQ25_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f6627])).
% 1.11/0.88 fof(f6787,definition,(
% 1.11/0.88 sQ281_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK9_skl)))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f6788,plain,(
% 1.11/0.88 v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK9_skl))))|~sQ281_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f6787])).
% 1.11/0.88 fof(f6794,plain,(
% 1.11/0.88 $false|~sQ281_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f6788,f143])).
% 1.11/0.88 fof(f6795,plain,(
% 1.11/0.88 ~sQ281_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f6794])).
% 1.11/0.88 fof(f7034,plain,(
% 1.11/0.88 $false|~sQ229_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f4111,f143])).
% 1.11/0.88 fof(f7035,plain,(
% 1.11/0.88 ~sQ229_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f7034])).
% 1.11/0.88 fof(f7128,definition,(
% 1.11/0.88 sQ295_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK9_skl))))),
% 1.11/0.88 introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition])).
% 1.11/0.88 fof(f7129,plain,(
% 1.11/0.88 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK9_skl)))|~sQ295_spl),
% 1.11/0.88 inference(component_clause,[status(thm)],[f7128])).
% 1.11/0.88 fof(f7135,plain,(
% 1.11/0.88 $false|~sQ295_spl),
% 1.11/0.88 inference(forward_subsumption_resolution,[status(thm)],[f7129,f143])).
% 1.11/0.88 fof(f7136,plain,(
% 1.11/0.88 ~sQ295_spl),
% 1.11/0.88 inference(contradiction_clause,[status(thm)],[f7135])).
% 1.11/0.88 fof(f7232,plain,(
% 1.11/0.88 ~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(sK3_skl,sK1_skl)|~sK3_skl=sK4_skl(sK3_skl,sK1_skl)|~sQ23_spl),
% 1.11/0.88 inference(resolution,[status(thm)],[f6568,f411])).
% 1.11/0.88 fof(f7233,plain,(
% 1.11/0.88 ~sQ24_spl|sQ33_spl|~sQ34_spl|~sQ23_spl),
% 1.11/0.88 inference(split_clause,[status(thm)],[f7232,f414,f540,f543,f410])).
% 1.11/0.88 fof(f7289,plain,(
% 1.11/0.88 ~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(sK3_skl,sK1_skl)|r1_tarski(sK3_skl,sK4_skl(sK3_skl,sK1_skl))|~sQ23_spl),
% 1.11/0.88 inference(resolution,[status(thm)],[f6571,f411])).
% 1.11/0.88 fof(f7290,plain,(
% 1.11/0.88 ~sQ24_spl|sQ33_spl|sQ246_spl|~sQ23_spl),
% 1.11/0.88 inference(split_clause,[status(thm)],[f7289,f414,f540,f6111,f410])).
% 1.11/0.88 fof(f7349,plain,(
% 1.11/0.88 ~m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK1_skl)))|v1_tsp_2(sK3_skl,sK1_skl)|m1_subset_1(sK4_skl(sK3_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~sQ23_spl),
% 1.11/0.88 inference(resolution,[status(thm)],[f6609,f411])).
% 1.11/0.88 fof(f7350,plain,(
% 1.11/0.88 ~sQ24_spl|sQ33_spl|sQ242_spl|~sQ23_spl),
% 1.11/0.88 inference(split_clause,[status(thm)],[f7349,f414,f540,f6096,f410])).
% 1.11/0.88 fof(f7351,plain,(
% 1.11/0.88 $false),
% 1.11/0.88 inference(sat_refutation,[status(thm)],[f219,f233,f235,f253,f296,f413,f422,f430,f492,f532,f555,f674,f787,f866,f937,f939,f1324,f1346,f1693,f1859,f4115,f4130,f6114,f6342,f6344,f6346,f6467,f6628,f6795,f7035,f7136,f7233,f7290,f7350])).
% 1.11/0.88 % SZS output end CNFRefutation for theBenchmark.p
% 2.64/0.92 % Elapsed time: 0.526581 seconds
% 2.64/0.92 % CPU time: 3.843822 seconds
% 2.64/0.92 % Total memory used: 203.648 MB
% 2.64/0.92 % Net memory used: 201.360 MB
%------------------------------------------------------------------------------