%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP026+1 : 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 : n020.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.31s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : TOP026+1 : 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.19/0.43 % Computer : n020.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.43 % WCLimit : 300
% 0.19/0.43 % DateTime : Mon Sep 21 12:41:02 UTC 2026
% 0.19/0.43 % CPUTime :
% 0.19/0.44 % Drodi V4.1.1
% 0.31/0.50 % Refutation found
% 0.31/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.31/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.31/0.50 fof(f1,conjecture,(
% 0.31/0.50 (! [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.31/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.31/0.50 fof(f2,negated_conjecture,(
% 0.31/0.50 ~((! [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.31/0.50 inference(negated_conjecture,[status(cth)],[f1])).
% 0.31/0.50 fof(f71,axiom,(
% 0.31/0.50 (! [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.31/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.31/0.50 fof(f76,axiom,(
% 0.31/0.50 (! [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.31/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.31/0.50 fof(f79,axiom,(
% 0.31/0.50 (! [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.31/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.31/0.50 fof(f80,plain,(
% 0.31/0.50 (?[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.31/0.50 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.31/0.50 fof(f81,plain,(
% 0.31/0.50 (((~v3_struct_0(sK0_skl)&v2_pre_topc(sK0_skl))&l1_pre_topc(sK0_skl))&(m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))&(v1_tsp_2(sK1_skl,sK0_skl)&(m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))&~k6_pre_topc(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k6_pre_topc(sK0_skl,sK2_skl)))))))),
% 0.31/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f80])).
% 0.31/0.50 fof(f82,plain,(
% 0.31/0.50 ~v3_struct_0(sK0_skl)),
% 0.31/0.50 inference(cnf_transformation,[status(thm)],[f81])).
% 0.31/0.50 fof(f83,plain,(
% 0.31/0.50 v2_pre_topc(sK0_skl)),
% 0.31/0.50 inference(cnf_transformation,[status(thm)],[f81])).
% 0.31/0.50 fof(f84,plain,(
% 0.31/0.50 l1_pre_topc(sK0_skl)),
% 0.31/0.50 inference(cnf_transformation,[status(thm)],[f81])).
% 0.31/0.50 fof(f85,plain,(
% 0.31/0.50 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.31/0.50 inference(cnf_transformation,[status(thm)],[f81])).
% 0.31/0.50 fof(f86,plain,(
% 0.31/0.50 v1_tsp_2(sK1_skl,sK0_skl)),
% 0.31/0.50 inference(cnf_transformation,[status(thm)],[f81])).
% 0.31/0.50 fof(f87,plain,(
% 0.31/0.50 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.31/0.50 inference(cnf_transformation,[status(thm)],[f81])).
% 0.31/0.50 fof(f88,plain,(
% 0.31/0.50 ~k6_pre_topc(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k6_pre_topc(sK0_skl,sK2_skl)))),
% 0.31/0.50 inference(cnf_transformation,[status(thm)],[f81])).
% 0.31/0.50 fof(f331,plain,(
% 0.31/0.50 ![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.31/0.50 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 0.31/0.50 fof(f332,plain,(
% 0.31/0.50 ![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.31/0.50 inference(cnf_transformation,[status(thm)],[f331])).
% 0.31/0.50 fof(f336,plain,(
% 0.31/0.50 ![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.31/0.50 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 0.31/0.50 fof(f337,plain,(
% 0.31/0.50 ![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.31/0.50 inference(cnf_transformation,[status(thm)],[f336])).
% 0.31/0.50 fof(f346,plain,(
% 0.31/0.50 ![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.31/0.50 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 0.31/0.50 fof(f347,plain,(
% 0.31/0.50 ![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.31/0.50 inference(cnf_transformation,[status(thm)],[f346])).
% 0.31/0.50 fof(f387,definition,(
% 0.31/0.50 sQ6_spl <=> (v3_struct_0(sK0_skl))),
% 0.31/0.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.31/0.50 fof(f388,plain,(
% 0.31/0.50 v3_struct_0(sK0_skl)|~sQ6_spl),
% 0.31/0.50 inference(component_clause,[status(thm)],[f387])).
% 0.31/0.50 fof(f390,definition,(
% 0.31/0.50 sQ7_spl <=> (l1_pre_topc(sK0_skl))),
% 0.31/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.31/0.50 fof(f392,plain,(
% 0.31/0.50 ~l1_pre_topc(sK0_skl)|sQ7_spl),
% 0.31/0.50 inference(component_clause,[status(thm)],[f390])).
% 0.31/0.50 fof(f431,plain,(
% 0.31/0.50 $false|sQ7_spl),
% 0.31/0.50 inference(forward_subsumption_resolution,[status(thm)],[f392,f84])).
% 0.31/0.50 fof(f432,plain,(
% 0.31/0.50 sQ7_spl),
% 0.31/0.50 inference(contradiction_clause,[status(thm)],[f431])).
% 0.31/0.50 fof(f433,plain,(
% 0.31/0.50 $false|~sQ6_spl),
% 0.31/0.50 inference(forward_subsumption_resolution,[status(thm)],[f388,f82])).
% 0.31/0.50 fof(f434,plain,(
% 0.31/0.50 ~sQ6_spl),
% 0.31/0.50 inference(contradiction_clause,[status(thm)],[f433])).
% 0.31/0.50 fof(f438,plain,(
% 0.31/0.50 ~l1_pre_topc(sK0_skl)|m1_subset_1(k6_pre_topc(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.31/0.50 inference(resolution,[status(thm)],[f332,f87])).
% 0.31/0.50 fof(f443,definition,(
% 0.31/0.50 sQ15_spl <=> (m1_subset_1(k6_pre_topc(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.31/0.50 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.31/0.50 fof(f444,plain,(
% 0.31/0.50 m1_subset_1(k6_pre_topc(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ15_spl),
% 0.31/0.50 inference(component_clause,[status(thm)],[f443])).
% 0.31/0.50 fof(f446,plain,(
% 0.31/0.50 ~sQ7_spl|sQ15_spl),
% 0.31/0.50 inference(split_clause,[status(thm)],[f438,f390,f443])).
% 0.31/0.50 fof(f471,plain,(
% 0.31/0.50 ~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v4_pre_topc(k6_pre_topc(sK0_skl,sK2_skl),sK0_skl)),
% 0.31/0.50 inference(resolution,[status(thm)],[f337,f87])).
% 0.31/0.50 fof(f472,definition,(
% 0.31/0.50 sQ19_spl <=> (v2_pre_topc(sK0_skl))),
% 0.31/0.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.31/0.50 fof(f474,plain,(
% 0.31/0.50 ~v2_pre_topc(sK0_skl)|sQ19_spl),
% 0.31/0.50 inference(component_clause,[status(thm)],[f472])).
% 0.31/0.50 fof(f479,definition,(
% 0.31/0.50 sQ21_spl <=> (v4_pre_topc(k6_pre_topc(sK0_skl,sK2_skl),sK0_skl))),
% 0.31/0.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.31/0.50 fof(f482,plain,(
% 0.31/0.50 ~sQ19_spl|~sQ7_spl|sQ21_spl),
% 0.31/0.50 inference(split_clause,[status(thm)],[f471,f472,f390,f479])).
% 0.31/0.50 fof(f483,plain,(
% 0.31/0.50 $false|sQ19_spl),
% 0.31/0.50 inference(forward_subsumption_resolution,[status(thm)],[f474,f83])).
% 0.31/0.50 fof(f484,plain,(
% 0.31/0.50 sQ19_spl),
% 0.31/0.50 inference(contradiction_clause,[status(thm)],[f483])).
% 0.31/0.50 fof(f485,plain,(
% 0.31/0.50 ![X0]: (v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|~v1_tsp_2(sK1_skl,sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v4_pre_topc(X0,sK0_skl)|X0=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,X0)))),
% 0.31/0.50 inference(resolution,[status(thm)],[f347,f85])).
% 0.31/0.50 fof(f487,definition,(
% 0.31/0.50 sQ22_spl <=> (v1_tsp_2(sK1_skl,sK0_skl))),
% 0.31/0.50 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.31/0.50 fof(f489,plain,(
% 0.31/0.50 ~v1_tsp_2(sK1_skl,sK0_skl)|sQ22_spl),
% 0.31/0.50 inference(component_clause,[status(thm)],[f487])).
% 0.31/0.50 fof(f490,definition,(
% 0.31/0.50 ![X0]: (sQ23_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v4_pre_topc(X0,sK0_skl)|X0=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,X0))))),
% 0.31/0.50 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.31/0.50 fof(f491,plain,(
% 0.31/0.50 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v4_pre_topc(X0,sK0_skl)|X0=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,X0))|~sQ23_spl)),
% 0.31/0.50 inference(component_clause,[status(thm)],[f490])).
% 0.31/0.50 fof(f493,plain,(
% 0.31/0.50 sQ6_spl|~sQ19_spl|~sQ7_spl|~sQ22_spl|sQ23_spl),
% 0.31/0.50 inference(split_clause,[status(thm)],[f485,f387,f472,f390,f487,f490])).
% 0.31/0.50 fof(f501,plain,(
% 0.31/0.50 $false|sQ22_spl),
% 0.31/0.50 inference(forward_subsumption_resolution,[status(thm)],[f489,f86])).
% 0.31/0.50 fof(f502,plain,(
% 0.31/0.50 sQ22_spl),
% 0.31/0.50 inference(contradiction_clause,[status(thm)],[f501])).
% 0.31/0.50 fof(f1051,plain,(
% 0.31/0.50 ~v4_pre_topc(k6_pre_topc(sK0_skl,sK2_skl),sK0_skl)|k6_pre_topc(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k6_pre_topc(sK0_skl,sK2_skl)))|~sQ23_spl|~sQ15_spl),
% 0.31/0.50 inference(resolution,[status(thm)],[f491,f444])).
% 0.31/0.50 fof(f1057,definition,(
% 0.31/0.50 sQ97_spl <=> (k6_pre_topc(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k6_pre_topc(sK0_skl,sK2_skl))))),
% 0.31/0.50 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.31/0.50 fof(f1058,plain,(
% 0.31/0.50 k6_pre_topc(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k6_pre_topc(sK0_skl,sK2_skl)))|~sQ97_spl),
% 0.31/0.50 inference(component_clause,[status(thm)],[f1057])).
% 0.31/0.50 fof(f1060,plain,(
% 0.31/0.50 ~sQ21_spl|sQ97_spl|~sQ23_spl|~sQ15_spl),
% 0.31/0.50 inference(split_clause,[status(thm)],[f1051,f479,f1057,f490,f443])).
% 0.31/0.50 fof(f1093,plain,(
% 0.31/0.50 $false|~sQ97_spl),
% 0.31/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1058,f88])).
% 0.31/0.50 fof(f1094,plain,(
% 0.31/0.50 ~sQ97_spl),
% 0.31/0.50 inference(contradiction_clause,[status(thm)],[f1093])).
% 0.31/0.50 fof(f1095,plain,(
% 0.31/0.50 $false),
% 0.31/0.50 inference(sat_refutation,[status(thm)],[f432,f434,f446,f482,f484,f493,f502,f1060,f1094])).
% 0.31/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.31/0.53 % Elapsed time: 0.098066 seconds
% 0.31/0.53 % CPU time: 0.428534 seconds
% 0.31/0.53 % Total memory used: 113.461 MB
% 0.31/0.53 % Net memory used: 113.236 MB
%------------------------------------------------------------------------------