%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP027+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 : n016.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:42 PM UTC 2026
% Result : Theorem 56.64s 13.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP027+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/5.44 % Computer : n016.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.44 % CPULimit : 300
% 0.17/5.44 % WCLimit : 300
% 0.17/5.44 % DateTime : Mon Sep 21 12:46:00 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.82/6.10 % Drodi V4.1.1
% 56.64/13.30 % Refutation found
% 56.64/13.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 56.64/13.30 % SZS output start CNFRefutation for theBenchmark
% 56.64/13.30 fof(f2265,axiom,(
% 56.64/13.30 (! [A,B] :( ( v2_pre_topc(A)& l1_pre_topc(A)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> v3_pre_topc(k1_tops_1(A,B),A) ) )),
% 56.64/13.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.64/13.30 fof(f2402,axiom,(
% 56.64/13.30 (! [A,B] :( ( l1_pre_topc(A)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> m1_subset_1(k1_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A))) ) )),
% 56.64/13.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.64/13.30 fof(f3587,axiom,(
% 56.64/13.30 (! [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)))=> ( v3_pre_topc(C,A)=> C = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,C)) ) ) )) ) )) )),
% 56.64/13.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.64/13.30 fof(f3589,conjecture,(
% 56.64/13.30 (! [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)))=> k1_tops_1(A,C) = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k1_tops_1(A,C))) ) )) ) )) )),
% 56.64/13.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.64/13.30 fof(f3590,negated_conjecture,(
% 56.64/13.30 ~((! [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)))=> k1_tops_1(A,C) = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k1_tops_1(A,C))) ) )) ) )) ))),
% 56.64/13.30 inference(negated_conjecture,[status(cth)],[f3589])).
% 56.64/13.30 fof(f10279,plain,(
% 56.64/13.30 ![A,B]: (((~v2_pre_topc(A)|~l1_pre_topc(A))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|v3_pre_topc(k1_tops_1(A,B),A))),
% 56.64/13.30 inference(pre_NNF_transformation,[status(thm)],[f2265])).
% 56.64/13.30 fof(f10280,plain,(
% 56.64/13.30 ![X0,X1]: (~v2_pre_topc(X0)|~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v3_pre_topc(k1_tops_1(X0,X1),X0))),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f10279])).
% 56.64/13.30 fof(f10636,plain,(
% 56.64/13.30 ![A,B]: ((~l1_pre_topc(A)|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|m1_subset_1(k1_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A))))),
% 56.64/13.30 inference(pre_NNF_transformation,[status(thm)],[f2402])).
% 56.64/13.30 fof(f10637,plain,(
% 56.64/13.30 ![X0,X1]: (~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m1_subset_1(k1_tops_1(X0,X1),k1_zfmisc_1(u1_struct_0(X0))))),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f10636])).
% 56.64/13.30 fof(f15844,plain,(
% 56.64/13.30 ![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)))|(~v3_pre_topc(C,A)|C=k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,C)))))))))),
% 56.64/13.30 inference(pre_NNF_transformation,[status(thm)],[f3587])).
% 56.64/13.30 fof(f15845,plain,(
% 56.64/13.30 ![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)))|~v3_pre_topc(X2,X0)|X2=k3_tex_4(X0,k5_subset_1(u1_struct_0(X0),X1,X2)))),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f15844])).
% 56.64/13.30 fof(f15848,plain,(
% 56.64/13.30 (?[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)))&~k1_tops_1(A,C)=k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k1_tops_1(A,C))))))))))),
% 56.64/13.30 inference(pre_NNF_transformation,[status(thm)],[f3590])).
% 56.64/13.30 fof(f15849,plain,(
% 56.64/13.30 (((~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)))&~k1_tops_1(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k1_tops_1(sK1083_skl,sK1085_skl)))))))),
% 56.64/13.30 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)],[f15848])).
% 56.64/13.30 fof(f15850,plain,(
% 56.64/13.30 ~v3_struct_0(sK1083_skl)),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f15849])).
% 56.64/13.30 fof(f15851,plain,(
% 56.64/13.30 v2_pre_topc(sK1083_skl)),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f15849])).
% 56.64/13.30 fof(f15852,plain,(
% 56.64/13.30 l1_pre_topc(sK1083_skl)),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f15849])).
% 56.64/13.30 fof(f15853,plain,(
% 56.64/13.30 m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f15849])).
% 56.64/13.30 fof(f15854,plain,(
% 56.64/13.30 v1_tsp_2(sK1084_skl,sK1083_skl)),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f15849])).
% 56.64/13.30 fof(f15855,plain,(
% 56.64/13.30 m1_subset_1(sK1085_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f15849])).
% 56.64/13.30 fof(f15856,plain,(
% 56.64/13.30 ~k1_tops_1(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k1_tops_1(sK1083_skl,sK1085_skl)))),
% 56.64/13.30 inference(cnf_transformation,[status(thm)],[f15849])).
% 56.64/13.30 fof(f18544,definition,(
% 56.64/13.30 sQ425_spl <=> (v2_pre_topc(sK1083_skl))),
% 56.64/13.30 introduced(definition,[new_symbols(definition,[sQ425_spl])],[split_symbol_definition])).
% 56.64/13.30 fof(f18546,plain,(
% 56.64/13.30 ~v2_pre_topc(sK1083_skl)|sQ425_spl),
% 56.64/13.30 inference(component_clause,[status(thm)],[f18544])).
% 56.64/13.30 fof(f18547,definition,(
% 56.64/13.30 sQ426_spl <=> (l1_pre_topc(sK1083_skl))),
% 56.64/13.30 introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition])).
% 56.64/13.30 fof(f18549,plain,(
% 56.64/13.30 ~l1_pre_topc(sK1083_skl)|sQ426_spl),
% 56.64/13.30 inference(component_clause,[status(thm)],[f18547])).
% 56.64/13.30 fof(f18552,plain,(
% 56.64/13.30 $false|sQ425_spl),
% 56.64/13.30 inference(forward_subsumption_resolution,[status(thm)],[f18546,f15851])).
% 56.64/13.30 fof(f18553,plain,(
% 56.64/13.30 sQ425_spl),
% 56.64/13.30 inference(contradiction_clause,[status(thm)],[f18552])).
% 56.64/13.30 fof(f18554,plain,(
% 56.64/13.30 $false|sQ426_spl),
% 56.64/13.30 inference(forward_subsumption_resolution,[status(thm)],[f18549,f15852])).
% 56.64/13.30 fof(f18555,plain,(
% 56.64/13.30 sQ426_spl),
% 56.64/13.30 inference(contradiction_clause,[status(thm)],[f18554])).
% 56.64/13.30 fof(f18627,plain,(
% 56.64/13.30 ~v2_pre_topc(sK1083_skl)|~l1_pre_topc(sK1083_skl)|v3_pre_topc(k1_tops_1(sK1083_skl,sK1085_skl),sK1083_skl)),
% 56.64/13.30 inference(resolution,[status(thm)],[f10280,f15855])).
% 56.64/13.30 fof(f18632,definition,(
% 56.64/13.30 sQ437_spl <=> (v3_pre_topc(k1_tops_1(sK1083_skl,sK1085_skl),sK1083_skl))),
% 56.64/13.30 introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition])).
% 56.64/13.30 fof(f18635,plain,(
% 56.64/13.30 ~sQ425_spl|~sQ426_spl|sQ437_spl),
% 56.64/13.30 inference(split_clause,[status(thm)],[f18627,f18544,f18547,f18632])).
% 56.64/13.30 fof(f19035,plain,(
% 56.64/13.30 ~l1_pre_topc(sK1083_skl)|m1_subset_1(k1_tops_1(sK1083_skl,sK1085_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl)))),
% 56.64/13.30 inference(resolution,[status(thm)],[f10637,f15855])).
% 56.64/13.30 fof(f19044,definition,(
% 56.64/13.30 sQ497_spl <=> (m1_subset_1(k1_tops_1(sK1083_skl,sK1085_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))))),
% 56.64/13.30 introduced(definition,[new_symbols(definition,[sQ497_spl])],[split_symbol_definition])).
% 56.64/13.30 fof(f19045,plain,(
% 56.64/13.30 m1_subset_1(k1_tops_1(sK1083_skl,sK1085_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl)))|~sQ497_spl),
% 56.64/13.30 inference(component_clause,[status(thm)],[f19044])).
% 56.64/13.30 fof(f19047,plain,(
% 56.64/13.30 ~sQ426_spl|sQ497_spl),
% 56.64/13.30 inference(split_clause,[status(thm)],[f19035,f18547,f19044])).
% 56.64/13.30 fof(f19881,definition,(
% 56.64/13.30 sQ612_spl <=> (v3_struct_0(sK1083_skl))),
% 56.64/13.30 introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition])).
% 56.64/13.30 fof(f19882,plain,(
% 56.64/13.30 v3_struct_0(sK1083_skl)|~sQ612_spl),
% 56.64/13.30 inference(component_clause,[status(thm)],[f19881])).
% 56.64/13.30 fof(f19912,plain,(
% 56.64/13.30 $false|~sQ612_spl),
% 56.64/13.30 inference(forward_subsumption_resolution,[status(thm)],[f19882,f15850])).
% 56.64/13.30 fof(f19913,plain,(
% 56.64/13.30 ~sQ612_spl),
% 56.64/13.30 inference(contradiction_clause,[status(thm)],[f19912])).
% 56.64/13.30 fof(f22088,definition,(
% 56.64/13.30 sQ767_spl <=> (v1_tsp_2(sK1084_skl,sK1083_skl))),
% 56.64/13.30 introduced(definition,[new_symbols(definition,[sQ767_spl])],[split_symbol_definition])).
% 56.64/13.30 fof(f22090,plain,(
% 56.64/13.30 ~v1_tsp_2(sK1084_skl,sK1083_skl)|sQ767_spl),
% 56.64/13.30 inference(component_clause,[status(thm)],[f22088])).
% 56.64/13.30 fof(f22102,plain,(
% 56.64/13.30 $false|sQ767_spl),
% 56.64/13.30 inference(forward_subsumption_resolution,[status(thm)],[f22090,f15854])).
% 56.64/13.30 fof(f22103,plain,(
% 56.64/13.30 sQ767_spl),
% 56.64/13.30 inference(contradiction_clause,[status(thm)],[f22102])).
% 56.64/13.30 fof(f22398,plain,(
% 56.64/13.30 ![X0]: (v3_struct_0(sK1083_skl)|~v2_pre_topc(sK1083_skl)|~l1_pre_topc(sK1083_skl)|~v1_tsp_2(sK1084_skl,sK1083_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|~v3_pre_topc(X0,sK1083_skl)|X0=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,X0)))),
% 50.44/13.45 inference(resolution,[status(thm)],[f15845,f15853])).
% 50.44/13.45 fof(f22400,definition,(
% 50.44/13.45 ![X0]: (sQ789_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|~v3_pre_topc(X0,sK1083_skl)|X0=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,X0))))),
% 50.44/13.45 introduced(definition,[new_symbols(definition,[sQ789_spl])],[split_symbol_definition])).
% 50.44/13.45 fof(f22401,plain,(
% 50.44/13.45 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))|~v3_pre_topc(X0,sK1083_skl)|X0=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,X0))|~sQ789_spl)),
% 50.44/13.45 inference(component_clause,[status(thm)],[f22400])).
% 50.44/13.45 fof(f22403,plain,(
% 50.44/13.45 sQ612_spl|~sQ425_spl|~sQ426_spl|~sQ767_spl|sQ789_spl),
% 50.44/13.45 inference(split_clause,[status(thm)],[f22398,f19881,f18544,f18547,f22088,f22400])).
% 50.44/13.45 fof(f28226,plain,(
% 50.44/13.45 ~v3_pre_topc(k1_tops_1(sK1083_skl,sK1085_skl),sK1083_skl)|k1_tops_1(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k1_tops_1(sK1083_skl,sK1085_skl)))|~sQ497_spl|~sQ789_spl),
% 50.44/13.45 inference(resolution,[status(thm)],[f19045,f22401])).
% 50.44/13.45 fof(f28329,definition,(
% 50.44/13.45 sQ1112_spl <=> (k1_tops_1(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k1_tops_1(sK1083_skl,sK1085_skl))))),
% 50.44/13.45 introduced(definition,[new_symbols(definition,[sQ1112_spl])],[split_symbol_definition])).
% 50.44/13.45 fof(f28330,plain,(
% 50.44/13.45 k1_tops_1(sK1083_skl,sK1085_skl)=k3_tex_4(sK1083_skl,k5_subset_1(u1_struct_0(sK1083_skl),sK1084_skl,k1_tops_1(sK1083_skl,sK1085_skl)))|~sQ1112_spl),
% 50.44/13.45 inference(component_clause,[status(thm)],[f28329])).
% 50.44/13.45 fof(f28332,plain,(
% 50.44/13.45 ~sQ437_spl|sQ1112_spl|~sQ497_spl|~sQ789_spl),
% 50.44/13.45 inference(split_clause,[status(thm)],[f28226,f18632,f28329,f19044,f22400])).
% 50.44/13.45 fof(f28532,plain,(
% 50.44/13.45 $false|~sQ1112_spl),
% 50.44/13.45 inference(forward_subsumption_resolution,[status(thm)],[f28330,f15856])).
% 50.44/13.45 fof(f28533,plain,(
% 50.44/13.45 ~sQ1112_spl),
% 50.44/13.45 inference(contradiction_clause,[status(thm)],[f28532])).
% 50.44/13.45 fof(f28534,plain,(
% 50.44/13.45 $false),
% 50.44/13.45 inference(sat_refutation,[status(thm)],[f18553,f18555,f18635,f19047,f19913,f22103,f22403,f28332,f28533])).
% 50.44/13.45 % SZS output end CNFRefutation for theBenchmark.p
% 9.59/13.48 % Elapsed time: 8.010199 seconds
% 9.59/13.48 % CPU time: 57.588935 seconds
% 9.59/13.48 % Total memory used: 817.252 MB
% 9.59/13.48 % Net memory used: 785.858 MB
%------------------------------------------------------------------------------