%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU341+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:20:13 PM UTC 2026
% Result : Theorem 0.42s 1.16s
% Output : CNFRefutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 18
% Syntax : Number of formulae : 83 ( 18 unt; 12 def)
% Number of atoms : 270 ( 11 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 311 ( 124 ~; 114 |; 35 &)
% ( 18 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 13 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 76 ( 73 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f51,axiom,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ( point_neighbourhood(C,A,B)
<=> in(B,interior(A,C)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f432,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f528,lemma,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( top_str(B)
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ! [D] :
( element(D,powerset(the_carrier(B)))
=> ( ( interior(A,C) = C
=> open_subset(C,A) )
& ( open_subset(D,B)
=> interior(B,D) = D ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f531,conjecture,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,the_carrier(A))
=> ( ( in(C,B)
& open_subset(B,A) )
=> point_neighbourhood(B,A,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f532,negated_conjecture,
~ ! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,the_carrier(A))
=> ( ( in(C,B)
& open_subset(B,A) )
=> point_neighbourhood(B,A,C) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f531]) ).
fof(f554,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f786,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( point_neighbourhood(C,A,B)
<=> in(B,interior(A,C)) )
| ~ element(C,powerset(the_carrier(A))) )
| ~ element(B,the_carrier(A)) )
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f787,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ in(B,interior(A,C))
| point_neighbourhood(C,A,B) )
& ( in(B,interior(A,C))
| ~ point_neighbourhood(C,A,B) ) )
| ~ element(C,powerset(the_carrier(A))) )
| ~ element(B,the_carrier(A)) )
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f786]) ).
fof(f789,plain,
! [X0,X1,X2] :
( ~ in(X1,interior(X0,X2))
| point_neighbourhood(X2,X0,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ element(X1,the_carrier(X0))
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f787]) ).
fof(f974,plain,
! [A,B] :
( ( ( element(B,A)
<=> empty(B) )
| ~ empty(A) )
& ( ( element(B,A)
<=> in(B,A) )
| empty(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f78]) ).
fof(f975,plain,
! [A,B] :
( ( ( ( ~ empty(B)
| element(B,A) )
& ( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ( ( ( ~ in(B,A)
| element(B,A) )
& ( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(NNF_transformation,[status(thm)],[f974]) ).
fof(f976,plain,
( ! [A] :
( ( ! [B] :
( ~ empty(B)
| element(B,A) )
& ! [B] :
( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ! [A] :
( ( ! [B] :
( ~ in(B,A)
| element(B,A) )
& ! [B] :
( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(miniscoping,[status(thm)],[f975]) ).
fof(f977,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f976]) ).
fof(f2537,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f432]) ).
fof(f2538,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2537]) ).
fof(f2852,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( open_subset(C,A)
| interior(A,C) != C )
& ( interior(B,D) = D
| ~ open_subset(D,B) ) )
| ~ element(D,powerset(the_carrier(B))) )
| ~ element(C,powerset(the_carrier(A))) )
| ~ top_str(B) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f528]) ).
fof(f2853,plain,
! [X0,X1,X2,X3] :
( interior(X1,X3) = X3
| ~ open_subset(X3,X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ element(X2,powerset(the_carrier(X0)))
| ~ top_str(X1)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f2852]) ).
fof(f2862,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ point_neighbourhood(B,A,C)
& in(C,B)
& open_subset(B,A)
& element(C,the_carrier(A)) )
& element(B,powerset(the_carrier(A))) )
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f532]) ).
fof(f2863,plain,
( ~ point_neighbourhood(sK363_skl,sK362_skl,sK364_skl)
& in(sK364_skl,sK363_skl)
& open_subset(sK363_skl,sK362_skl)
& element(sK364_skl,the_carrier(sK362_skl))
& element(sK363_skl,powerset(the_carrier(sK362_skl)))
& top_str(sK362_skl)
& topological_space(sK362_skl)
& ~ empty_carrier(sK362_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK362_skl,sK363_skl,sK364_skl]),skolemize(A,sK362_skl),skolemize(B,sK363_skl),skolemize(C,sK364_skl)],[f2862]) ).
fof(f2864,plain,
~ empty_carrier(sK362_skl),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2865,plain,
topological_space(sK362_skl),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2866,plain,
top_str(sK362_skl),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2867,plain,
element(sK363_skl,powerset(the_carrier(sK362_skl))),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2868,plain,
element(sK364_skl,the_carrier(sK362_skl)),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2869,plain,
open_subset(sK363_skl,sK362_skl),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2870,plain,
in(sK364_skl,sK363_skl),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2871,plain,
~ point_neighbourhood(sK363_skl,sK362_skl,sK364_skl),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2935,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f554]) ).
fof(f2936,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f2935]) ).
fof(f2937,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2936]) ).
fof(f3670,definition,
! [X0,X2] :
( sQ31_spl
<=> ( ~ element(X2,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f3671,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(component_clause,[status(thm)],[f3670]) ).
fof(f3673,definition,
! [X1,X3] :
( sQ32_spl
<=> ( interior(X1,X3) = X3
| ~ open_subset(X3,X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ top_str(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f3674,plain,
! [X0,X1] :
( ~ sQ32_spl
| interior(X0,X1) = X1
| ~ open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(component_clause,[status(thm)],[f3673]) ).
fof(f3676,plain,
( sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f2853,f3670,f3673]) ).
fof(f4112,plain,
! [X0] :
( ~ in(sK364_skl,interior(sK362_skl,X0))
| point_neighbourhood(X0,sK362_skl,sK364_skl)
| ~ element(X0,powerset(the_carrier(sK362_skl)))
| ~ top_str(sK362_skl)
| ~ topological_space(sK362_skl)
| empty_carrier(sK362_skl) ),
inference(resolution,[status(thm)],[f2868,f789]) ).
fof(f4114,definition,
( sQ61_spl
<=> empty_carrier(sK362_skl) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f4115,plain,
( ~ sQ61_spl
| empty_carrier(sK362_skl) ),
inference(component_clause,[status(thm)],[f4114]) ).
fof(f4117,definition,
( sQ62_spl
<=> topological_space(sK362_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f4119,plain,
( sQ62_spl
| ~ topological_space(sK362_skl) ),
inference(component_clause,[status(thm)],[f4117]) ).
fof(f4120,definition,
( sQ63_spl
<=> top_str(sK362_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f4122,plain,
( sQ63_spl
| ~ top_str(sK362_skl) ),
inference(component_clause,[status(thm)],[f4120]) ).
fof(f4123,definition,
! [X0] :
( sQ64_spl
<=> ( ~ in(sK364_skl,interior(sK362_skl,X0))
| point_neighbourhood(X0,sK362_skl,sK364_skl)
| ~ element(X0,powerset(the_carrier(sK362_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f4124,plain,
! [X0] :
( ~ sQ64_spl
| ~ in(sK364_skl,interior(sK362_skl,X0))
| point_neighbourhood(X0,sK362_skl,sK364_skl)
| ~ element(X0,powerset(the_carrier(sK362_skl))) ),
inference(component_clause,[status(thm)],[f4123]) ).
fof(f4126,plain,
( sQ64_spl
| ~ sQ63_spl
| ~ sQ62_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f4112,f4114,f4117,f4120,f4123]) ).
fof(f4131,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4122,f2866]) ).
fof(f4132,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f4131]) ).
fof(f4133,plain,
( sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4119,f2865]) ).
fof(f4134,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f4133]) ).
fof(f4135,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4115,f2864]) ).
fof(f4136,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f4135]) ).
fof(f4137,plain,
element(sK364_skl,sK363_skl),
inference(resolution,[status(thm)],[f2538,f2870]) ).
fof(f4160,definition,
( sQ70_spl
<=> element(sK363_skl,powerset(the_carrier(sK362_skl))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f4162,plain,
( sQ70_spl
| ~ element(sK363_skl,powerset(the_carrier(sK362_skl))) ),
inference(component_clause,[status(thm)],[f4160]) ).
fof(f4214,plain,
~ empty(sK363_skl),
inference(resolution,[status(thm)],[f2937,f2870]) ).
fof(f4233,plain,
( in(sK364_skl,sK363_skl)
| empty(sK363_skl) ),
inference(resolution,[status(thm)],[f977,f4137]) ).
fof(f4245,definition,
( sQ80_spl
<=> empty(sK363_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f4246,plain,
( ~ sQ80_spl
| empty(sK363_skl) ),
inference(component_clause,[status(thm)],[f4245]) ).
fof(f4248,definition,
( sQ81_spl
<=> in(sK364_skl,sK363_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f4251,plain,
( sQ81_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f4233,f4245,f4248]) ).
fof(f4276,plain,
( ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4246,f4214]) ).
fof(f4277,plain,
~ sQ80_spl,
inference(contradiction_clause,[status(thm)],[f4276]) ).
fof(f4302,plain,
! [X0] :
( ~ sQ31_spl
| ~ element(X0,powerset(the_carrier(sK362_skl)))
| ~ top_str(sK362_skl) ),
inference(resolution,[status(thm)],[f3671,f2865]) ).
fof(f4303,definition,
! [X0] :
( sQ91_spl
<=> ~ element(X0,powerset(the_carrier(sK362_skl))) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f4304,plain,
! [X0] :
( ~ sQ91_spl
| ~ element(X0,powerset(the_carrier(sK362_skl))) ),
inference(component_clause,[status(thm)],[f4303]) ).
fof(f4306,plain,
( ~ sQ31_spl
| sQ91_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f4302,f4120,f4303,f3670]) ).
fof(f4307,plain,
( ~ sQ91_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2867,f4304]) ).
fof(f4308,plain,
~ sQ91_spl,
inference(contradiction_clause,[status(thm)],[f4307]) ).
fof(f4729,plain,
( sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4162,f2867]) ).
fof(f4730,plain,
sQ70_spl,
inference(contradiction_clause,[status(thm)],[f4729]) ).
fof(f4864,plain,
! [X0] :
( ~ sQ32_spl
| interior(sK362_skl,X0) = X0
| ~ open_subset(X0,sK362_skl)
| ~ element(X0,powerset(the_carrier(sK362_skl))) ),
inference(resolution,[status(thm)],[f3674,f2866]) ).
fof(f4871,plain,
( ~ sQ32_spl
| interior(sK362_skl,sK363_skl) = sK363_skl
| ~ element(sK363_skl,powerset(the_carrier(sK362_skl))) ),
inference(resolution,[status(thm)],[f4864,f2869]) ).
fof(f4877,definition,
( sQ192_spl
<=> interior(sK362_skl,sK363_skl) = sK363_skl ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f4878,plain,
( ~ sQ192_spl
| interior(sK362_skl,sK363_skl) = sK363_skl ),
inference(component_clause,[status(thm)],[f4877]) ).
fof(f4880,plain,
( ~ sQ32_spl
| sQ192_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f4871,f4160,f4877,f3673]) ).
fof(f4893,plain,
( ~ sQ192_spl
| ~ sQ64_spl
| ~ in(sK364_skl,sK363_skl)
| point_neighbourhood(sK363_skl,sK362_skl,sK364_skl)
| ~ element(sK363_skl,powerset(the_carrier(sK362_skl))) ),
inference(paramodulation,[status(thm)],[f4878,f4124]) ).
fof(f4900,definition,
( sQ195_spl
<=> point_neighbourhood(sK363_skl,sK362_skl,sK364_skl) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f4901,plain,
( ~ sQ195_spl
| point_neighbourhood(sK363_skl,sK362_skl,sK364_skl) ),
inference(component_clause,[status(thm)],[f4900]) ).
fof(f4903,plain,
( ~ sQ192_spl
| ~ sQ64_spl
| ~ sQ81_spl
| sQ195_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f4893,f4160,f4900,f4248,f4123,f4877]) ).
fof(f4909,plain,
( ~ sQ195_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4901,f2871]) ).
fof(f4910,plain,
~ sQ195_spl,
inference(contradiction_clause,[status(thm)],[f4909]) ).
fof(f4911,plain,
$false,
inference(sat_refutation,[status(thm)],[f3676,f4126,f4132,f4134,f4136,f4251,f4277,f4306,f4308,f4730,f4880,f4903,f4910]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU341+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n006.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 06:13:42 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.28/0.58 % Drodi V4.1.1
% 0.42/1.16 % Refutation found
% 0.42/1.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.42/1.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.42/1.23 % Elapsed time: 0.758372 seconds
% 0.42/1.23 % CPU time: 4.679932 seconds
% 0.42/1.23 % Total memory used: 217.941 MB
% 0.42/1.23 % Net memory used: 214.215 MB
%------------------------------------------------------------------------------