%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP028+1 : 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 : n007.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.17s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : TOP028+1 : 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.17/0.44 % Computer : n007.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 12:39:05 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 0.17/0.53 % Refutation found
% 0.17/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.53 fof(f1,conjecture,(
% 0.17/0.53 (! [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) ) )) )),
% 0.17/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.53 fof(f2,negated_conjecture,(
% 0.17/0.53 ~((! [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) ) )) ))),
% 0.17/0.53 inference(negated_conjecture,[status(cth)],[f1])).
% 0.17/0.53 fof(f39,axiom,(
% 0.17/0.53 ( v1_xboole_0(k1_xboole_0)& v1_membered(k1_xboole_0)& v2_membered(k1_xboole_0)& v3_membered(k1_xboole_0)& v4_membered(k1_xboole_0)& v5_membered(k1_xboole_0) ) ),
% 0.17/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.53 fof(f44,axiom,(
% 0.17/0.53 (! [A] :(? [B] :( m1_subset_1(B,k1_zfmisc_1(A))& v1_xboole_0(B) ) ))),
% 0.17/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.53 fof(f54,axiom,(
% 0.17/0.53 (! [A] :( ( ~ v3_struct_0(A)& l1_pre_topc(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( v3_tex_2(B,A)=> v1_tsp_1(B,A) ) ) )) )),
% 0.17/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.53 fof(f57,axiom,(
% 0.17/0.53 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> (! [B] :( ( v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> v3_tex_2(B,A) ) )) )),
% 0.17/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.53 fof(f61,axiom,(
% 0.17/0.53 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 0.17/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.53 fof(f64,axiom,(
% 0.17/0.53 (! [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_1(B,A)& (! [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))=> ~ ( r1_tarski(B,C)& v1_tsp_2(C,A) ) ) )) ) )) )),
% 0.17/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.53 fof(f65,plain,(
% 0.17/0.53 (?[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)))))),
% 0.17/0.53 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.17/0.53 fof(f66,plain,(
% 0.17/0.53 (((~v3_struct_0(sK0_skl)&v2_pre_topc(sK0_skl))&l1_pre_topc(sK0_skl))&(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v1_tsp_2(B,sK0_skl))))),
% 0.17/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f65])).
% 0.17/0.53 fof(f67,plain,(
% 0.17/0.53 ~v3_struct_0(sK0_skl)),
% 0.17/0.53 inference(cnf_transformation,[status(thm)],[f66])).
% 0.17/0.53 fof(f68,plain,(
% 0.17/0.53 v2_pre_topc(sK0_skl)),
% 0.17/0.53 inference(cnf_transformation,[status(thm)],[f66])).
% 0.17/0.53 fof(f69,plain,(
% 0.17/0.53 l1_pre_topc(sK0_skl)),
% 0.17/0.53 inference(cnf_transformation,[status(thm)],[f66])).
% 0.17/0.53 fof(f70,plain,(
% 0.17/0.53 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~v1_tsp_2(X0,sK0_skl))),
% 0.17/0.53 inference(cnf_transformation,[status(thm)],[f66])).
% 0.17/0.53 fof(f178,plain,(
% 0.17/0.53 v1_xboole_0(k1_xboole_0)),
% 0.17/0.53 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.53 fof(f208,plain,(
% 0.17/0.53 ![A]: (m1_subset_1(sK7_skl(A),k1_zfmisc_1(A))&v1_xboole_0(sK7_skl(A)))),
% 0.17/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f44])).
% 0.17/0.53 fof(f209,plain,(
% 0.17/0.53 ![X0]: (m1_subset_1(sK7_skl(X0),k1_zfmisc_1(X0)))),
% 0.17/0.53 inference(cnf_transformation,[status(thm)],[f208])).
% 0.17/0.53 fof(f210,plain,(
% 0.17/0.53 ![X0]: (v1_xboole_0(sK7_skl(X0)))),
% 0.17/0.53 inference(cnf_transformation,[status(thm)],[f208])).
% 0.17/0.53 fof(f263,plain,(
% 0.17/0.53 ![A]: ((v3_struct_0(A)|~l1_pre_topc(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|(~v3_tex_2(B,A)|v1_tsp_1(B,A)))))),
% 0.17/0.53 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.17/0.53 fof(f264,plain,(
% 0.17/0.53 ![X0,X1]: (v3_struct_0(X0)|~l1_pre_topc(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v3_tex_2(X1,X0)|v1_tsp_1(X1,X0))),
% 0.17/0.53 inference(cnf_transformation,[status(thm)],[f263])).
% 0.17/0.53 fof(f269,plain,(
% 0.17/0.53 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|(![B]: ((~v1_xboole_0(B)|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|v3_tex_2(B,A))))),
% 0.17/0.53 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.17/0.53 fof(f270,plain,(
% 0.17/0.53 ![X0,X1]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v3_tex_2(X1,X0))),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f269])).
% 0.23/0.54 fof(f281,plain,(
% 0.23/0.54 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 0.23/0.54 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.23/0.54 fof(f282,plain,(
% 0.23/0.54 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f281])).
% 0.23/0.54 fof(f289,plain,(
% 0.23/0.54 ![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_1(B,A)|(?[C]: (m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))&(r1_tarski(B,C)&v1_tsp_2(C,A))))))))),
% 0.23/0.54 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.23/0.54 fof(f290,plain,(
% 0.23/0.54 ![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_1(B,A)|(m1_subset_1(sK16_skl(B,A),k1_zfmisc_1(u1_struct_0(A)))&(r1_tarski(B,sK16_skl(B,A))&v1_tsp_2(sK16_skl(B,A),A)))))))),
% 0.23/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(C,sK16_skl(B,A))],[f289])).
% 0.23/0.54 fof(f291,plain,(
% 0.23/0.54 ![X0,X1]: (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_1(X1,X0)|m1_subset_1(sK16_skl(X1,X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f290])).
% 0.23/0.54 fof(f293,plain,(
% 0.23/0.54 ![X0,X1]: (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_1(X1,X0)|v1_tsp_2(sK16_skl(X1,X0),X0))),
% 0.23/0.54 inference(cnf_transformation,[status(thm)],[f290])).
% 0.23/0.54 fof(f303,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(X0)))|v3_tex_2(k1_xboole_0,X0))),
% 0.23/0.54 inference(resolution,[status(thm)],[f270,f178])).
% 0.23/0.54 fof(f420,plain,(
% 0.23/0.54 ![X0]: (sK7_skl(X0)=k1_xboole_0)),
% 0.23/0.54 inference(resolution,[status(thm)],[f282,f210])).
% 0.23/0.54 fof(f440,plain,(
% 0.23/0.54 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 0.23/0.54 inference(backward_demodulation,[status(thm)],[f420,f209])).
% 0.23/0.54 fof(f446,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_tex_2(k1_xboole_0,X0))),
% 0.23/0.54 inference(backward_subsumption_resolution,[status(thm)],[f303,f440])).
% 0.23/0.54 fof(f447,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X0)|~l1_pre_topc(X0)|~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_1(k1_xboole_0,X0))),
% 0.23/0.54 inference(resolution,[status(thm)],[f446,f264])).
% 0.23/0.54 fof(f448,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(X0)))|v1_tsp_1(k1_xboole_0,X0))),
% 0.23/0.54 inference(duplicate_literals_removal,[status(thm)],[f447])).
% 0.23/0.54 fof(f449,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_tsp_1(k1_xboole_0,X0))),
% 0.23/0.54 inference(forward_subsumption_resolution,[status(thm)],[f448,f440])).
% 0.23/0.54 fof(f450,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(X0)))|m1_subset_1(sK16_skl(k1_xboole_0,X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 0.23/0.54 inference(resolution,[status(thm)],[f449,f291])).
% 0.23/0.54 fof(f451,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(X0)))|m1_subset_1(sK16_skl(k1_xboole_0,X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 0.23/0.54 inference(duplicate_literals_removal,[status(thm)],[f450])).
% 0.23/0.54 fof(f452,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m1_subset_1(sK16_skl(k1_xboole_0,X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 0.23/0.54 inference(forward_subsumption_resolution,[status(thm)],[f451,f440])).
% 0.23/0.54 fof(f457,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~v1_tsp_1(k1_xboole_0,X0)|v1_tsp_2(sK16_skl(k1_xboole_0,X0),X0))),
% 0.23/0.54 inference(resolution,[status(thm)],[f440,f293])).
% 0.23/0.54 fof(f458,plain,(
% 0.23/0.54 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_tsp_2(sK16_skl(k1_xboole_0,X0),X0))),
% 0.23/0.54 inference(forward_subsumption_resolution,[status(thm)],[f457,f449])).
% 0.23/0.54 fof(f459,plain,(
% 0.23/0.54 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|~m1_subset_1(sK16_skl(k1_xboole_0,sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.23/0.54 inference(resolution,[status(thm)],[f458,f70])).
% 0.23/0.55 fof(f460,plain,(
% 0.23/0.55 ~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|~m1_subset_1(sK16_skl(k1_xboole_0,sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.23/0.55 inference(forward_subsumption_resolution,[status(thm)],[f459,f67])).
% 0.23/0.55 fof(f462,plain,(
% 0.23/0.55 ~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)),
% 0.23/0.55 inference(resolution,[status(thm)],[f460,f452])).
% 0.23/0.55 fof(f464,plain,(
% 0.23/0.55 ~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_struct_0(sK0_skl)),
% 0.23/0.55 inference(duplicate_literals_removal,[status(thm)],[f462])).
% 0.23/0.55 fof(f465,plain,(
% 0.23/0.55 ~l1_pre_topc(sK0_skl)|v3_struct_0(sK0_skl)),
% 0.23/0.55 inference(forward_subsumption_resolution,[status(thm)],[f464,f68])).
% 0.23/0.55 fof(f467,plain,(
% 0.23/0.55 v3_struct_0(sK0_skl)),
% 0.23/0.55 inference(resolution,[status(thm)],[f465,f69])).
% 0.23/0.55 fof(f468,plain,(
% 0.23/0.55 $false),
% 0.23/0.55 inference(forward_subsumption_resolution,[status(thm)],[f467,f67])).
% 0.23/0.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.57 % Elapsed time: 0.097926 seconds
% 0.23/0.57 % CPU time: 0.496868 seconds
% 0.23/0.57 % Total memory used: 88.025 MB
% 0.23/0.57 % Net memory used: 87.782 MB
%------------------------------------------------------------------------------