%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP027+3 : 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 : n009.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 39.69s 8.07s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : TOP027+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n009.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 12:41:14 UTC 2026
% 0.18/0.45 % CPUTime :
% 2.93/3.28 % Drodi V4.1.1
% 39.69/8.07 % Refutation found
% 39.69/8.07 % SZS status Theorem for theBenchmark: Theorem is valid
% 39.69/8.07 % SZS output start CNFRefutation for theBenchmark
% 39.69/8.07 fof(f6870,axiom,(
% 39.69/8.07 (! [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) ) )),
% 39.69/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.69/8.07 fof(f7007,axiom,(
% 39.69/8.07 (! [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))) ) )),
% 39.69/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.69/8.07 fof(f13481,axiom,(
% 39.69/8.07 (! [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)) ) ) )) ) )) )),
% 39.69/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.69/8.07 fof(f13483,conjecture,(
% 39.69/8.07 (! [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))) ) )) ) )) )),
% 39.69/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.69/8.07 fof(f13484,negated_conjecture,(
% 39.69/8.07 ~((! [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))) ) )) ) )) ))),
% 39.69/8.07 inference(negated_conjecture,[status(cth)],[f13483])).
% 39.69/8.07 fof(f34519,plain,(
% 39.69/8.07 ![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))),
% 39.69/8.07 inference(pre_NNF_transformation,[status(thm)],[f6870])).
% 39.69/8.07 fof(f34520,plain,(
% 39.69/8.07 ![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))),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f34519])).
% 39.69/8.07 fof(f34876,plain,(
% 39.69/8.07 ![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))))),
% 39.69/8.07 inference(pre_NNF_transformation,[status(thm)],[f7007])).
% 39.69/8.07 fof(f34877,plain,(
% 39.69/8.07 ![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))))),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f34876])).
% 39.69/8.07 fof(f57101,plain,(
% 39.69/8.07 ![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)))))))))),
% 39.69/8.07 inference(pre_NNF_transformation,[status(thm)],[f13481])).
% 39.69/8.07 fof(f57102,plain,(
% 39.69/8.07 ![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)))),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f57101])).
% 39.69/8.07 fof(f57105,plain,(
% 39.69/8.07 (?[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))))))))))),
% 39.69/8.07 inference(pre_NNF_transformation,[status(thm)],[f13484])).
% 39.69/8.07 fof(f57106,plain,(
% 39.69/8.07 (((~v3_struct_0(sK3942_skl)&v2_pre_topc(sK3942_skl))&l1_pre_topc(sK3942_skl))&(m1_subset_1(sK3943_skl,k1_zfmisc_1(u1_struct_0(sK3942_skl)))&(v1_tsp_2(sK3943_skl,sK3942_skl)&(m1_subset_1(sK3944_skl,k1_zfmisc_1(u1_struct_0(sK3942_skl)))&~k1_tops_1(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k1_tops_1(sK3942_skl,sK3944_skl)))))))),
% 39.69/8.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK3942_skl,sK3943_skl,sK3944_skl]),skolemize(A,sK3942_skl),skolemize(B,sK3943_skl),skolemize(C,sK3944_skl)],[f57105])).
% 39.69/8.07 fof(f57107,plain,(
% 39.69/8.07 ~v3_struct_0(sK3942_skl)),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f57106])).
% 39.69/8.07 fof(f57108,plain,(
% 39.69/8.07 v2_pre_topc(sK3942_skl)),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f57106])).
% 39.69/8.07 fof(f57109,plain,(
% 39.69/8.07 l1_pre_topc(sK3942_skl)),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f57106])).
% 39.69/8.07 fof(f57110,plain,(
% 39.69/8.07 m1_subset_1(sK3943_skl,k1_zfmisc_1(u1_struct_0(sK3942_skl)))),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f57106])).
% 39.69/8.07 fof(f57111,plain,(
% 39.69/8.07 v1_tsp_2(sK3943_skl,sK3942_skl)),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f57106])).
% 39.69/8.07 fof(f57112,plain,(
% 39.69/8.07 m1_subset_1(sK3944_skl,k1_zfmisc_1(u1_struct_0(sK3942_skl)))),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f57106])).
% 39.69/8.07 fof(f57113,plain,(
% 39.69/8.07 ~k1_tops_1(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k1_tops_1(sK3942_skl,sK3944_skl)))),
% 39.69/8.07 inference(cnf_transformation,[status(thm)],[f57106])).
% 39.69/8.07 fof(f67595,definition,(
% 39.69/8.07 sQ1183_spl <=> (l1_pre_topc(sK3942_skl))),
% 39.69/8.07 introduced(definition,[new_symbols(definition,[sQ1183_spl])],[split_symbol_definition])).
% 39.69/8.07 fof(f67597,plain,(
% 39.69/8.07 ~l1_pre_topc(sK3942_skl)|sQ1183_spl),
% 39.69/8.07 inference(component_clause,[status(thm)],[f67595])).
% 39.69/8.07 fof(f67598,definition,(
% 39.69/8.07 sQ1184_spl <=> (v2_pre_topc(sK3942_skl))),
% 39.69/8.07 introduced(definition,[new_symbols(definition,[sQ1184_spl])],[split_symbol_definition])).
% 39.69/8.07 fof(f67600,plain,(
% 39.69/8.07 ~v2_pre_topc(sK3942_skl)|sQ1184_spl),
% 39.69/8.07 inference(component_clause,[status(thm)],[f67598])).
% 39.69/8.07 fof(f67615,plain,(
% 39.69/8.07 $false|sQ1184_spl),
% 39.69/8.07 inference(forward_subsumption_resolution,[status(thm)],[f67600,f57108])).
% 39.69/8.07 fof(f67616,plain,(
% 39.69/8.07 sQ1184_spl),
% 39.69/8.07 inference(contradiction_clause,[status(thm)],[f67615])).
% 39.69/8.07 fof(f67617,plain,(
% 39.69/8.07 $false|sQ1183_spl),
% 39.69/8.07 inference(forward_subsumption_resolution,[status(thm)],[f67597,f57109])).
% 39.69/8.07 fof(f67618,plain,(
% 39.69/8.07 sQ1183_spl),
% 39.69/8.07 inference(contradiction_clause,[status(thm)],[f67617])).
% 39.69/8.07 fof(f67636,plain,(
% 39.69/8.07 ~v2_pre_topc(sK3942_skl)|~l1_pre_topc(sK3942_skl)|v3_pre_topc(k1_tops_1(sK3942_skl,sK3944_skl),sK3942_skl)),
% 39.69/8.07 inference(resolution,[status(thm)],[f34520,f57112])).
% 39.69/8.07 fof(f67641,definition,(
% 39.69/8.07 sQ1192_spl <=> (v3_pre_topc(k1_tops_1(sK3942_skl,sK3944_skl),sK3942_skl))),
% 39.69/8.07 introduced(definition,[new_symbols(definition,[sQ1192_spl])],[split_symbol_definition])).
% 39.69/8.07 fof(f67644,plain,(
% 39.69/8.07 ~sQ1184_spl|~sQ1183_spl|sQ1192_spl),
% 39.69/8.07 inference(split_clause,[status(thm)],[f67636,f67598,f67595,f67641])).
% 39.69/8.07 fof(f67975,plain,(
% 39.69/8.07 ~l1_pre_topc(sK3942_skl)|m1_subset_1(k1_tops_1(sK3942_skl,sK3944_skl),k1_zfmisc_1(u1_struct_0(sK3942_skl)))),
% 39.69/8.07 inference(resolution,[status(thm)],[f34877,f57112])).
% 39.69/8.07 fof(f67980,definition,(
% 39.69/8.07 sQ1230_spl <=> (m1_subset_1(k1_tops_1(sK3942_skl,sK3944_skl),k1_zfmisc_1(u1_struct_0(sK3942_skl))))),
% 39.69/8.07 introduced(definition,[new_symbols(definition,[sQ1230_spl])],[split_symbol_definition])).
% 39.69/8.07 fof(f67981,plain,(
% 39.69/8.07 m1_subset_1(k1_tops_1(sK3942_skl,sK3944_skl),k1_zfmisc_1(u1_struct_0(sK3942_skl)))|~sQ1230_spl),
% 39.69/8.07 inference(component_clause,[status(thm)],[f67980])).
% 39.69/8.07 fof(f67983,plain,(
% 39.69/8.07 ~sQ1183_spl|sQ1230_spl),
% 39.69/8.07 inference(split_clause,[status(thm)],[f67975,f67595,f67980])).
% 39.69/8.07 fof(f69138,definition,(
% 39.69/8.07 sQ1324_spl <=> (v3_struct_0(sK3942_skl))),
% 39.69/8.07 introduced(definition,[new_symbols(definition,[sQ1324_spl])],[split_symbol_definition])).
% 39.69/8.07 fof(f69139,plain,(
% 39.69/8.07 v3_struct_0(sK3942_skl)|~sQ1324_spl),
% 39.69/8.07 inference(component_clause,[status(thm)],[f69138])).
% 39.69/8.07 fof(f69145,plain,(
% 39.69/8.07 $false|~sQ1324_spl),
% 39.69/8.07 inference(forward_subsumption_resolution,[status(thm)],[f69139,f57107])).
% 39.69/8.07 fof(f69146,plain,(
% 39.69/8.07 ~sQ1324_spl),
% 39.69/8.07 inference(contradiction_clause,[status(thm)],[f69145])).
% 39.69/8.07 fof(f72287,plain,(
% 39.69/8.07 ![X0]: (v3_struct_0(sK3942_skl)|~v2_pre_topc(sK3942_skl)|~l1_pre_topc(sK3942_skl)|~v1_tsp_2(sK3943_skl,sK3942_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3942_skl)))|~v3_pre_topc(X0,sK3942_skl)|X0=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,X0)))),
% 39.69/8.07 inference(resolution,[status(thm)],[f57110,f57102])).
% 39.69/8.07 fof(f72352,definition,(
% 39.69/8.07 sQ1551_spl <=> (v1_tsp_2(sK3943_skl,sK3942_skl))),
% 39.69/8.07 introduced(definition,[new_symbols(definition,[sQ1551_spl])],[split_symbol_definition])).
% 39.69/8.07 fof(f72354,plain,(
% 39.69/8.07 ~v1_tsp_2(sK3943_skl,sK3942_skl)|sQ1551_spl),
% 28.38/8.38 inference(component_clause,[status(thm)],[f72352])).
% 28.38/8.38 fof(f72359,definition,(
% 28.38/8.38 ![X0]: (sQ1553_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3942_skl)))|~v3_pre_topc(X0,sK3942_skl)|X0=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,X0))))),
% 28.38/8.38 introduced(definition,[new_symbols(definition,[sQ1553_spl])],[split_symbol_definition])).
% 28.38/8.38 fof(f72360,plain,(
% 28.38/8.38 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3942_skl)))|~v3_pre_topc(X0,sK3942_skl)|X0=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,X0))|~sQ1553_spl)),
% 28.38/8.38 inference(component_clause,[status(thm)],[f72359])).
% 28.38/8.38 fof(f72362,plain,(
% 28.38/8.38 sQ1324_spl|~sQ1184_spl|~sQ1183_spl|~sQ1551_spl|sQ1553_spl),
% 28.38/8.38 inference(split_clause,[status(thm)],[f72287,f69138,f67598,f67595,f72352,f72359])).
% 28.38/8.38 fof(f72496,plain,(
% 28.38/8.38 $false|sQ1551_spl),
% 28.38/8.38 inference(forward_subsumption_resolution,[status(thm)],[f72354,f57111])).
% 28.38/8.38 fof(f72497,plain,(
% 28.38/8.38 sQ1551_spl),
% 28.38/8.38 inference(contradiction_clause,[status(thm)],[f72496])).
% 28.38/8.38 fof(f79513,definition,(
% 28.38/8.38 sQ2055_spl <=> (k1_tops_1(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k1_tops_1(sK3942_skl,sK3944_skl))))),
% 28.38/8.38 introduced(definition,[new_symbols(definition,[sQ2055_spl])],[split_symbol_definition])).
% 28.38/8.38 fof(f79514,plain,(
% 28.38/8.38 k1_tops_1(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k1_tops_1(sK3942_skl,sK3944_skl)))|~sQ2055_spl),
% 28.38/8.38 inference(component_clause,[status(thm)],[f79513])).
% 28.38/8.38 fof(f79526,plain,(
% 28.38/8.38 $false|~sQ2055_spl),
% 28.38/8.38 inference(forward_subsumption_resolution,[status(thm)],[f79514,f57113])).
% 28.38/8.38 fof(f79527,plain,(
% 28.38/8.38 ~sQ2055_spl),
% 28.38/8.38 inference(contradiction_clause,[status(thm)],[f79526])).
% 28.38/8.38 fof(f79639,plain,(
% 28.38/8.38 ~v3_pre_topc(k1_tops_1(sK3942_skl,sK3944_skl),sK3942_skl)|k1_tops_1(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k1_tops_1(sK3942_skl,sK3944_skl)))|~sQ1553_spl|~sQ1230_spl),
% 28.38/8.38 inference(resolution,[status(thm)],[f72360,f67981])).
% 28.38/8.38 fof(f79643,plain,(
% 28.38/8.38 ~sQ1192_spl|sQ2055_spl|~sQ1553_spl|~sQ1230_spl),
% 28.38/8.38 inference(split_clause,[status(thm)],[f79639,f67641,f79513,f72359,f67980])).
% 28.38/8.38 fof(f79646,plain,(
% 28.38/8.38 $false),
% 28.38/8.38 inference(sat_refutation,[status(thm)],[f67616,f67618,f67644,f67983,f69146,f72362,f72497,f79527,f79643])).
% 28.38/8.38 % SZS output end CNFRefutation for theBenchmark.p
% 4.65/8.57 % Elapsed time: 8.067853 seconds
% 4.65/8.57 % CPU time: 40.663362 seconds
% 4.65/8.57 % Total memory used: 3.896 GB
% 4.65/8.57 % Net memory used: 3.861 GB
%------------------------------------------------------------------------------