%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU388+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 02:22:30 PM UTC 2026
% Result : Theorem 69.49s 24.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU388+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/15.52 % Computer : n010.cluster.edu
% 0.09/15.52 % Model : x86_64 x86_64
% 0.09/15.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.52 % Memory : 8046.5625MB
% 0.09/15.52 % OS : Linux 6.8.0-71-generic
% 0.09/15.52 % CPULimit : 300
% 0.09/15.52 % WCLimit : 300
% 0.09/15.52 % DateTime : Mon Sep 21 06:18:57 UTC 2026
% 0.09/15.52 % CPUTime :
% 0.13/15.64 % Drodi V4.1.1
% 69.49/24.48 % Refutation found
% 69.49/24.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 69.49/24.48 % SZS output start CNFRefutation for theBenchmark
% 69.49/24.48 fof(f146,axiom,(
% 69.49/24.48 (! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( element(B,the_carrier(A))=> neighborhood_system(A,B) = a_2_0_yellow19(A,B) ) )) )),
% 69.49/24.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.49/24.48 fof(f458,axiom,(
% 69.49/24.48 (! [A,B,C] :( ( ~ empty_carrier(B)& topological_space(B)& top_str(B)& element(C,the_carrier(B)) )=> ( in(A,a_2_0_yellow19(B,C))<=> (? [D] :( point_neighbourhood(D,B,C)& A = D ) )) ) )),
% 69.49/24.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.49/24.48 fof(f791,conjecture,(
% 69.49/24.48 (! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( in(C,neighborhood_system(A,B))<=> point_neighbourhood(C,A,B) ) )) )) )),
% 69.49/24.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.49/24.48 fof(f792,negated_conjecture,(
% 69.49/24.48 ~((! [A] :( ( ~ empty_carrier(A)& topological_space(A)& top_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( in(C,neighborhood_system(A,B))<=> point_neighbourhood(C,A,B) ) )) )) ))),
% 69.49/24.48 inference(negated_conjecture,[status(cth)],[f791])).
% 69.49/24.48 fof(f1672,plain,(
% 69.49/24.48 ![A]: (((empty_carrier(A)|~topological_space(A))|~top_str(A))|(![B]: (~element(B,the_carrier(A))|neighborhood_system(A,B)=a_2_0_yellow19(A,B))))),
% 69.49/24.48 inference(pre_NNF_transformation,[status(thm)],[f146])).
% 69.49/24.48 fof(f1673,plain,(
% 69.49/24.48 ![X0,X1]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|neighborhood_system(X0,X1)=a_2_0_yellow19(X0,X1))),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f1672])).
% 69.49/24.48 fof(f2985,plain,(
% 69.49/24.48 ![A,B,C]: ((((empty_carrier(B)|~topological_space(B))|~top_str(B))|~element(C,the_carrier(B)))|(in(A,a_2_0_yellow19(B,C))<=>(?[D]: (point_neighbourhood(D,B,C)&A=D))))),
% 69.49/24.48 inference(pre_NNF_transformation,[status(thm)],[f458])).
% 69.49/24.48 fof(f2986,plain,(
% 69.49/24.48 ![A,B,C]: ((((empty_carrier(B)|~topological_space(B))|~top_str(B))|~element(C,the_carrier(B)))|((~in(A,a_2_0_yellow19(B,C))|(?[D]: (point_neighbourhood(D,B,C)&A=D)))&(in(A,a_2_0_yellow19(B,C))|(![D]: (~point_neighbourhood(D,B,C)|~A=D)))))),
% 69.49/24.48 inference(NNF_transformation,[status(thm)],[f2985])).
% 69.49/24.48 fof(f2987,plain,(
% 69.49/24.48 ![B,C]: ((((empty_carrier(B)|~topological_space(B))|~top_str(B))|~element(C,the_carrier(B)))|((![A]: (~in(A,a_2_0_yellow19(B,C))|(?[D]: (point_neighbourhood(D,B,C)&A=D))))&(![A]: (in(A,a_2_0_yellow19(B,C))|(![D]: (~point_neighbourhood(D,B,C)|~A=D))))))),
% 69.49/24.48 inference(miniscoping,[status(thm)],[f2986])).
% 69.49/24.48 fof(f2988,plain,(
% 69.49/24.48 ![B,C]: ((((empty_carrier(B)|~topological_space(B))|~top_str(B))|~element(C,the_carrier(B)))|((![A]: (~in(A,a_2_0_yellow19(B,C))|(point_neighbourhood(sK167_skl(A,C,B),B,C)&A=sK167_skl(A,C,B))))&(![A]: (in(A,a_2_0_yellow19(B,C))|(![D]: (~point_neighbourhood(D,B,C)|~A=D))))))),
% 69.49/24.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK167_skl]),skolemize(D,sK167_skl(A,C,B))],[f2987])).
% 69.49/24.48 fof(f2989,plain,(
% 69.49/24.48 ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|~in(X2,a_2_0_yellow19(X0,X1))|point_neighbourhood(sK167_skl(X2,X1,X0),X0,X1))),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f2988])).
% 69.49/24.48 fof(f2990,plain,(
% 69.49/24.48 ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|~in(X2,a_2_0_yellow19(X0,X1))|X2=sK167_skl(X2,X1,X0))),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f2988])).
% 69.49/24.48 fof(f2991,plain,(
% 69.49/24.48 ![X0,X1,X2,X3]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|in(X2,a_2_0_yellow19(X0,X1))|~point_neighbourhood(X3,X0,X1)|~X2=X3)),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f2988])).
% 69.49/24.48 fof(f4737,plain,(
% 69.49/24.48 (?[A]: (((~empty_carrier(A)&topological_space(A))&top_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: (in(C,neighborhood_system(A,B))<~>point_neighbourhood(C,A,B)))))))),
% 69.49/24.48 inference(pre_NNF_transformation,[status(thm)],[f792])).
% 69.49/24.48 fof(f4738,plain,(
% 69.49/24.48 ?[A]: (((~empty_carrier(A)&topological_space(A))&top_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: ((in(C,neighborhood_system(A,B))|point_neighbourhood(C,A,B))&(~in(C,neighborhood_system(A,B))|~point_neighbourhood(C,A,B)))))))),
% 69.49/24.48 inference(NNF_transformation,[status(thm)],[f4737])).
% 69.49/24.48 fof(f4739,plain,(
% 69.49/24.48 (((~empty_carrier(sK473_skl)&topological_space(sK473_skl))&top_str(sK473_skl))&(element(sK474_skl,the_carrier(sK473_skl))&((in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))|point_neighbourhood(sK475_skl,sK473_skl,sK474_skl))&(~in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))|~point_neighbourhood(sK475_skl,sK473_skl,sK474_skl)))))),
% 69.49/24.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK473_skl,sK474_skl,sK475_skl]),skolemize(A,sK473_skl),skolemize(B,sK474_skl),skolemize(C,sK475_skl)],[f4738])).
% 69.49/24.48 fof(f4740,plain,(
% 69.49/24.48 ~empty_carrier(sK473_skl)),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f4739])).
% 69.49/24.48 fof(f4741,plain,(
% 69.49/24.48 topological_space(sK473_skl)),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f4739])).
% 69.49/24.48 fof(f4742,plain,(
% 69.49/24.48 top_str(sK473_skl)),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f4739])).
% 69.49/24.48 fof(f4743,plain,(
% 69.49/24.48 element(sK474_skl,the_carrier(sK473_skl))),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f4739])).
% 69.49/24.48 fof(f4744,plain,(
% 69.49/24.48 in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))|point_neighbourhood(sK475_skl,sK473_skl,sK474_skl)),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f4739])).
% 69.49/24.48 fof(f4745,plain,(
% 69.49/24.48 ~in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))|~point_neighbourhood(sK475_skl,sK473_skl,sK474_skl)),
% 69.49/24.48 inference(cnf_transformation,[status(thm)],[f4739])).
% 69.49/24.48 fof(f5643,plain,(
% 69.49/24.48 ![X0,X1,X2]: (empty_carrier(X0)|~topological_space(X0)|~top_str(X0)|~element(X1,the_carrier(X0))|in(X2,a_2_0_yellow19(X0,X1))|~point_neighbourhood(X2,X0,X1))),
% 69.49/24.48 inference(destructive_equality_resolution,[status(thm)],[f2991])).
% 69.49/24.48 fof(f5826,plain,(
% 69.49/24.48 ![X0]: (empty_carrier(sK473_skl)|~top_str(sK473_skl)|~element(X0,the_carrier(sK473_skl))|neighborhood_system(sK473_skl,X0)=a_2_0_yellow19(sK473_skl,X0))),
% 69.49/24.48 inference(resolution,[status(thm)],[f1673,f4741])).
% 69.49/24.48 fof(f5827,plain,(
% 69.49/24.48 ![X0]: (~top_str(sK473_skl)|~element(X0,the_carrier(sK473_skl))|neighborhood_system(sK473_skl,X0)=a_2_0_yellow19(sK473_skl,X0))),
% 69.49/24.48 inference(forward_subsumption_resolution,[status(thm)],[f5826,f4740])).
% 69.49/24.48 fof(f5919,plain,(
% 69.49/24.48 ![X0]: (~element(X0,the_carrier(sK473_skl))|neighborhood_system(sK473_skl,X0)=a_2_0_yellow19(sK473_skl,X0))),
% 69.49/24.48 inference(forward_subsumption_resolution,[status(thm)],[f5827,f4742])).
% 69.49/24.48 fof(f5938,plain,(
% 69.49/24.48 neighborhood_system(sK473_skl,sK474_skl)=a_2_0_yellow19(sK473_skl,sK474_skl)),
% 69.49/24.48 inference(resolution,[status(thm)],[f5919,f4743])).
% 69.49/24.48 fof(f7756,plain,(
% 69.49/24.48 ![X0,X1]: (empty_carrier(sK473_skl)|~top_str(sK473_skl)|~element(X0,the_carrier(sK473_skl))|in(X1,a_2_0_yellow19(sK473_skl,X0))|~point_neighbourhood(X1,sK473_skl,X0))),
% 69.49/24.48 inference(resolution,[status(thm)],[f5643,f4741])).
% 69.49/24.48 fof(f7757,plain,(
% 69.49/24.48 ![X0,X1]: (~top_str(sK473_skl)|~element(X0,the_carrier(sK473_skl))|in(X1,a_2_0_yellow19(sK473_skl,X0))|~point_neighbourhood(X1,sK473_skl,X0))),
% 69.49/24.48 inference(forward_subsumption_resolution,[status(thm)],[f7756,f4740])).
% 69.49/24.48 fof(f7861,plain,(
% 69.49/24.48 ![X0,X1]: (~element(X0,the_carrier(sK473_skl))|in(X1,a_2_0_yellow19(sK473_skl,X0))|~point_neighbourhood(X1,sK473_skl,X0))),
% 69.49/24.49 inference(forward_subsumption_resolution,[status(thm)],[f7757,f4742])).
% 69.49/24.49 fof(f8487,plain,(
% 69.49/24.49 ![X0,X1]: (empty_carrier(sK473_skl)|~top_str(sK473_skl)|~element(X0,the_carrier(sK473_skl))|~in(X1,a_2_0_yellow19(sK473_skl,X0))|X1=sK167_skl(X1,X0,sK473_skl))),
% 69.49/24.49 inference(resolution,[status(thm)],[f2990,f4741])).
% 69.49/24.49 fof(f8488,plain,(
% 69.49/24.49 ![X0,X1]: (~top_str(sK473_skl)|~element(X0,the_carrier(sK473_skl))|~in(X1,a_2_0_yellow19(sK473_skl,X0))|X1=sK167_skl(X1,X0,sK473_skl))),
% 69.49/24.49 inference(forward_subsumption_resolution,[status(thm)],[f8487,f4740])).
% 69.49/24.49 fof(f8566,plain,(
% 69.49/24.49 ![X0,X1]: (~element(X0,the_carrier(sK473_skl))|~in(X1,a_2_0_yellow19(sK473_skl,X0))|X1=sK167_skl(X1,X0,sK473_skl))),
% 69.49/24.49 inference(forward_subsumption_resolution,[status(thm)],[f8488,f4742])).
% 69.49/24.49 fof(f8630,plain,(
% 69.49/24.49 ![X0]: (~in(X0,a_2_0_yellow19(sK473_skl,sK474_skl))|X0=sK167_skl(X0,sK474_skl,sK473_skl))),
% 69.49/24.49 inference(resolution,[status(thm)],[f8566,f4743])).
% 69.49/24.49 fof(f8637,plain,(
% 69.49/24.49 ![X0]: (~in(X0,neighborhood_system(sK473_skl,sK474_skl))|X0=sK167_skl(X0,sK474_skl,sK473_skl))),
% 70.32/24.53 inference(forward_demodulation,[status(thm)],[f5938,f8630])).
% 70.32/24.53 fof(f9145,plain,(
% 70.32/24.53 sK475_skl=sK167_skl(sK475_skl,sK474_skl,sK473_skl)|point_neighbourhood(sK475_skl,sK473_skl,sK474_skl)),
% 70.32/24.53 inference(resolution,[status(thm)],[f8637,f4744])).
% 70.32/24.53 fof(f9284,plain,(
% 70.32/24.53 sK475_skl=sK167_skl(sK475_skl,sK474_skl,sK473_skl)|~element(sK474_skl,the_carrier(sK473_skl))|in(sK475_skl,a_2_0_yellow19(sK473_skl,sK474_skl))),
% 70.32/24.53 inference(resolution,[status(thm)],[f9145,f7861])).
% 70.32/24.53 fof(f9286,plain,(
% 70.32/24.53 sK475_skl=sK167_skl(sK475_skl,sK474_skl,sK473_skl)|~element(sK474_skl,the_carrier(sK473_skl))|in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))),
% 70.32/24.53 inference(forward_demodulation,[status(thm)],[f5938,f9284])).
% 70.32/24.53 fof(f9287,plain,(
% 70.32/24.53 sK475_skl=sK167_skl(sK475_skl,sK474_skl,sK473_skl)|in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))),
% 70.32/24.53 inference(forward_subsumption_resolution,[status(thm)],[f9286,f4743])).
% 70.32/24.53 fof(f9314,plain,(
% 70.32/24.53 sK475_skl=sK167_skl(sK475_skl,sK474_skl,sK473_skl)),
% 70.32/24.53 inference(forward_subsumption_resolution,[status(thm)],[f9287,f8637])).
% 70.32/24.53 fof(f10468,plain,(
% 70.32/24.53 ![X0,X1]: (empty_carrier(sK473_skl)|~top_str(sK473_skl)|~element(X0,the_carrier(sK473_skl))|~in(X1,a_2_0_yellow19(sK473_skl,X0))|point_neighbourhood(sK167_skl(X1,X0,sK473_skl),sK473_skl,X0))),
% 70.32/24.53 inference(resolution,[status(thm)],[f2989,f4741])).
% 70.32/24.53 fof(f10469,plain,(
% 70.32/24.53 ![X0,X1]: (~top_str(sK473_skl)|~element(X0,the_carrier(sK473_skl))|~in(X1,a_2_0_yellow19(sK473_skl,X0))|point_neighbourhood(sK167_skl(X1,X0,sK473_skl),sK473_skl,X0))),
% 70.32/24.53 inference(forward_subsumption_resolution,[status(thm)],[f10468,f4740])).
% 70.32/24.53 fof(f10486,plain,(
% 70.32/24.53 ![X0,X1]: (~element(X0,the_carrier(sK473_skl))|~in(X1,a_2_0_yellow19(sK473_skl,X0))|point_neighbourhood(sK167_skl(X1,X0,sK473_skl),sK473_skl,X0))),
% 70.32/24.53 inference(forward_subsumption_resolution,[status(thm)],[f10469,f4742])).
% 70.32/24.53 fof(f10490,plain,(
% 70.32/24.53 ~element(sK474_skl,the_carrier(sK473_skl))|~in(sK475_skl,a_2_0_yellow19(sK473_skl,sK474_skl))|point_neighbourhood(sK475_skl,sK473_skl,sK474_skl)),
% 70.32/24.53 inference(paramodulation,[status(thm)],[f9314,f10486])).
% 70.32/24.53 fof(f10494,plain,(
% 70.32/24.53 ~element(sK474_skl,the_carrier(sK473_skl))|~in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))|point_neighbourhood(sK475_skl,sK473_skl,sK474_skl)),
% 70.32/24.53 inference(forward_demodulation,[status(thm)],[f5938,f10490])).
% 70.32/24.53 fof(f10495,plain,(
% 70.32/24.53 ~in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))|point_neighbourhood(sK475_skl,sK473_skl,sK474_skl)),
% 70.32/24.53 inference(forward_subsumption_resolution,[status(thm)],[f10494,f4743])).
% 70.32/24.53 fof(f11364,plain,(
% 70.32/24.53 ~in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))),
% 70.32/24.53 inference(backward_subsumption_resolution,[status(thm)],[f4745,f11366])).
% 70.32/24.53 fof(f11366,plain,(
% 70.32/24.53 point_neighbourhood(sK475_skl,sK473_skl,sK474_skl)),
% 70.32/24.53 inference(forward_subsumption_resolution,[status(thm)],[f10495,f4744])).
% 70.32/24.53 fof(f11368,plain,(
% 70.32/24.53 ~element(sK474_skl,the_carrier(sK473_skl))|in(sK475_skl,a_2_0_yellow19(sK473_skl,sK474_skl))),
% 70.32/24.53 inference(resolution,[status(thm)],[f11366,f7861])).
% 70.32/24.53 fof(f11371,plain,(
% 70.32/24.53 ~element(sK474_skl,the_carrier(sK473_skl))|in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))),
% 70.32/24.53 inference(forward_demodulation,[status(thm)],[f5938,f11368])).
% 70.32/24.53 fof(f11372,plain,(
% 70.32/24.53 in(sK475_skl,neighborhood_system(sK473_skl,sK474_skl))),
% 70.32/24.53 inference(forward_subsumption_resolution,[status(thm)],[f11371,f4743])).
% 70.32/24.53 fof(f17787,plain,(
% 70.32/24.53 $false),
% 70.32/24.53 inference(forward_subsumption_resolution,[status(thm)],[f11372,f11364])).
% 70.32/24.53 % SZS output end CNFRefutation for theBenchmark.p
% 70.32/24.58 % Elapsed time: 9.042364 seconds
% 70.32/24.58 % CPU time: 70.692742 seconds
% 70.32/24.58 % Total memory used: 683.376 MB
% 70.32/24.58 % Net memory used: 648.542 MB
%------------------------------------------------------------------------------