%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP034+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 : n002.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:44 PM UTC 2026
% Result : Theorem 0.20s 5.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : TOP034+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/5.43 % Computer : n002.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Mon Sep 21 12:45:08 UTC 2026
% 0.16/5.43 % CPUTime :
% 0.16/5.46 % Drodi V4.1.1
% 0.20/5.56 % Refutation found
% 0.20/5.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/5.56 % SZS output start CNFRefutation for theBenchmark
% 0.20/5.56 fof(f1,conjecture,(
% 0.20/5.56 (! [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) )=> r1_borsuk_1(A,B) ) )) )),
% 0.20/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/5.56 fof(f2,negated_conjecture,(
% 0.20/5.56 ~((! [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) )=> r1_borsuk_1(A,B) ) )) ))),
% 0.20/5.56 inference(negated_conjecture,[status(cth)],[f1])).
% 0.20/5.56 fof(f50,axiom,(
% 0.20/5.56 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( ( ~ v3_struct_0(B)& m1_pre_topc(B,A) )=> ( r1_borsuk_1(A,B)<=> (? [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))& v3_borsuk_1(C,A,B) ) )) ) )) )),
% 0.20/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/5.56 fof(f86,axiom,(
% 0.20/5.56 (! [A] :( l1_pre_topc(A)=> (! [B] :( m2_tsp_1(B,A)<=> m1_pre_topc(B,A) ) )) )),
% 0.20/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/5.56 fof(f89,axiom,(
% 0.20/5.56 (! [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))& v3_borsuk_1(C,A,B) ) )) )) )),
% 0.20/5.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/5.56 fof(f97,plain,(
% 0.20/5.56 (?[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))&~r1_borsuk_1(A,B)))))),
% 0.20/5.56 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.20/5.56 fof(f98,plain,(
% 0.20/5.56 (((~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))&~r1_borsuk_1(sK0_skl,sK1_skl)))),
% 0.20/5.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f97])).
% 0.20/5.56 fof(f99,plain,(
% 0.20/5.56 ~v3_struct_0(sK0_skl)),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f98])).
% 0.20/5.56 fof(f100,plain,(
% 0.20/5.56 v2_pre_topc(sK0_skl)),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f98])).
% 0.20/5.56 fof(f101,plain,(
% 0.20/5.56 l1_pre_topc(sK0_skl)),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f98])).
% 0.20/5.56 fof(f102,plain,(
% 0.20/5.56 ~v3_struct_0(sK1_skl)),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f98])).
% 0.20/5.56 fof(f103,plain,(
% 0.20/5.56 v2_tsp_2(sK1_skl,sK0_skl)),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f98])).
% 0.20/5.56 fof(f104,plain,(
% 0.20/5.56 m2_tsp_1(sK1_skl,sK0_skl)),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f98])).
% 0.20/5.56 fof(f105,plain,(
% 0.20/5.56 ~r1_borsuk_1(sK0_skl,sK1_skl)),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f98])).
% 0.20/5.56 fof(f286,plain,(
% 0.20/5.56 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: ((v3_struct_0(B)|~m1_pre_topc(B,A))|(r1_borsuk_1(A,B)<=>(?[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)))&v3_borsuk_1(C,A,B)))))))),
% 0.20/5.56 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.20/5.56 fof(f287,plain,(
% 0.20/5.56 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: ((v3_struct_0(B)|~m1_pre_topc(B,A))|((~r1_borsuk_1(A,B)|(?[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)))&v3_borsuk_1(C,A,B))))&(r1_borsuk_1(A,B)|(![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)))|~v3_borsuk_1(C,A,B))))))))),
% 0.20/5.56 inference(NNF_transformation,[status(thm)],[f286])).
% 0.20/5.56 fof(f288,plain,(
% 0.20/5.56 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: ((v3_struct_0(B)|~m1_pre_topc(B,A))|((~r1_borsuk_1(A,B)|((((v1_funct_1(sK2_skl(B,A))&v1_funct_2(sK2_skl(B,A),u1_struct_0(A),u1_struct_0(B)))&v5_pre_topc(sK2_skl(B,A),A,B))&m2_relset_1(sK2_skl(B,A),u1_struct_0(A),u1_struct_0(B)))&v3_borsuk_1(sK2_skl(B,A),A,B)))&(r1_borsuk_1(A,B)|(![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)))|~v3_borsuk_1(C,A,B))))))))),
% 0.20/5.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f287])).
% 0.20/5.56 fof(f294,plain,(
% 0.20/5.56 ![X0,X1,X2]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X1)|~m1_pre_topc(X1,X0)|r1_borsuk_1(X0,X1)|~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))|~v3_borsuk_1(X2,X0,X1))),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f288])).
% 0.20/5.56 fof(f402,plain,(
% 0.20/5.56 ![A]: (~l1_pre_topc(A)|(![B]: (m2_tsp_1(B,A)<=>m1_pre_topc(B,A))))),
% 0.20/5.56 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 0.20/5.56 fof(f403,plain,(
% 0.20/5.56 ![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)))))),
% 0.20/5.56 inference(NNF_transformation,[status(thm)],[f402])).
% 0.20/5.56 fof(f404,plain,(
% 0.20/5.56 ![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)))))),
% 0.20/5.56 inference(miniscoping,[status(thm)],[f403])).
% 0.20/5.56 fof(f405,plain,(
% 0.20/5.56 ![X0,X1]: (~l1_pre_topc(X0)|~m2_tsp_1(X1,X0)|m1_pre_topc(X1,X0))),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f404])).
% 0.20/5.56 fof(f411,plain,(
% 0.20/5.56 ![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)))&v3_borsuk_1(C,A,B))))))),
% 0.20/5.56 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 0.20/5.56 fof(f412,plain,(
% 0.20/5.56 ![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))|((((v1_funct_1(sK22_skl(B,A))&v1_funct_2(sK22_skl(B,A),u1_struct_0(A),u1_struct_0(B)))&v5_pre_topc(sK22_skl(B,A),A,B))&m2_relset_1(sK22_skl(B,A),u1_struct_0(A),u1_struct_0(B)))&v3_borsuk_1(sK22_skl(B,A),A,B)))))),
% 0.20/5.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(C,sK22_skl(B,A))],[f411])).
% 0.20/5.56 fof(f413,plain,(
% 0.20/5.56 ![X0,X1]: (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(sK22_skl(X1,X0)))),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f412])).
% 0.20/5.56 fof(f414,plain,(
% 0.20/5.56 ![X0,X1]: (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_2(sK22_skl(X1,X0),u1_struct_0(X0),u1_struct_0(X1)))),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f412])).
% 0.20/5.56 fof(f415,plain,(
% 0.20/5.56 ![X0,X1]: (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)|v5_pre_topc(sK22_skl(X1,X0),X0,X1))),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f412])).
% 0.20/5.56 fof(f416,plain,(
% 0.20/5.56 ![X0,X1]: (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)|m2_relset_1(sK22_skl(X1,X0),u1_struct_0(X0),u1_struct_0(X1)))),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f412])).
% 0.20/5.56 fof(f417,plain,(
% 0.20/5.56 ![X0,X1]: (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)|v3_borsuk_1(sK22_skl(X1,X0),X0,X1))),
% 0.20/5.56 inference(cnf_transformation,[status(thm)],[f412])).
% 0.20/5.56 fof(f440,definition,(
% 0.20/5.56 sQ0_spl <=> (l1_pre_topc(sK0_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f442,plain,(
% 0.20/5.56 ~l1_pre_topc(sK0_skl)|sQ0_spl),
% 0.20/5.56 inference(component_clause,[status(thm)],[f440])).
% 0.20/5.56 fof(f447,plain,(
% 0.20/5.56 $false|sQ0_spl),
% 0.20/5.56 inference(forward_subsumption_resolution,[status(thm)],[f442,f101])).
% 0.20/5.56 fof(f448,plain,(
% 0.20/5.56 sQ0_spl),
% 0.20/5.56 inference(contradiction_clause,[status(thm)],[f447])).
% 0.20/5.56 fof(f449,plain,(
% 0.20/5.56 ~l1_pre_topc(sK0_skl)|m1_pre_topc(sK1_skl,sK0_skl)),
% 0.20/5.56 inference(resolution,[status(thm)],[f405,f104])).
% 0.20/5.56 fof(f450,definition,(
% 0.20/5.56 sQ2_spl <=> (m1_pre_topc(sK1_skl,sK0_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f453,plain,(
% 0.20/5.56 ~sQ0_spl|sQ2_spl),
% 0.20/5.56 inference(split_clause,[status(thm)],[f449,f440,f450])).
% 0.20/5.56 fof(f473,definition,(
% 0.20/5.56 sQ6_spl <=> (v3_struct_0(sK0_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f474,plain,(
% 0.20/5.56 v3_struct_0(sK0_skl)|~sQ6_spl),
% 0.20/5.56 inference(component_clause,[status(thm)],[f473])).
% 0.20/5.56 fof(f476,definition,(
% 0.20/5.56 sQ7_spl <=> (v2_pre_topc(sK0_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f478,plain,(
% 0.20/5.56 ~v2_pre_topc(sK0_skl)|sQ7_spl),
% 0.20/5.56 inference(component_clause,[status(thm)],[f476])).
% 0.20/5.56 fof(f483,plain,(
% 0.20/5.56 $false|sQ7_spl),
% 0.20/5.56 inference(forward_subsumption_resolution,[status(thm)],[f478,f100])).
% 0.20/5.56 fof(f484,plain,(
% 0.20/5.56 sQ7_spl),
% 0.20/5.56 inference(contradiction_clause,[status(thm)],[f483])).
% 0.20/5.56 fof(f485,plain,(
% 0.20/5.56 $false|~sQ6_spl),
% 0.20/5.56 inference(forward_subsumption_resolution,[status(thm)],[f474,f99])).
% 0.20/5.56 fof(f486,plain,(
% 0.20/5.56 ~sQ6_spl),
% 0.20/5.56 inference(contradiction_clause,[status(thm)],[f485])).
% 0.20/5.56 fof(f535,plain,(
% 0.20/5.56 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(sK22_skl(sK1_skl,sK0_skl))),
% 0.20/5.56 inference(resolution,[status(thm)],[f413,f104])).
% 0.20/5.56 fof(f536,definition,(
% 0.20/5.56 sQ19_spl <=> (v3_struct_0(sK1_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f537,plain,(
% 0.20/5.56 v3_struct_0(sK1_skl)|~sQ19_spl),
% 0.20/5.56 inference(component_clause,[status(thm)],[f536])).
% 0.20/5.56 fof(f539,definition,(
% 0.20/5.56 sQ20_spl <=> (v2_tsp_2(sK1_skl,sK0_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f541,plain,(
% 0.20/5.56 ~v2_tsp_2(sK1_skl,sK0_skl)|sQ20_spl),
% 0.20/5.56 inference(component_clause,[status(thm)],[f539])).
% 0.20/5.56 fof(f542,definition,(
% 0.20/5.56 sQ21_spl <=> (v1_funct_1(sK22_skl(sK1_skl,sK0_skl)))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f545,plain,(
% 0.20/5.56 sQ6_spl|~sQ7_spl|~sQ0_spl|sQ19_spl|~sQ20_spl|sQ21_spl),
% 0.20/5.56 inference(split_clause,[status(thm)],[f535,f473,f476,f440,f536,f539,f542])).
% 0.20/5.56 fof(f546,plain,(
% 0.20/5.56 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)|v5_pre_topc(sK22_skl(sK1_skl,sK0_skl),sK0_skl,sK1_skl)),
% 0.20/5.56 inference(resolution,[status(thm)],[f415,f104])).
% 0.20/5.56 fof(f547,definition,(
% 0.20/5.56 sQ22_spl <=> (v5_pre_topc(sK22_skl(sK1_skl,sK0_skl),sK0_skl,sK1_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f550,plain,(
% 0.20/5.56 sQ6_spl|~sQ7_spl|~sQ0_spl|sQ19_spl|~sQ20_spl|sQ22_spl),
% 0.20/5.56 inference(split_clause,[status(thm)],[f546,f473,f476,f440,f536,f539,f547])).
% 0.20/5.56 fof(f551,plain,(
% 0.20/5.56 $false|sQ20_spl),
% 0.20/5.56 inference(forward_subsumption_resolution,[status(thm)],[f541,f103])).
% 0.20/5.56 fof(f552,plain,(
% 0.20/5.56 sQ20_spl),
% 0.20/5.56 inference(contradiction_clause,[status(thm)],[f551])).
% 0.20/5.56 fof(f553,plain,(
% 0.20/5.56 $false|~sQ19_spl),
% 0.20/5.56 inference(forward_subsumption_resolution,[status(thm)],[f537,f102])).
% 0.20/5.56 fof(f554,plain,(
% 0.20/5.56 ~sQ19_spl),
% 0.20/5.56 inference(contradiction_clause,[status(thm)],[f553])).
% 0.20/5.56 fof(f555,plain,(
% 0.20/5.56 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)|v3_borsuk_1(sK22_skl(sK1_skl,sK0_skl),sK0_skl,sK1_skl)),
% 0.20/5.56 inference(resolution,[status(thm)],[f417,f104])).
% 0.20/5.56 fof(f556,definition,(
% 0.20/5.56 sQ23_spl <=> (v3_borsuk_1(sK22_skl(sK1_skl,sK0_skl),sK0_skl,sK1_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f559,plain,(
% 0.20/5.56 sQ6_spl|~sQ7_spl|~sQ0_spl|sQ19_spl|~sQ20_spl|sQ23_spl),
% 0.20/5.56 inference(split_clause,[status(thm)],[f555,f473,f476,f440,f536,f539,f556])).
% 0.20/5.56 fof(f560,plain,(
% 0.20/5.56 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_2(sK22_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.20/5.56 inference(resolution,[status(thm)],[f414,f104])).
% 0.20/5.56 fof(f561,definition,(
% 0.20/5.56 sQ24_spl <=> (v1_funct_2(sK22_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f564,plain,(
% 0.20/5.56 sQ6_spl|~sQ7_spl|~sQ0_spl|sQ19_spl|~sQ20_spl|sQ24_spl),
% 0.20/5.56 inference(split_clause,[status(thm)],[f560,f473,f476,f440,f536,f539,f561])).
% 0.20/5.56 fof(f565,plain,(
% 0.20/5.56 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_relset_1(sK22_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.20/5.56 inference(resolution,[status(thm)],[f416,f104])).
% 0.20/5.56 fof(f566,definition,(
% 0.20/5.56 sQ25_spl <=> (m2_relset_1(sK22_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f567,plain,(
% 0.20/5.56 m2_relset_1(sK22_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~sQ25_spl),
% 0.20/5.56 inference(component_clause,[status(thm)],[f566])).
% 0.20/5.56 fof(f569,plain,(
% 0.20/5.56 sQ6_spl|~sQ7_spl|~sQ0_spl|sQ19_spl|~sQ20_spl|sQ25_spl),
% 0.20/5.56 inference(split_clause,[status(thm)],[f565,f473,f476,f440,f536,f539,f566])).
% 0.20/5.56 fof(f608,definition,(
% 0.20/5.56 sQ32_spl <=> (r1_borsuk_1(sK0_skl,sK1_skl))),
% 0.20/5.56 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.20/5.56 fof(f609,plain,(
% 0.20/5.56 r1_borsuk_1(sK0_skl,sK1_skl)|~sQ32_spl),
% 0.20/5.56 inference(component_clause,[status(thm)],[f608])).
% 0.20/5.56 fof(f703,plain,(
% 0.20/5.56 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)|r1_borsuk_1(sK0_skl,sK1_skl)|~v1_funct_1(sK22_skl(sK1_skl,sK0_skl))|~v1_funct_2(sK22_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v5_pre_topc(sK22_skl(sK1_skl,sK0_skl),sK0_skl,sK1_skl)|~v3_borsuk_1(sK22_skl(sK1_skl,sK0_skl),sK0_skl,sK1_skl)|~sQ25_spl),
% 0.20/5.56 inference(resolution,[status(thm)],[f567,f294])).
% 0.20/5.56 fof(f704,plain,(
% 0.20/5.56 sQ6_spl|~sQ7_spl|~sQ0_spl|sQ19_spl|~sQ2_spl|sQ32_spl|~sQ21_spl|~sQ24_spl|~sQ22_spl|~sQ23_spl|~sQ25_spl),
% 0.20/5.56 inference(split_clause,[status(thm)],[f703,f473,f476,f440,f536,f450,f608,f542,f561,f547,f556,f566])).
% 0.20/5.56 fof(f705,plain,(
% 0.20/5.56 $false|~sQ32_spl),
% 0.20/5.56 inference(forward_subsumption_resolution,[status(thm)],[f609,f105])).
% 0.20/5.56 fof(f706,plain,(
% 0.20/5.56 ~sQ32_spl),
% 0.20/5.56 inference(contradiction_clause,[status(thm)],[f705])).
% 0.20/5.56 fof(f707,plain,(
% 0.20/5.56 $false),
% 0.20/5.56 inference(sat_refutation,[status(thm)],[f448,f453,f484,f486,f545,f550,f552,f554,f559,f564,f569,f704,f706])).
% 0.20/5.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/5.61 % Elapsed time: 0.153812 seconds
% 0.20/5.61 % CPU time: 0.290444 seconds
% 0.20/5.61 % Total memory used: 90.426 MB
% 0.20/5.61 % Net memory used: 90.310 MB
%------------------------------------------------------------------------------