%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP035+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:53:44 PM UTC 2026
% Result : Theorem 0.17s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP035+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.46 % Computer : n018.cluster.edu
% 0.17/0.46 % Model : x86_64 x86_64
% 0.17/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.46 % Memory : 8046.5625MB
% 0.17/0.46 % OS : Linux 6.8.0-71-generic
% 0.17/0.46 % CPULimit : 300
% 0.17/0.46 % WCLimit : 300
% 0.17/0.46 % DateTime : Mon Sep 21 12:44:30 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.17/0.52 % Drodi V4.1.1
% 0.17/0.56 % Refutation found
% 0.17/0.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.56 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.56 fof(f1,conjecture,(
% 0.17/0.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] :( m1_subset_1(C,u1_struct_0(A))=> (! [D] :( m1_subset_1(D,u1_struct_0(B))=> ( C = D=> k5_pre_topc(A,B,k1_tsp_2(A,B),k6_pre_topc(B,k1_struct_0(B,D))) = k6_pre_topc(A,k1_struct_0(A,C)) ) ) )) )) )) )),
% 0.17/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f2,negated_conjecture,(
% 0.17/0.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] :( m1_subset_1(C,u1_struct_0(A))=> (! [D] :( m1_subset_1(D,u1_struct_0(B))=> ( C = D=> k5_pre_topc(A,B,k1_tsp_2(A,B),k6_pre_topc(B,k1_struct_0(B,D))) = k6_pre_topc(A,k1_struct_0(A,C)) ) ) )) )) )) ))),
% 0.17/0.56 inference(negated_conjecture,[status(cth)],[f1])).
% 0.17/0.56 fof(f50,axiom,(
% 0.17/0.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)) )=> ( C = k1_tsp_2(A,B)<=> v3_borsuk_1(C,A,B) ) ) )) )) )),
% 0.17/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f54,axiom,(
% 0.17/0.56 (! [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)) ) ) )),
% 0.17/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f86,axiom,(
% 0.17/0.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)=> (! [D] :( m1_subset_1(D,u1_struct_0(A))=> (! [E] :( m1_subset_1(E,u1_struct_0(B))=> ( D = E=> k5_pre_topc(A,B,C,k6_pre_topc(B,k1_struct_0(B,E))) = k6_pre_topc(A,k1_struct_0(A,D)) ) ) )) )) ) )) )) )),
% 0.17/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f102,axiom,(
% 0.17/0.56 (! [A] :( l1_pre_topc(A)=> (! [B] :( m2_tsp_1(B,A)<=> m1_pre_topc(B,A) ) )) )),
% 0.17/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f112,plain,(
% 0.17/0.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]: (m1_subset_1(C,u1_struct_0(A))&(?[D]: (m1_subset_1(D,u1_struct_0(B))&(C=D&~k5_pre_topc(A,B,k1_tsp_2(A,B),k6_pre_topc(B,k1_struct_0(B,D)))=k6_pre_topc(A,k1_struct_0(A,C)))))))))))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.17/0.56 fof(f113,plain,(
% 0.17/0.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))&(m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))&(m1_subset_1(sK3_skl,u1_struct_0(sK1_skl))&(sK2_skl=sK3_skl&~k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK3_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl)))))))),
% 0.17/0.56 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)],[f112])).
% 0.17/0.56 fof(f114,plain,(
% 0.17/0.56 ~v3_struct_0(sK0_skl)),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f115,plain,(
% 0.17/0.56 v2_pre_topc(sK0_skl)),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f116,plain,(
% 0.17/0.56 l1_pre_topc(sK0_skl)),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f117,plain,(
% 0.17/0.56 ~v3_struct_0(sK1_skl)),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f118,plain,(
% 0.17/0.56 v2_tsp_2(sK1_skl,sK0_skl)),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f119,plain,(
% 0.17/0.56 m2_tsp_1(sK1_skl,sK0_skl)),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f120,plain,(
% 0.17/0.56 m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f121,plain,(
% 0.17/0.56 m1_subset_1(sK3_skl,u1_struct_0(sK1_skl))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f122,plain,(
% 0.17/0.56 sK2_skl=sK3_skl),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f123,plain,(
% 0.17/0.56 ~k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK3_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f113])).
% 0.17/0.56 fof(f304,plain,(
% 0.17/0.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)))|(C=k1_tsp_2(A,B)<=>v3_borsuk_1(C,A,B)))))))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.17/0.56 fof(f305,plain,(
% 0.17/0.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)))|((~C=k1_tsp_2(A,B)|v3_borsuk_1(C,A,B))&(C=k1_tsp_2(A,B)|~v3_borsuk_1(C,A,B))))))))),
% 0.17/0.56 inference(NNF_transformation,[status(thm)],[f304])).
% 0.17/0.56 fof(f306,plain,(
% 0.17/0.56 ![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(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=k1_tsp_2(X0,X1)|v3_borsuk_1(X2,X0,X1))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f305])).
% 0.17/0.56 fof(f310,plain,(
% 0.17/0.56 ![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))))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.17/0.56 fof(f311,plain,(
% 0.17/0.56 ![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(k1_tsp_2(X0,X1)))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f310])).
% 0.17/0.56 fof(f312,plain,(
% 0.17/0.56 ![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)))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f310])).
% 0.17/0.56 fof(f313,plain,(
% 0.17/0.56 ![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))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f310])).
% 0.17/0.56 fof(f314,plain,(
% 0.17/0.56 ![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)))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f310])).
% 0.17/0.56 fof(f378,plain,(
% 0.17/0.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)|(![D]: (~m1_subset_1(D,u1_struct_0(A))|(![E]: (~m1_subset_1(E,u1_struct_0(B))|(~D=E|k5_pre_topc(A,B,C,k6_pre_topc(B,k1_struct_0(B,E)))=k6_pre_topc(A,k1_struct_0(A,D)))))))))))))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 0.17/0.56 fof(f379,plain,(
% 0.17/0.56 ![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))|~v3_borsuk_1(X2,X0,X1)|~m1_subset_1(X3,u1_struct_0(X0))|~m1_subset_1(X4,u1_struct_0(X1))|~X3=X4|k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X4)))=k6_pre_topc(X0,k1_struct_0(X0,X3)))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f378])).
% 0.17/0.56 fof(f457,plain,(
% 0.17/0.56 ![A]: (~l1_pre_topc(A)|(![B]: (m2_tsp_1(B,A)<=>m1_pre_topc(B,A))))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f102])).
% 0.17/0.56 fof(f458,plain,(
% 0.17/0.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.17/0.56 inference(NNF_transformation,[status(thm)],[f457])).
% 0.17/0.56 fof(f459,plain,(
% 0.17/0.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.17/0.56 inference(miniscoping,[status(thm)],[f458])).
% 0.17/0.56 fof(f460,plain,(
% 0.17/0.56 ![X0,X1]: (~l1_pre_topc(X0)|~m2_tsp_1(X1,X0)|m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f459])).
% 0.17/0.56 fof(f486,plain,(
% 0.17/0.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(k1_tsp_2(X0,X1))|~v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|~m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1))),
% 0.17/0.56 inference(destructive_equality_resolution,[status(thm)],[f306])).
% 0.17/0.56 fof(f487,plain,(
% 0.17/0.56 ![X0,X1,X2,X3]: (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))|~v3_borsuk_1(X2,X0,X1)|~m1_subset_1(X3,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X1))|k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X3)))=k6_pre_topc(X0,k1_struct_0(X0,X3)))),
% 0.17/0.56 inference(destructive_equality_resolution,[status(thm)],[f379])).
% 0.17/0.56 fof(f488,plain,(
% 0.17/0.56 m1_subset_1(sK2_skl,u1_struct_0(sK1_skl))),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f122,f121])).
% 0.17/0.56 fof(f489,plain,(
% 0.17/0.56 ~k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK2_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl))),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f122,f123])).
% 0.17/0.56 fof(f523,definition,(
% 0.17/0.56 sQ6_spl <=> (v3_struct_0(sK1_skl))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f524,plain,(
% 0.17/0.56 v3_struct_0(sK1_skl)|~sQ6_spl),
% 0.17/0.56 inference(component_clause,[status(thm)],[f523])).
% 0.17/0.56 fof(f533,definition,(
% 0.17/0.56 sQ9_spl <=> (v3_struct_0(sK0_skl))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f534,plain,(
% 0.17/0.56 v3_struct_0(sK0_skl)|~sQ9_spl),
% 0.17/0.56 inference(component_clause,[status(thm)],[f533])).
% 0.17/0.56 fof(f543,plain,(
% 0.17/0.56 $false|~sQ9_spl),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f534,f114])).
% 0.17/0.56 fof(f544,plain,(
% 0.17/0.56 ~sQ9_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f543])).
% 0.17/0.56 fof(f653,definition,(
% 0.17/0.56 sQ33_spl <=> (v2_pre_topc(sK0_skl))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f655,plain,(
% 0.17/0.56 ~v2_pre_topc(sK0_skl)|sQ33_spl),
% 0.17/0.56 inference(component_clause,[status(thm)],[f653])).
% 0.17/0.56 fof(f660,plain,(
% 0.17/0.56 $false|~sQ6_spl),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f524,f117])).
% 0.17/0.56 fof(f661,plain,(
% 0.17/0.56 ~sQ6_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f660])).
% 0.17/0.56 fof(f662,plain,(
% 0.17/0.56 $false|sQ33_spl),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f655,f115])).
% 0.17/0.56 fof(f663,plain,(
% 0.17/0.56 sQ33_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f662])).
% 0.17/0.56 fof(f703,plain,(
% 0.17/0.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(k1_tsp_2(X0,X1))|~v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|v3_borsuk_1(k1_tsp_2(X0,X1),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))),
% 0.17/0.56 inference(resolution,[status(thm)],[f486,f314])).
% 0.17/0.56 fof(f704,plain,(
% 0.17/0.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(k1_tsp_2(X0,X1))|~v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(duplicate_literals_removal,[status(thm)],[f703])).
% 0.17/0.56 fof(f706,plain,(
% 0.17/0.56 ![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(k1_tsp_2(X0,X1))|~v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|~v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X2)))=k6_pre_topc(X0,k1_struct_0(X0,X2))|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))),
% 0.17/0.56 inference(resolution,[status(thm)],[f487,f314])).
% 0.17/0.56 fof(f714,plain,(
% 0.17/0.56 ![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(k1_tsp_2(X0,X1))|~v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|~v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X2)))=k6_pre_topc(X0,k1_struct_0(X0,X2))|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(duplicate_literals_removal,[status(thm)],[f706])).
% 0.17/0.56 fof(f715,plain,(
% 0.17/0.56 ![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_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|~v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X2)))=k6_pre_topc(X0,k1_struct_0(X0,X2))|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f714,f311])).
% 0.17/0.56 fof(f736,definition,(
% 0.17/0.56 sQ47_spl <=> (l1_pre_topc(sK0_skl))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f738,plain,(
% 0.17/0.56 ~l1_pre_topc(sK0_skl)|sQ47_spl),
% 0.17/0.56 inference(component_clause,[status(thm)],[f736])).
% 0.17/0.56 fof(f762,plain,(
% 0.17/0.56 $false|sQ47_spl),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f738,f116])).
% 0.17/0.56 fof(f763,plain,(
% 0.17/0.56 sQ47_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f762])).
% 0.17/0.56 fof(f954,plain,(
% 0.17/0.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(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f704,f311])).
% 0.17/0.56 fof(f955,plain,(
% 0.17/0.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(k1_tsp_2(X0,X1),X0,X1)|v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)|~m1_pre_topc(X1,X0)|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))),
% 0.17/0.56 inference(resolution,[status(thm)],[f954,f312])).
% 0.17/0.56 fof(f956,plain,(
% 0.17/0.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(k1_tsp_2(X0,X1),X0,X1)|v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(duplicate_literals_removal,[status(thm)],[f955])).
% 0.17/0.56 fof(f957,plain,(
% 0.17/0.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(k1_tsp_2(X0,X1),X0,X1)|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f956,f313])).
% 0.17/0.56 fof(f958,plain,(
% 0.17/0.56 ![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)|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|~v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X2)))=k6_pre_topc(X0,k1_struct_0(X0,X2))|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f715,f312])).
% 0.17/0.56 fof(f1222,plain,(
% 0.17/0.56 ![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)|~v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X2)))=k6_pre_topc(X0,k1_struct_0(X0,X2))|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f958,f957])).
% 0.17/0.56 fof(f1226,plain,(
% 0.17/0.56 ![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)|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X2)))=k6_pre_topc(X0,k1_struct_0(X0,X2))|~m1_pre_topc(X1,X0))),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1222,f313])).
% 0.17/0.56 fof(f1245,plain,(
% 0.17/0.56 ![X0]: (v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(X0)|~v2_tsp_2(X0,sK0_skl)|~m2_tsp_1(X0,sK0_skl)|~m1_subset_1(sK2_skl,u1_struct_0(X0))|k5_pre_topc(sK0_skl,X0,k1_tsp_2(sK0_skl,X0),k6_pre_topc(X0,k1_struct_0(X0,sK2_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl))|~m1_pre_topc(X0,sK0_skl))),
% 0.17/0.56 inference(resolution,[status(thm)],[f1226,f120])).
% 0.17/0.56 fof(f1255,definition,(
% 0.17/0.56 ![X0]: (sQ113_spl <=> (v3_struct_0(X0)|~v2_tsp_2(X0,sK0_skl)|~m2_tsp_1(X0,sK0_skl)|~m1_subset_1(sK2_skl,u1_struct_0(X0))|k5_pre_topc(sK0_skl,X0,k1_tsp_2(sK0_skl,X0),k6_pre_topc(X0,k1_struct_0(X0,sK2_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl))|~m1_pre_topc(X0,sK0_skl)))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f1256,plain,(
% 0.17/0.56 ![X0]: (v3_struct_0(X0)|~v2_tsp_2(X0,sK0_skl)|~m2_tsp_1(X0,sK0_skl)|~m1_subset_1(sK2_skl,u1_struct_0(X0))|k5_pre_topc(sK0_skl,X0,k1_tsp_2(sK0_skl,X0),k6_pre_topc(X0,k1_struct_0(X0,sK2_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl))|~m1_pre_topc(X0,sK0_skl)|~sQ113_spl)),
% 0.17/0.56 inference(component_clause,[status(thm)],[f1255])).
% 0.17/0.56 fof(f1258,plain,(
% 0.17/0.56 sQ9_spl|~sQ33_spl|~sQ47_spl|sQ113_spl),
% 0.17/0.56 inference(split_clause,[status(thm)],[f1245,f533,f653,f736,f1255])).
% 0.17/0.56 fof(f1400,plain,(
% 0.17/0.56 ~l1_pre_topc(sK0_skl)|m1_pre_topc(sK1_skl,sK0_skl)),
% 0.17/0.56 inference(resolution,[status(thm)],[f460,f119])).
% 0.17/0.56 fof(f1412,definition,(
% 0.17/0.56 sQ138_spl <=> (m1_pre_topc(sK1_skl,sK0_skl))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f1415,plain,(
% 0.17/0.56 ~sQ47_spl|sQ138_spl),
% 0.17/0.56 inference(split_clause,[status(thm)],[f1400,f736,f1412])).
% 0.17/0.56 fof(f1533,plain,(
% 0.17/0.56 v3_struct_0(sK1_skl)|~v2_tsp_2(sK1_skl,sK0_skl)|~m2_tsp_1(sK1_skl,sK0_skl)|k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK2_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl))|~m1_pre_topc(sK1_skl,sK0_skl)|~sQ113_spl),
% 0.17/0.56 inference(resolution,[status(thm)],[f1256,f488])).
% 0.17/0.56 fof(f1535,definition,(
% 0.17/0.56 sQ142_spl <=> (v2_tsp_2(sK1_skl,sK0_skl))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f1537,plain,(
% 0.17/0.56 ~v2_tsp_2(sK1_skl,sK0_skl)|sQ142_spl),
% 0.17/0.56 inference(component_clause,[status(thm)],[f1535])).
% 0.17/0.56 fof(f1538,definition,(
% 0.17/0.56 sQ143_spl <=> (m2_tsp_1(sK1_skl,sK0_skl))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f1540,plain,(
% 0.17/0.56 ~m2_tsp_1(sK1_skl,sK0_skl)|sQ143_spl),
% 0.17/0.56 inference(component_clause,[status(thm)],[f1538])).
% 0.17/0.56 fof(f1541,definition,(
% 0.17/0.56 sQ144_spl <=> (k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK2_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl)))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f1542,plain,(
% 0.17/0.56 k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK2_skl)))=k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl))|~sQ144_spl),
% 0.17/0.56 inference(component_clause,[status(thm)],[f1541])).
% 0.17/0.56 fof(f1544,plain,(
% 0.17/0.56 sQ6_spl|~sQ142_spl|~sQ143_spl|sQ144_spl|~sQ138_spl|~sQ113_spl),
% 0.17/0.56 inference(split_clause,[status(thm)],[f1533,f523,f1535,f1538,f1541,f1412,f1255])).
% 0.17/0.56 fof(f1546,plain,(
% 0.17/0.56 $false|~sQ144_spl),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1542,f489])).
% 0.17/0.56 fof(f1547,plain,(
% 0.17/0.56 ~sQ144_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f1546])).
% 0.17/0.56 fof(f1548,plain,(
% 0.17/0.56 $false|sQ142_spl),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1537,f118])).
% 0.17/0.56 fof(f1549,plain,(
% 0.17/0.56 sQ142_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f1548])).
% 0.17/0.56 fof(f1550,plain,(
% 0.17/0.56 $false|sQ143_spl),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1540,f119])).
% 0.17/0.56 fof(f1551,plain,(
% 0.17/0.56 sQ143_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f1550])).
% 0.17/0.56 fof(f1552,plain,(
% 0.17/0.56 $false),
% 0.17/0.56 inference(sat_refutation,[status(thm)],[f544,f661,f663,f763,f1258,f1415,f1544,f1547,f1549,f1551])).
% 0.17/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/0.60 % Elapsed time: 0.115068 seconds
% 0.21/0.60 % CPU time: 0.296661 seconds
% 0.21/0.60 % Total memory used: 47.978 MB
% 0.21/0.60 % Net memory used: 47.860 MB
%------------------------------------------------------------------------------