%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP026+2 : 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:41 PM UTC 2026
% Result : Theorem 0.95s 2.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP026+2 : 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.42 % Computer : n018.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 12:41:59 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.78/1.10 % Drodi V4.1.1
% 0.95/2.43 % Refutation found
% 0.95/2.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.95/2.43 % SZS output start CNFRefutation for theBenchmark
% 0.95/2.43 fof(f2255,axiom,(
% 0.95/2.43 (! [A,B] :( ( l1_pre_topc(A)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> m1_subset_1(k6_pre_topc(A,B),k1_zfmisc_1(u1_struct_0(A))) ) )),
% 0.95/2.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/2.43 fof(f2260,axiom,(
% 0.95/2.43 (! [A,B] :( ( v2_pre_topc(A)& l1_pre_topc(A)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> v4_pre_topc(k6_pre_topc(A,B),A) ) )),
% 0.95/2.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/2.43 fof(f3586,axiom,(
% 0.95/2.43 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( v1_tsp_2(B,A)=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> ( v4_pre_topc(C,A)=> C = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,C)) ) ) )) ) )) )),
% 0.95/2.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/2.43 fof(f3588,conjecture,(
% 0.95/2.43 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( v1_tsp_2(B,A)=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> k6_pre_topc(A,C) = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k6_pre_topc(A,C))) ) )) ) )) )),
% 0.95/2.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/2.43 fof(f3589,negated_conjecture,(
% 0.95/2.43 ~((! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( v1_tsp_2(B,A)=> (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> k6_pre_topc(A,C) = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k6_pre_topc(A,C))) ) )) ) )) ))),
% 0.95/2.43 inference(negated_conjecture,[status(cth)],[f3588])).
% 0.95/2.43 fof(f10243,plain,(
% 0.95/2.43 ![A,B]: ((~l1_pre_topc(A)|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|m1_subset_1(k6_pre_topc(A,B),k1_zfmisc_1(u1_struct_0(A))))),
% 0.95/2.43 inference(pre_NNF_transformation,[status(thm)],[f2255])).
% 0.95/2.43 fof(f10244,plain,(
% 0.95/2.43 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m1_subset_1(k6_pre_topc(X0,X1),k1_zfmisc_1(u1_struct_0(X0))))),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f10243])).
% 0.95/2.43 fof(f10261,plain,(
% 0.95/2.43 ![A,B]: (((~v2_pre_topc(A)|~l1_pre_topc(A))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|v4_pre_topc(k6_pre_topc(A,B),A))),
% 0.95/2.43 inference(pre_NNF_transformation,[status(thm)],[f2260])).
% 0.95/2.43 fof(f10262,plain,(
% 0.95/2.43 ![X0,X1]: (~v2_pre_topc(X0)|~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v4_pre_topc(k6_pre_topc(X0,X1),X0))),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f10261])).
% 0.95/2.43 fof(f15841,plain,(
% 0.95/2.43 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|(~v1_tsp_2(B,A)|(![C]: (~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))|(~v4_pre_topc(C,A)|C=k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,C)))))))))),
% 0.95/2.43 inference(pre_NNF_transformation,[status(thm)],[f3586])).
% 0.95/2.43 fof(f15842,plain,(
% 0.95/2.43 ![X0,X1,X2]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~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)))|~v4_pre_topc(X2,X0)|X2=k3_tex_4(X0,k5_subset_1(u1_struct_0(X0),X1,X2)))),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f15841])).
% 0.95/2.43 fof(f15845,plain,(
% 0.95/2.43 (?[A]: (((~v3_struct_0(A)&v2_pre_topc(A))&l1_pre_topc(A))&(?[B]: (m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))&(v1_tsp_2(B,A)&(?[C]: (m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))&~k6_pre_topc(A,C)=k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k6_pre_topc(A,C))))))))))),
% 0.95/2.43 inference(pre_NNF_transformation,[status(thm)],[f3589])).
% 0.95/2.43 fof(f15846,plain,(
% 0.95/2.43 (((~v3_struct_0(sK1083_skl)&v2_pre_topc(sK1083_skl))&l1_pre_topc(sK1083_skl))&(m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))&(v1_tsp_2(sK1084_skl,sK1083_skl)&(m1_subset_1(sK1085_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))&~k6_pre_topc(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k6_pre_topc(sK1083_skl,sK1085_skl)))))))),
% 0.95/2.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK1083_skl,sK1084_skl,sK1085_skl]),skolemize(A,sK1083_skl),skolemize(B,sK1084_skl),skolemize(C,sK1085_skl)],[f15845])).
% 0.95/2.43 fof(f15847,plain,(
% 0.95/2.43 ~v3_struct_0(sK1083_skl)),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f15846])).
% 0.95/2.43 fof(f15848,plain,(
% 0.95/2.43 v2_pre_topc(sK1083_skl)),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f15846])).
% 0.95/2.43 fof(f15849,plain,(
% 0.95/2.43 l1_pre_topc(sK1083_skl)),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f15846])).
% 0.95/2.43 fof(f15850,plain,(
% 0.95/2.43 m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f15846])).
% 0.95/2.43 fof(f15851,plain,(
% 0.95/2.43 v1_tsp_2(sK1084_skl,sK1083_skl)),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f15846])).
% 0.95/2.43 fof(f15852,plain,(
% 0.95/2.43 m1_subset_1(sK1085_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f15846])).
% 0.95/2.43 fof(f15853,plain,(
% 0.95/2.43 ~k6_pre_topc(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k6_pre_topc(sK1083_skl,sK1085_skl)))),
% 0.95/2.43 inference(cnf_transformation,[status(thm)],[f15846])).
% 0.95/2.43 fof(f19162,definition,(
% 0.95/2.43 sQ425_spl <=> (m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl))))),
% 10.60/2.43 introduced(definition,[new_symbols(definition,[sQ425_spl])],[split_symbol_definition])).
% 10.60/2.43 fof(f19164,plain,(
% 10.60/2.43 ~m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|sQ425_spl),
% 10.60/2.43 inference(component_clause,[status(thm)],[f19162])).
% 10.60/2.43 fof(f19169,plain,(
% 10.60/2.43 $false|sQ425_spl),
% 10.60/2.43 inference(forward_subsumption_resolution,[status(thm)],[f19164,f15850])).
% 10.60/2.43 fof(f19170,plain,(
% 10.60/2.43 sQ425_spl),
% 10.60/2.43 inference(contradiction_clause,[status(thm)],[f19169])).
% 10.60/2.43 fof(f19175,definition,(
% 10.60/2.43 sQ427_spl <=> (v2_pre_topc(sK1083_skl))),
% 10.60/2.43 introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition])).
% 10.60/2.43 fof(f19177,plain,(
% 10.60/2.43 ~v2_pre_topc(sK1083_skl)|sQ427_spl),
% 10.60/2.43 inference(component_clause,[status(thm)],[f19175])).
% 10.60/2.43 fof(f19182,plain,(
% 10.60/2.43 $false|sQ427_spl),
% 10.60/2.43 inference(forward_subsumption_resolution,[status(thm)],[f19177,f15848])).
% 10.60/2.43 fof(f19183,plain,(
% 10.60/2.43 sQ427_spl),
% 10.60/2.43 inference(contradiction_clause,[status(thm)],[f19182])).
% 10.60/2.43 fof(f19214,plain,(
% 10.60/2.43 ![X0]: (~v2_pre_topc(sK1083_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|v4_pre_topc(k6_pre_topc(sK1083_skl,X0),sK1083_skl))),
% 10.60/2.43 inference(resolution,[status(thm)],[f10262,f15849])).
% 10.60/2.43 fof(f19215,definition,(
% 10.60/2.43 ![X0]: (sQ429_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|v4_pre_topc(k6_pre_topc(sK1083_skl,X0),sK1083_skl)))),
% 10.60/2.43 introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition])).
% 10.60/2.43 fof(f19216,plain,(
% 10.60/2.43 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|v4_pre_topc(k6_pre_topc(sK1083_skl,X0),sK1083_skl)|~sQ429_spl)),
% 10.60/2.43 inference(component_clause,[status(thm)],[f19215])).
% 10.60/2.43 fof(f19218,plain,(
% 10.60/2.43 ~sQ427_spl|sQ429_spl),
% 10.60/2.43 inference(split_clause,[status(thm)],[f19214,f19175,f19215])).
% 10.60/2.43 fof(f19221,plain,(
% 10.60/2.43 v4_pre_topc(k6_pre_topc(sK1083_skl,sK1085_skl),sK1083_skl)|~sQ429_spl),
% 10.60/2.43 inference(resolution,[status(thm)],[f19216,f15852])).
% 10.60/2.43 fof(f19225,definition,(
% 10.60/2.43 sQ430_spl <=> (l1_pre_topc(sK1083_skl))),
% 10.60/2.43 introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition])).
% 10.60/2.43 fof(f19227,plain,(
% 10.60/2.43 ~l1_pre_topc(sK1083_skl)|sQ430_spl),
% 10.60/2.44 inference(component_clause,[status(thm)],[f19225])).
% 10.60/2.44 fof(f19231,definition,(
% 10.60/2.44 sQ432_spl <=> (m1_subset_1(k6_pre_topc(sK1083_skl,sK1085_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))))),
% 10.60/2.44 introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition])).
% 10.60/2.44 fof(f19233,plain,(
% 10.60/2.44 ~m1_subset_1(k6_pre_topc(sK1083_skl,sK1085_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl)))|sQ432_spl),
% 10.60/2.44 inference(component_clause,[status(thm)],[f19231])).
% 10.60/2.44 fof(f19239,plain,(
% 10.60/2.44 $false|sQ430_spl),
% 10.60/2.44 inference(forward_subsumption_resolution,[status(thm)],[f19227,f15849])).
% 10.60/2.44 fof(f19240,plain,(
% 10.60/2.44 sQ430_spl),
% 10.60/2.44 inference(contradiction_clause,[status(thm)],[f19239])).
% 10.60/2.44 fof(f19410,plain,(
% 10.60/2.44 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|m1_subset_1(k6_pre_topc(sK1083_skl,X0),k1_zfmisc_1(u1_struct_0(sK1083_skl))))),
% 10.60/2.44 inference(resolution,[status(thm)],[f10244,f15849])).
% 10.60/2.44 fof(f19546,plain,(
% 10.60/2.44 m1_subset_1(k6_pre_topc(sK1083_skl,sK1085_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl)))),
% 10.60/2.44 inference(resolution,[status(thm)],[f19410,f15852])).
% 10.60/2.49 fof(f19550,plain,(
% 10.60/2.49 $false|sQ432_spl),
% 10.60/2.49 inference(forward_subsumption_resolution,[status(thm)],[f19546,f19233])).
% 10.60/2.49 fof(f19551,plain,(
% 10.60/2.49 sQ432_spl),
% 10.60/2.49 inference(contradiction_clause,[status(thm)],[f19550])).
% 10.60/2.49 fof(f19908,definition,(
% 10.60/2.49 sQ510_spl <=> (v3_struct_0(sK1083_skl))),
% 10.60/2.49 introduced(definition,[new_symbols(definition,[sQ510_spl])],[split_symbol_definition])).
% 10.60/2.49 fof(f19909,plain,(
% 10.60/2.49 v3_struct_0(sK1083_skl)|~sQ510_spl),
% 10.60/2.49 inference(component_clause,[status(thm)],[f19908])).
% 10.60/2.49 fof(f19926,plain,(
% 10.60/2.49 $false|~sQ510_spl),
% 10.60/2.49 inference(forward_subsumption_resolution,[status(thm)],[f19909,f15847])).
% 10.60/2.49 fof(f19927,plain,(
% 10.60/2.49 ~sQ510_spl),
% 10.60/2.49 inference(contradiction_clause,[status(thm)],[f19926])).
% 10.60/2.49 fof(f23684,plain,(
% 10.60/2.49 ![X0]: (v3_struct_0(sK1083_skl)|~v2_pre_topc(sK1083_skl)|~l1_pre_topc(sK1083_skl)|~m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|~v4_pre_topc(X0,sK1083_skl)|X0=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,X0)))),
% 10.60/2.49 inference(resolution,[status(thm)],[f15842,f15851])).
% 10.60/2.49 fof(f23685,definition,(
% 10.60/2.49 ![X0]: (sQ968_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|~v4_pre_topc(X0,sK1083_skl)|X0=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,X0))))),
% 10.60/2.49 introduced(definition,[new_symbols(definition,[sQ968_spl])],[split_symbol_definition])).
% 10.60/2.49 fof(f23686,plain,(
% 10.60/2.49 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|~v4_pre_topc(X0,sK1083_skl)|X0=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,X0))|~sQ968_spl)),
% 10.60/2.49 inference(component_clause,[status(thm)],[f23685])).
% 10.60/2.49 fof(f23688,plain,(
% 10.60/2.49 sQ510_spl|~sQ427_spl|~sQ430_spl|~sQ425_spl|sQ968_spl),
% 10.60/2.49 inference(split_clause,[status(thm)],[f23684,f19908,f19175,f19225,f19162,f23685])).
% 10.60/2.49 fof(f30675,plain,(
% 10.60/2.49 ~m1_subset_1(k6_pre_topc(sK1083_skl,sK1085_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl)))|k6_pre_topc(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k6_pre_topc(sK1083_skl,sK1085_skl)))|~sQ968_spl|~sQ429_spl),
% 10.60/2.49 inference(resolution,[status(thm)],[f23686,f19221])).
% 10.60/2.49 fof(f30681,definition,(
% 10.60/2.49 sQ1294_spl <=> (k6_pre_topc(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k6_pre_topc(sK1083_skl,sK1085_skl))))),
% 10.60/2.49 introduced(definition,[new_symbols(definition,[sQ1294_spl])],[split_symbol_definition])).
% 10.60/2.49 fof(f30682,plain,(
% 10.60/2.49 k6_pre_topc(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k6_pre_topc(sK1083_skl,sK1085_skl)))|~sQ1294_spl),
% 10.60/2.49 inference(component_clause,[status(thm)],[f30681])).
% 10.60/2.49 fof(f30684,plain,(
% 10.60/2.49 ~sQ432_spl|sQ1294_spl|~sQ968_spl|~sQ429_spl),
% 10.60/2.49 inference(split_clause,[status(thm)],[f30675,f19231,f30681,f23685,f19215])).
% 10.60/2.49 fof(f30689,plain,(
% 10.60/2.49 $false|~sQ1294_spl),
% 10.60/2.49 inference(forward_subsumption_resolution,[status(thm)],[f30682,f15853])).
% 10.60/2.49 fof(f30690,plain,(
% 10.60/2.49 ~sQ1294_spl),
% 10.60/2.49 inference(contradiction_clause,[status(thm)],[f30689])).
% 10.60/2.49 fof(f30691,plain,(
% 10.60/2.49 $false),
% 10.60/2.49 inference(sat_refutation,[status(thm)],[f19170,f19183,f19218,f19240,f19551,f19927,f23688,f30684,f30690])).
% 10.60/2.49 % SZS output end CNFRefutation for theBenchmark.p
% 3.33/2.59 % Elapsed time: 2.132150 seconds
% 3.33/2.59 % CPU time: 11.331593 seconds
% 3.33/2.59 % Total memory used: 631.509 MB
% 3.33/2.59 % Net memory used: 620.926 MB
%------------------------------------------------------------------------------