%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU341+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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.10s 0.40s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 15
% Syntax : Number of formulae : 69 ( 17 unt; 12 def)
% Number of atoms : 218 ( 10 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 248 ( 99 ~; 92 |; 26 &)
% ( 14 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 13 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 47 ( 44 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,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/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [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/sandbox/benchmark/theBenchmark.p') ).
fof(f41,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/sandbox/benchmark/theBenchmark.p') ).
fof(f42,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)],[f41]) ).
fof(f103,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)],[f17]) ).
fof(f104,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)],[f103]) ).
fof(f106,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)],[f104]) ).
fof(f156,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)],[f40]) ).
fof(f157,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)],[f156]) ).
fof(f159,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)],[f42]) ).
fof(f160,plain,
( ~ point_neighbourhood(sK8_skl,sK7_skl,sK9_skl)
& in(sK9_skl,sK8_skl)
& open_subset(sK8_skl,sK7_skl)
& element(sK9_skl,the_carrier(sK7_skl))
& element(sK8_skl,powerset(the_carrier(sK7_skl)))
& top_str(sK7_skl)
& topological_space(sK7_skl)
& ~ empty_carrier(sK7_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl]),skolemize(A,sK7_skl),skolemize(B,sK8_skl),skolemize(C,sK9_skl)],[f159]) ).
fof(f161,plain,
~ empty_carrier(sK7_skl),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f162,plain,
topological_space(sK7_skl),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f163,plain,
top_str(sK7_skl),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f164,plain,
element(sK8_skl,powerset(the_carrier(sK7_skl))),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f165,plain,
element(sK9_skl,the_carrier(sK7_skl)),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f166,plain,
open_subset(sK8_skl,sK7_skl),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f167,plain,
in(sK9_skl,sK8_skl),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f168,plain,
~ point_neighbourhood(sK8_skl,sK7_skl,sK9_skl),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f180,definition,
! [X0,X2] :
( sQ0_spl
<=> ( ~ element(X2,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f181,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(component_clause,[status(thm)],[f180]) ).
fof(f183,definition,
! [X1,X3] :
( sQ1_spl
<=> ( interior(X1,X3) = X3
| ~ open_subset(X3,X1)
| ~ element(X3,powerset(the_carrier(X1)))
| ~ top_str(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f184,plain,
! [X0,X1] :
( ~ sQ1_spl
| interior(X0,X1) = X1
| ~ open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(component_clause,[status(thm)],[f183]) ).
fof(f186,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f157,f180,f183]) ).
fof(f197,plain,
! [X0] :
( ~ in(sK9_skl,interior(sK7_skl,X0))
| point_neighbourhood(X0,sK7_skl,sK9_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl)
| ~ topological_space(sK7_skl)
| empty_carrier(sK7_skl) ),
inference(resolution,[status(thm)],[f165,f106]) ).
fof(f198,definition,
( sQ4_spl
<=> empty_carrier(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( ~ sQ4_spl
| empty_carrier(sK7_skl) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,definition,
( sQ5_spl
<=> topological_space(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f203,plain,
( sQ5_spl
| ~ topological_space(sK7_skl) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,definition,
( sQ6_spl
<=> top_str(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f206,plain,
( sQ6_spl
| ~ top_str(sK7_skl) ),
inference(component_clause,[status(thm)],[f204]) ).
fof(f211,definition,
! [X0] :
( sQ8_spl
<=> ( ~ in(sK9_skl,interior(sK7_skl,X0))
| point_neighbourhood(X0,sK7_skl,sK9_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f212,plain,
! [X0] :
( ~ sQ8_spl
| ~ in(sK9_skl,interior(sK7_skl,X0))
| point_neighbourhood(X0,sK7_skl,sK9_skl)
| ~ element(X0,powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f214,plain,
( sQ8_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f197,f198,f201,f204,f211]) ).
fof(f215,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f206,f163]) ).
fof(f216,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f215]) ).
fof(f217,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f203,f162]) ).
fof(f218,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f217]) ).
fof(f219,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f199,f161]) ).
fof(f220,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f219]) ).
fof(f236,plain,
! [X0] :
( ~ sQ0_spl
| ~ element(X0,powerset(the_carrier(sK7_skl)))
| ~ top_str(sK7_skl) ),
inference(resolution,[status(thm)],[f181,f162]) ).
fof(f237,definition,
! [X0] :
( sQ11_spl
<=> ~ element(X0,powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f238,plain,
! [X0] :
( ~ sQ11_spl
| ~ element(X0,powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f237]) ).
fof(f240,plain,
( ~ sQ0_spl
| sQ11_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f236,f204,f237,f180]) ).
fof(f250,plain,
( ~ sQ11_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f164,f238]) ).
fof(f251,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f250]) ).
fof(f255,plain,
( ~ sQ1_spl
| interior(sK7_skl,sK8_skl) = sK8_skl
| ~ open_subset(sK8_skl,sK7_skl)
| ~ top_str(sK7_skl) ),
inference(resolution,[status(thm)],[f164,f184]) ).
fof(f262,definition,
( sQ13_spl
<=> interior(sK7_skl,sK8_skl) = sK8_skl ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( ~ sQ13_spl
| interior(sK7_skl,sK8_skl) = sK8_skl ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f265,definition,
( sQ14_spl
<=> open_subset(sK8_skl,sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f267,plain,
( sQ14_spl
| ~ open_subset(sK8_skl,sK7_skl) ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f269,plain,
( ~ sQ1_spl
| sQ13_spl
| ~ sQ14_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f255,f204,f265,f262,f183]) ).
fof(f271,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f267,f166]) ).
fof(f272,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f271]) ).
fof(f273,plain,
( ~ sQ13_spl
| ~ sQ8_spl
| ~ in(sK9_skl,sK8_skl)
| point_neighbourhood(sK8_skl,sK7_skl,sK9_skl)
| ~ element(sK8_skl,powerset(the_carrier(sK7_skl))) ),
inference(paramodulation,[status(thm)],[f263,f212]) ).
fof(f274,definition,
( sQ15_spl
<=> element(sK8_skl,powerset(the_carrier(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f276,plain,
( sQ15_spl
| ~ element(sK8_skl,powerset(the_carrier(sK7_skl))) ),
inference(component_clause,[status(thm)],[f274]) ).
fof(f277,definition,
( sQ16_spl
<=> point_neighbourhood(sK8_skl,sK7_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( ~ sQ16_spl
| point_neighbourhood(sK8_skl,sK7_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f280,definition,
( sQ17_spl
<=> in(sK9_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f282,plain,
( sQ17_spl
| ~ in(sK9_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f280]) ).
fof(f283,plain,
( ~ sQ13_spl
| ~ sQ8_spl
| ~ sQ17_spl
| sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f273,f274,f277,f280,f211,f262]) ).
fof(f284,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f282,f167]) ).
fof(f285,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f284]) ).
fof(f286,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f276,f164]) ).
fof(f287,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f286]) ).
fof(f288,plain,
( ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f278,f168]) ).
fof(f289,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f288]) ).
fof(f290,plain,
$false,
inference(sat_refutation,[status(thm)],[f186,f214,f216,f218,f220,f240,f251,f269,f272,f283,f285,f287,f289]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU341+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n008.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 06:14:39 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.40 % Refutation found
% 0.10/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.44 % Elapsed time: 0.061689 seconds
% 0.10/0.44 % CPU time: 0.165303 seconds
% 0.10/0.44 % Total memory used: 83.161 MB
% 0.10/0.44 % Net memory used: 83.114 MB
%------------------------------------------------------------------------------