%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP026+3 : 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 : n003.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 51.60s 8.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : TOP026+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n003.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 12:41:47 UTC 2026
% 0.16/0.43 % CPUTime :
% 1.94/2.20 % Drodi V4.1.1
% 51.60/8.72 % Refutation found
% 51.60/8.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 51.60/8.72 % SZS output start CNFRefutation for theBenchmark
% 51.60/8.72 fof(f6860,axiom,(
% 51.60/8.72 (! [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))) ) )),
% 51.60/8.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.60/8.72 fof(f6865,axiom,(
% 51.60/8.72 (! [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) ) )),
% 51.60/8.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.60/8.72 fof(f13480,axiom,(
% 51.60/8.72 (! [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)) ) ) )) ) )) )),
% 51.60/8.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.60/8.72 fof(f13482,conjecture,(
% 51.60/8.72 (! [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))) ) )) ) )) )),
% 51.60/8.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 51.60/8.72 fof(f13483,negated_conjecture,(
% 51.60/8.72 ~((! [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))) ) )) ) )) ))),
% 51.60/8.72 inference(negated_conjecture,[status(cth)],[f13482])).
% 51.60/8.72 fof(f34483,plain,(
% 51.60/8.72 ![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))))),
% 51.60/8.72 inference(pre_NNF_transformation,[status(thm)],[f6860])).
% 51.60/8.72 fof(f34484,plain,(
% 51.60/8.72 ![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))))),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f34483])).
% 51.60/8.72 fof(f34501,plain,(
% 51.60/8.72 ![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))),
% 51.60/8.72 inference(pre_NNF_transformation,[status(thm)],[f6865])).
% 51.60/8.72 fof(f34502,plain,(
% 51.60/8.72 ![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))),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f34501])).
% 51.60/8.72 fof(f57098,plain,(
% 51.60/8.72 ![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)))))))))),
% 51.60/8.72 inference(pre_NNF_transformation,[status(thm)],[f13480])).
% 51.60/8.72 fof(f57099,plain,(
% 51.60/8.72 ![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)))),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f57098])).
% 51.60/8.72 fof(f57102,plain,(
% 51.60/8.72 (?[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))))))))))),
% 51.60/8.72 inference(pre_NNF_transformation,[status(thm)],[f13483])).
% 51.60/8.72 fof(f57103,plain,(
% 51.60/8.72 (((~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)))&~k6_pre_topc(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k6_pre_topc(sK3942_skl,sK3944_skl)))))))),
% 51.60/8.72 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)],[f57102])).
% 51.60/8.72 fof(f57104,plain,(
% 51.60/8.72 ~v3_struct_0(sK3942_skl)),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f57103])).
% 51.60/8.72 fof(f57105,plain,(
% 51.60/8.72 v2_pre_topc(sK3942_skl)),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f57103])).
% 51.60/8.72 fof(f57106,plain,(
% 51.60/8.72 l1_pre_topc(sK3942_skl)),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f57103])).
% 51.60/8.72 fof(f57107,plain,(
% 51.60/8.72 m1_subset_1(sK3943_skl,k1_zfmisc_1(u1_struct_0(sK3942_skl)))),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f57103])).
% 51.60/8.72 fof(f57108,plain,(
% 51.60/8.72 v1_tsp_2(sK3943_skl,sK3942_skl)),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f57103])).
% 51.60/8.72 fof(f57109,plain,(
% 51.60/8.72 m1_subset_1(sK3944_skl,k1_zfmisc_1(u1_struct_0(sK3942_skl)))),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f57103])).
% 51.60/8.72 fof(f57110,plain,(
% 51.60/8.72 ~k6_pre_topc(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k6_pre_topc(sK3942_skl,sK3944_skl)))),
% 51.60/8.72 inference(cnf_transformation,[status(thm)],[f57103])).
% 51.60/8.72 fof(f65296,definition,(
% 51.60/8.72 sQ1183_spl <=> (l1_pre_topc(sK3942_skl))),
% 51.60/8.72 introduced(definition,[new_symbols(definition,[sQ1183_spl])],[split_symbol_definition])).
% 51.60/8.72 fof(f65298,plain,(
% 51.60/8.72 ~l1_pre_topc(sK3942_skl)|sQ1183_spl),
% 51.60/8.72 inference(component_clause,[status(thm)],[f65296])).
% 51.60/8.72 fof(f65299,definition,(
% 51.60/8.72 sQ1184_spl <=> (v2_pre_topc(sK3942_skl))),
% 51.60/8.72 introduced(definition,[new_symbols(definition,[sQ1184_spl])],[split_symbol_definition])).
% 51.60/8.72 fof(f65301,plain,(
% 51.60/8.72 ~v2_pre_topc(sK3942_skl)|sQ1184_spl),
% 51.60/8.72 inference(component_clause,[status(thm)],[f65299])).
% 51.60/8.72 fof(f65316,plain,(
% 51.60/8.72 $false|sQ1184_spl),
% 51.60/8.72 inference(forward_subsumption_resolution,[status(thm)],[f65301,f57105])).
% 51.60/8.72 fof(f65317,plain,(
% 51.60/8.72 sQ1184_spl),
% 51.60/8.72 inference(contradiction_clause,[status(thm)],[f65316])).
% 51.60/8.72 fof(f65318,plain,(
% 51.60/8.72 $false|sQ1183_spl),
% 51.60/8.72 inference(forward_subsumption_resolution,[status(thm)],[f65298,f57106])).
% 51.60/8.72 fof(f65319,plain,(
% 51.60/8.72 sQ1183_spl),
% 51.60/8.72 inference(contradiction_clause,[status(thm)],[f65318])).
% 51.60/8.72 fof(f65424,definition,(
% 51.60/8.72 sQ1202_spl <=> (v3_struct_0(sK3942_skl))),
% 51.60/8.72 introduced(definition,[new_symbols(definition,[sQ1202_spl])],[split_symbol_definition])).
% 51.60/8.72 fof(f65425,plain,(
% 51.60/8.72 v3_struct_0(sK3942_skl)|~sQ1202_spl),
% 51.60/8.72 inference(component_clause,[status(thm)],[f65424])).
% 51.60/8.72 fof(f65459,plain,(
% 51.60/8.72 ~l1_pre_topc(sK3942_skl)|m1_subset_1(k6_pre_topc(sK3942_skl,sK3944_skl),k1_zfmisc_1(u1_struct_0(sK3942_skl)))),
% 51.60/8.72 inference(resolution,[status(thm)],[f34484,f57109])).
% 51.60/8.72 fof(f65464,definition,(
% 51.60/8.72 sQ1207_spl <=> (m1_subset_1(k6_pre_topc(sK3942_skl,sK3944_skl),k1_zfmisc_1(u1_struct_0(sK3942_skl))))),
% 51.60/8.72 introduced(definition,[new_symbols(definition,[sQ1207_spl])],[split_symbol_definition])).
% 51.60/8.72 fof(f65465,plain,(
% 51.60/8.72 m1_subset_1(k6_pre_topc(sK3942_skl,sK3944_skl),k1_zfmisc_1(u1_struct_0(sK3942_skl)))|~sQ1207_spl),
% 51.60/8.72 inference(component_clause,[status(thm)],[f65464])).
% 51.60/8.72 fof(f65467,plain,(
% 51.60/8.72 ~sQ1183_spl|sQ1207_spl),
% 51.60/8.72 inference(split_clause,[status(thm)],[f65459,f65296,f65464])).
% 51.60/8.72 fof(f65542,plain,(
% 51.60/8.72 ~v2_pre_topc(sK3942_skl)|~l1_pre_topc(sK3942_skl)|v4_pre_topc(k6_pre_topc(sK3942_skl,sK3944_skl),sK3942_skl)),
% 51.60/8.72 inference(resolution,[status(thm)],[f34502,f57109])).
% 51.60/8.72 fof(f65547,definition,(
% 51.60/8.72 sQ1213_spl <=> (v4_pre_topc(k6_pre_topc(sK3942_skl,sK3944_skl),sK3942_skl))),
% 51.60/8.72 introduced(definition,[new_symbols(definition,[sQ1213_spl])],[split_symbol_definition])).
% 51.60/8.72 fof(f65550,plain,(
% 51.60/8.72 ~sQ1184_spl|~sQ1183_spl|sQ1213_spl),
% 51.60/8.72 inference(split_clause,[status(thm)],[f65542,f65299,f65296,f65547])).
% 51.60/8.72 fof(f66201,plain,(
% 51.60/8.72 $false|~sQ1202_spl),
% 51.60/8.72 inference(forward_subsumption_resolution,[status(thm)],[f65425,f57104])).
% 51.60/8.72 fof(f66202,plain,(
% 51.60/8.72 ~sQ1202_spl),
% 51.60/8.72 inference(contradiction_clause,[status(thm)],[f66201])).
% 51.60/8.72 fof(f68347,definition,(
% 51.60/8.72 sQ1407_spl <=> (v1_tsp_2(sK3943_skl,sK3942_skl))),
% 51.60/8.72 introduced(definition,[new_symbols(definition,[sQ1407_spl])],[split_symbol_definition])).
% 51.60/8.72 fof(f68349,plain,(
% 51.60/8.72 ~v1_tsp_2(sK3943_skl,sK3942_skl)|sQ1407_spl),
% 51.60/8.72 inference(component_clause,[status(thm)],[f68347])).
% 51.60/8.72 fof(f68361,plain,(
% 51.60/8.72 $false|sQ1407_spl),
% 51.60/8.72 inference(forward_subsumption_resolution,[status(thm)],[f68349,f57108])).
% 51.60/8.72 fof(f68362,plain,(
% 51.60/8.72 sQ1407_spl),
% 51.60/8.72 inference(contradiction_clause,[status(thm)],[f68361])).
% 51.60/8.72 fof(f68791,plain,(
% 51.30/8.96 ![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)))|~v4_pre_topc(X0,sK3942_skl)|X0=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,X0)))),
% 51.30/8.96 inference(resolution,[status(thm)],[f57099,f57107])).
% 51.30/8.96 fof(f68796,definition,(
% 51.30/8.96 ![X0]: (sQ1429_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3942_skl)))|~v4_pre_topc(X0,sK3942_skl)|X0=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,X0))))),
% 51.30/8.96 introduced(definition,[new_symbols(definition,[sQ1429_spl])],[split_symbol_definition])).
% 51.30/8.96 fof(f68797,plain,(
% 51.30/8.96 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK3942_skl)))|~v4_pre_topc(X0,sK3942_skl)|X0=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,X0))|~sQ1429_spl)),
% 51.30/8.96 inference(component_clause,[status(thm)],[f68796])).
% 51.30/8.96 fof(f68799,plain,(
% 51.30/8.96 sQ1202_spl|~sQ1184_spl|~sQ1183_spl|~sQ1407_spl|sQ1429_spl),
% 51.30/8.96 inference(split_clause,[status(thm)],[f68791,f65424,f65299,f65296,f68347,f68796])).
% 51.30/8.96 fof(f80917,plain,(
% 51.30/8.96 ~v4_pre_topc(k6_pre_topc(sK3942_skl,sK3944_skl),sK3942_skl)|k6_pre_topc(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k6_pre_topc(sK3942_skl,sK3944_skl)))|~sQ1207_spl|~sQ1429_spl),
% 51.30/8.96 inference(resolution,[status(thm)],[f65465,f68797])).
% 51.30/8.96 fof(f81036,definition,(
% 51.30/8.96 sQ2132_spl <=> (k6_pre_topc(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k6_pre_topc(sK3942_skl,sK3944_skl))))),
% 51.30/8.96 introduced(definition,[new_symbols(definition,[sQ2132_spl])],[split_symbol_definition])).
% 51.30/8.96 fof(f81037,plain,(
% 51.30/8.96 k6_pre_topc(sK3942_skl,sK3944_skl)=k3_tex_4(sK3942_skl,k5_subset_1(u1_struct_0(sK3942_skl),sK3943_skl,k6_pre_topc(sK3942_skl,sK3944_skl)))|~sQ2132_spl),
% 51.30/8.96 inference(component_clause,[status(thm)],[f81036])).
% 51.30/8.96 fof(f81040,plain,(
% 51.30/8.96 ~sQ1213_spl|sQ2132_spl|~sQ1207_spl|~sQ1429_spl),
% 51.30/8.96 inference(split_clause,[status(thm)],[f80917,f65547,f81036,f65464,f68796])).
% 51.30/8.96 fof(f81114,plain,(
% 51.30/8.96 $false|~sQ2132_spl),
% 51.30/8.96 inference(forward_subsumption_resolution,[status(thm)],[f81037,f57110])).
% 51.30/8.96 fof(f81115,plain,(
% 51.30/8.96 ~sQ2132_spl),
% 51.30/8.96 inference(contradiction_clause,[status(thm)],[f81114])).
% 51.30/8.96 fof(f81116,plain,(
% 51.30/8.96 $false),
% 51.30/8.96 inference(sat_refutation,[status(thm)],[f65317,f65319,f65467,f65550,f66202,f68362,f68799,f81040,f81115])).
% 51.30/8.96 % SZS output end CNFRefutation for theBenchmark.p
% 3.53/9.03 % Elapsed time: 8.561125 seconds
% 3.53/9.03 % CPU time: 53.900782 seconds
% 3.53/9.03 % Total memory used: 4.018 GB
% 3.53/9.03 % Net memory used: 3.967 GB
%------------------------------------------------------------------------------