%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP027+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 : n011.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 0.02s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP027+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 12:39:55 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.38 % Drodi V4.1.1
% 0.02/0.42 % Refutation found
% 0.02/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.02/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.02/0.42 fof(f1,conjecture,(
% 0.02/0.42 (! [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))) ) )) ) )) )),
% 0.02/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.42 fof(f2,negated_conjecture,(
% 0.02/0.42 ~((! [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))) ) )) ) )) ))),
% 0.02/0.42 inference(negated_conjecture,[status(cth)],[f1])).
% 0.02/0.42 fof(f69,axiom,(
% 0.02/0.42 (! [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))) ) )),
% 0.02/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.42 fof(f77,axiom,(
% 0.02/0.42 (! [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) ) )),
% 0.02/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.42 fof(f80,axiom,(
% 0.02/0.42 (! [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)) ) ) )) ) )) )),
% 0.02/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.42 fof(f81,plain,(
% 0.02/0.42 (?[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))))))))))),
% 0.02/0.42 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.02/0.42 fof(f82,plain,(
% 0.02/0.42 (((~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)))&~k1_tops_1(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k1_tops_1(sK0_skl,sK2_skl)))))))),
% 0.02/0.42 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)],[f81])).
% 0.02/0.42 fof(f83,plain,(
% 0.02/0.42 ~v3_struct_0(sK0_skl)),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f82])).
% 0.02/0.42 fof(f84,plain,(
% 0.02/0.42 v2_pre_topc(sK0_skl)),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f82])).
% 0.02/0.42 fof(f85,plain,(
% 0.02/0.42 l1_pre_topc(sK0_skl)),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f82])).
% 0.02/0.42 fof(f86,plain,(
% 0.02/0.42 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f82])).
% 0.02/0.42 fof(f87,plain,(
% 0.02/0.42 v1_tsp_2(sK1_skl,sK0_skl)),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f82])).
% 0.02/0.42 fof(f88,plain,(
% 0.02/0.42 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f82])).
% 0.02/0.42 fof(f89,plain,(
% 0.02/0.42 ~k1_tops_1(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k1_tops_1(sK0_skl,sK2_skl)))),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f82])).
% 0.02/0.42 fof(f336,plain,(
% 0.02/0.42 ![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))))),
% 0.02/0.42 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 0.02/0.42 fof(f337,plain,(
% 0.02/0.42 ![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))))),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f336])).
% 0.02/0.42 fof(f345,plain,(
% 0.02/0.42 ![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))),
% 0.02/0.42 inference(pre_NNF_transformation,[status(thm)],[f77])).
% 0.02/0.42 fof(f346,plain,(
% 0.02/0.42 ![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))),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f345])).
% 0.02/0.42 fof(f355,plain,(
% 0.02/0.42 ![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)))))))))),
% 0.02/0.42 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 0.02/0.42 fof(f356,plain,(
% 0.02/0.42 ![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)))),
% 0.02/0.42 inference(cnf_transformation,[status(thm)],[f355])).
% 0.02/0.42 fof(f372,definition,(
% 0.02/0.42 sQ3_spl <=> (l1_pre_topc(sK0_skl))),
% 0.02/0.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.02/0.42 fof(f374,plain,(
% 0.02/0.42 ~l1_pre_topc(sK0_skl)|sQ3_spl),
% 0.02/0.42 inference(component_clause,[status(thm)],[f372])).
% 0.02/0.42 fof(f389,plain,(
% 0.02/0.42 $false|sQ3_spl),
% 0.02/0.42 inference(forward_subsumption_resolution,[status(thm)],[f374,f85])).
% 0.02/0.42 fof(f390,plain,(
% 0.02/0.42 sQ3_spl),
% 0.02/0.42 inference(contradiction_clause,[status(thm)],[f389])).
% 0.02/0.42 fof(f587,plain,(
% 0.02/0.42 ~l1_pre_topc(sK0_skl)|m1_subset_1(k1_tops_1(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.02/0.42 inference(resolution,[status(thm)],[f337,f88])).
% 0.02/0.42 fof(f592,definition,(
% 0.02/0.42 sQ33_spl <=> (m1_subset_1(k1_tops_1(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.02/0.42 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.02/0.42 fof(f593,plain,(
% 0.02/0.42 m1_subset_1(k1_tops_1(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ33_spl),
% 0.02/0.42 inference(component_clause,[status(thm)],[f592])).
% 0.02/0.42 fof(f595,plain,(
% 0.02/0.42 ~sQ3_spl|sQ33_spl),
% 0.02/0.42 inference(split_clause,[status(thm)],[f587,f372,f592])).
% 0.02/0.42 fof(f712,definition,(
% 0.02/0.42 sQ51_spl <=> (v3_struct_0(sK0_skl))),
% 0.02/0.42 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.02/0.42 fof(f713,plain,(
% 0.02/0.42 v3_struct_0(sK0_skl)|~sQ51_spl),
% 0.02/0.42 inference(component_clause,[status(thm)],[f712])).
% 0.02/0.42 fof(f727,plain,(
% 0.02/0.42 $false|~sQ51_spl),
% 0.02/0.42 inference(forward_subsumption_resolution,[status(thm)],[f713,f83])).
% 0.02/0.42 fof(f728,plain,(
% 0.02/0.42 ~sQ51_spl),
% 0.02/0.42 inference(contradiction_clause,[status(thm)],[f727])).
% 0.02/0.42 fof(f766,plain,(
% 0.02/0.42 ~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_pre_topc(k1_tops_1(sK0_skl,sK2_skl),sK0_skl)),
% 0.02/0.42 inference(resolution,[status(thm)],[f346,f88])).
% 0.02/0.42 fof(f767,definition,(
% 0.02/0.42 sQ58_spl <=> (v2_pre_topc(sK0_skl))),
% 0.02/0.42 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.02/0.42 fof(f769,plain,(
% 0.02/0.42 ~v2_pre_topc(sK0_skl)|sQ58_spl),
% 0.02/0.42 inference(component_clause,[status(thm)],[f767])).
% 0.02/0.42 fof(f778,definition,(
% 0.02/0.42 sQ61_spl <=> (v3_pre_topc(k1_tops_1(sK0_skl,sK2_skl),sK0_skl))),
% 0.02/0.42 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.02/0.42 fof(f781,plain,(
% 0.02/0.42 ~sQ58_spl|~sQ3_spl|sQ61_spl),
% 0.02/0.42 inference(split_clause,[status(thm)],[f766,f767,f372,f778])).
% 0.02/0.42 fof(f782,plain,(
% 0.02/0.42 $false|sQ58_spl),
% 0.02/0.42 inference(forward_subsumption_resolution,[status(thm)],[f769,f84])).
% 0.02/0.42 fof(f783,plain,(
% 0.02/0.42 sQ58_spl),
% 0.02/0.42 inference(contradiction_clause,[status(thm)],[f782])).
% 0.02/0.43 fof(f785,plain,(
% 0.02/0.43 ![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)))|~v3_pre_topc(X0,sK0_skl)|X0=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,X0)))),
% 0.02/0.43 inference(resolution,[status(thm)],[f356,f86])).
% 0.02/0.43 fof(f794,definition,(
% 0.02/0.43 sQ64_spl <=> (v1_tsp_2(sK1_skl,sK0_skl))),
% 0.02/0.43 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.02/0.43 fof(f796,plain,(
% 0.02/0.43 ~v1_tsp_2(sK1_skl,sK0_skl)|sQ64_spl),
% 0.02/0.43 inference(component_clause,[status(thm)],[f794])).
% 0.02/0.43 fof(f797,definition,(
% 0.02/0.43 ![X0]: (sQ65_spl <=> (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v3_pre_topc(X0,sK0_skl)|X0=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,X0))))),
% 0.02/0.43 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.02/0.43 fof(f798,plain,(
% 0.02/0.43 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v3_pre_topc(X0,sK0_skl)|X0=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,X0))|~sQ65_spl)),
% 0.02/0.43 inference(component_clause,[status(thm)],[f797])).
% 0.02/0.43 fof(f800,plain,(
% 0.02/0.43 sQ51_spl|~sQ58_spl|~sQ3_spl|~sQ64_spl|sQ65_spl),
% 0.02/0.43 inference(split_clause,[status(thm)],[f785,f712,f767,f372,f794,f797])).
% 0.02/0.43 fof(f808,plain,(
% 0.02/0.43 $false|sQ64_spl),
% 0.02/0.43 inference(forward_subsumption_resolution,[status(thm)],[f796,f87])).
% 0.02/0.43 fof(f809,plain,(
% 0.02/0.43 sQ64_spl),
% 0.02/0.43 inference(contradiction_clause,[status(thm)],[f808])).
% 0.02/0.43 fof(f1360,plain,(
% 0.02/0.43 ~v3_pre_topc(k1_tops_1(sK0_skl,sK2_skl),sK0_skl)|k1_tops_1(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k1_tops_1(sK0_skl,sK2_skl)))|~sQ65_spl|~sQ33_spl),
% 0.02/0.43 inference(resolution,[status(thm)],[f798,f593])).
% 0.02/0.43 fof(f1378,definition,(
% 0.02/0.43 sQ145_spl <=> (k1_tops_1(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k1_tops_1(sK0_skl,sK2_skl))))),
% 0.02/0.43 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 0.02/0.43 fof(f1379,plain,(
% 0.02/0.43 k1_tops_1(sK0_skl,sK2_skl)=k3_tex_4(sK0_skl,k5_subset_1(u1_struct_0(sK0_skl),sK1_skl,k1_tops_1(sK0_skl,sK2_skl)))|~sQ145_spl),
% 0.02/0.43 inference(component_clause,[status(thm)],[f1378])).
% 0.02/0.43 fof(f1381,plain,(
% 0.02/0.43 ~sQ61_spl|sQ145_spl|~sQ65_spl|~sQ33_spl),
% 0.02/0.43 inference(split_clause,[status(thm)],[f1360,f778,f1378,f797,f592])).
% 0.02/0.43 fof(f1400,plain,(
% 0.02/0.43 $false|~sQ145_spl),
% 0.02/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1379,f89])).
% 0.02/0.43 fof(f1401,plain,(
% 0.02/0.43 ~sQ145_spl),
% 0.02/0.43 inference(contradiction_clause,[status(thm)],[f1400])).
% 0.02/0.43 fof(f1402,plain,(
% 0.02/0.43 $false),
% 0.02/0.43 inference(sat_refutation,[status(thm)],[f390,f595,f728,f781,f783,f800,f809,f1381,f1401])).
% 0.02/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.02/0.46 % Elapsed time: 0.080800 seconds
% 0.02/0.46 % CPU time: 0.276940 seconds
% 0.02/0.46 % Total memory used: 111.950 MB
% 0.02/0.46 % Net memory used: 111.727 MB
%------------------------------------------------------------------------------