%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU337+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 : n019.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:12 PM UTC 2026
% Result : Theorem 0.19s 5.76s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 22
% Syntax : Number of formulae : 106 ( 7 unt; 14 def)
% Number of atoms : 318 ( 38 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 369 ( 157 ~; 155 |; 21 &)
% ( 20 <=>; 15 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 15 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 86 ( 81 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f66,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ( open_subsets(B,A)
<=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ( in(C,B)
=> open_subset(C,A) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(complements_of_subsets(A,B),powerset(powerset(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f260,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> complements_of_subsets(A,complements_of_subsets(A,B)) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f372,lemma,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ( ~ ( B = empty_set
& complements_of_subsets(A,B) != empty_set )
& ~ ( complements_of_subsets(A,B) = empty_set
& B != empty_set ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f404,lemma,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ( closed_subsets(B,A)
<=> open_subsets(complements_of_subsets(the_carrier(A),B),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f410,conjecture,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ( open_subsets(B,A)
<=> closed_subsets(complements_of_subsets(the_carrier(A),B),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f411,negated_conjecture,
~ ! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ( open_subsets(B,A)
<=> closed_subsets(complements_of_subsets(the_carrier(A),B),A) ) ) ),
inference(negated_conjecture,[status(cth)],[f410]) ).
fof(f493,lemma,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ~ ( complements_of_subsets(A,B) = empty_set
& B != empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f502,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f877,plain,
! [A] :
( ! [B] :
( ( open_subsets(B,A)
<=> ! [C] :
( open_subset(C,A)
| ~ in(C,B)
| ~ element(C,powerset(the_carrier(A))) ) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f66]) ).
fof(f878,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ~ open_subset(C,A)
& in(C,B)
& element(C,powerset(the_carrier(A))) )
| open_subsets(B,A) )
& ( ! [C] :
( open_subset(C,A)
| ~ in(C,B)
| ~ element(C,powerset(the_carrier(A))) )
| ~ open_subsets(B,A) ) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ top_str(A) ),
inference(NNF_transformation,[status(thm)],[f877]) ).
fof(f879,plain,
! [A] :
( ! [B] :
( ( ( ( ~ open_subset(sK37_skl(B,A),A)
& in(sK37_skl(B,A),B)
& element(sK37_skl(B,A),powerset(the_carrier(A))) )
| open_subsets(B,A) )
& ( ! [C] :
( open_subset(C,A)
| ~ in(C,B)
| ~ element(C,powerset(the_carrier(A))) )
| ~ open_subsets(B,A) ) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ top_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl]),skolemize(C,sK37_skl(B,A))],[f878]) ).
fof(f880,plain,
! [X0,X1,X2] :
( open_subset(X2,X0)
| ~ in(X2,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ open_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f879]) ).
fof(f1305,plain,
! [A,B] :
( element(complements_of_subsets(A,B),powerset(powerset(A)))
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f169]) ).
fof(f1306,plain,
! [X0,X1] :
( element(complements_of_subsets(X1,X0),powerset(powerset(X1)))
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f1305]) ).
fof(f1573,plain,
! [A,B] :
( complements_of_subsets(A,complements_of_subsets(A,B)) = B
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f260]) ).
fof(f1574,plain,
! [X0,X1] :
( complements_of_subsets(X1,complements_of_subsets(X1,X0)) = X0
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f1573]) ).
fof(f2304,plain,
! [A,B] :
( ( ( B != empty_set
| complements_of_subsets(A,B) = empty_set )
& ( complements_of_subsets(A,B) != empty_set
| B = empty_set ) )
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f372]) ).
fof(f2305,plain,
! [X0,X1] :
( complements_of_subsets(X1,X0) != empty_set
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f2304]) ).
fof(f2306,plain,
! [X0,X1] :
( X0 != empty_set
| complements_of_subsets(X1,X0) = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f2304]) ).
fof(f2411,plain,
! [A] :
( ! [B] :
( ( closed_subsets(B,A)
<=> open_subsets(complements_of_subsets(the_carrier(A),B),A) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f404]) ).
fof(f2412,plain,
! [A] :
( ! [B] :
( ( ( ~ open_subsets(complements_of_subsets(the_carrier(A),B),A)
| closed_subsets(B,A) )
& ( open_subsets(complements_of_subsets(the_carrier(A),B),A)
| ~ closed_subsets(B,A) ) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ top_str(A) ),
inference(NNF_transformation,[status(thm)],[f2411]) ).
fof(f2413,plain,
! [X0,X1] :
( open_subsets(complements_of_subsets(the_carrier(X0),X1),X0)
| ~ closed_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f2412]) ).
fof(f2414,plain,
! [X0,X1] :
( ~ open_subsets(complements_of_subsets(the_carrier(X0),X1),X0)
| closed_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f2412]) ).
fof(f2432,plain,
? [A] :
( ? [B] :
( ( open_subsets(B,A)
<~> closed_subsets(complements_of_subsets(the_carrier(A),B),A) )
& element(B,powerset(powerset(the_carrier(A)))) )
& top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f411]) ).
fof(f2433,plain,
? [A] :
( ? [B] :
( ( ~ closed_subsets(complements_of_subsets(the_carrier(A),B),A)
| ~ open_subsets(B,A) )
& ( closed_subsets(complements_of_subsets(the_carrier(A),B),A)
| open_subsets(B,A) )
& element(B,powerset(powerset(the_carrier(A)))) )
& top_str(A) ),
inference(NNF_transformation,[status(thm)],[f2432]) ).
fof(f2434,plain,
( ( ~ closed_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl)
| ~ open_subsets(sK330_skl,sK329_skl) )
& ( closed_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl)
| open_subsets(sK330_skl,sK329_skl) )
& element(sK330_skl,powerset(powerset(the_carrier(sK329_skl))))
& top_str(sK329_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK329_skl,sK330_skl]),skolemize(A,sK329_skl),skolemize(B,sK330_skl)],[f2433]) ).
fof(f2435,plain,
top_str(sK329_skl),
inference(cnf_transformation,[status(thm)],[f2434]) ).
fof(f2436,plain,
element(sK330_skl,powerset(powerset(the_carrier(sK329_skl)))),
inference(cnf_transformation,[status(thm)],[f2434]) ).
fof(f2437,plain,
( closed_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl)
| open_subsets(sK330_skl,sK329_skl) ),
inference(cnf_transformation,[status(thm)],[f2434]) ).
fof(f2438,plain,
( ~ closed_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl)
| ~ open_subsets(sK330_skl,sK329_skl) ),
inference(cnf_transformation,[status(thm)],[f2434]) ).
fof(f2708,plain,
! [A,B] :
( complements_of_subsets(A,B) != empty_set
| B = empty_set
| ~ element(B,powerset(powerset(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f493]) ).
fof(f2709,plain,
! [X0,X1] :
( complements_of_subsets(X1,X0) != empty_set
| X0 = empty_set
| ~ element(X0,powerset(powerset(X1))) ),
inference(cnf_transformation,[status(thm)],[f2708]) ).
fof(f2724,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f502]) ).
fof(f2725,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f2724]) ).
fof(f2726,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2725]) ).
fof(f3576,definition,
( sQ31_spl
<=> open_subsets(sK330_skl,sK329_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f3577,plain,
( ~ sQ31_spl
| open_subsets(sK330_skl,sK329_skl) ),
inference(component_clause,[status(thm)],[f3576]) ).
fof(f3579,definition,
( sQ32_spl
<=> closed_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f3580,plain,
( ~ sQ32_spl
| closed_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl) ),
inference(component_clause,[status(thm)],[f3579]) ).
fof(f3581,plain,
( sQ32_spl
| ~ closed_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl) ),
inference(component_clause,[status(thm)],[f3579]) ).
fof(f3582,plain,
( sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f2437,f3576,f3579]) ).
fof(f3583,plain,
( ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2438,f3576,f3579]) ).
fof(f3892,plain,
! [X0] :
( complements_of_subsets(X0,empty_set) = empty_set
| ~ element(empty_set,powerset(powerset(X0))) ),
inference(destructive_equality_resolution,[status(thm)],[f2306]) ).
fof(f4025,definition,
( sQ63_spl
<=> top_str(sK329_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f4027,plain,
( sQ63_spl
| ~ top_str(sK329_skl) ),
inference(component_clause,[status(thm)],[f4025]) ).
fof(f4028,definition,
( sQ64_spl
<=> element(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),powerset(powerset(the_carrier(sK329_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f4029,plain,
( ~ sQ64_spl
| element(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),powerset(powerset(the_carrier(sK329_skl)))) ),
inference(component_clause,[status(thm)],[f4028]) ).
fof(f4030,plain,
( sQ64_spl
| ~ element(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),powerset(powerset(the_carrier(sK329_skl)))) ),
inference(component_clause,[status(thm)],[f4028]) ).
fof(f4036,plain,
! [X0,X1,X2] :
( open_subset(X2,X0)
| ~ in(X2,X1)
| ~ open_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f880,f2726]) ).
fof(f4038,plain,
complements_of_subsets(the_carrier(sK329_skl),complements_of_subsets(the_carrier(sK329_skl),sK330_skl)) = sK330_skl,
inference(resolution,[status(thm)],[f1574,f2436]) ).
fof(f4041,plain,
( element(sK330_skl,powerset(powerset(the_carrier(sK329_skl))))
| ~ element(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),powerset(powerset(the_carrier(sK329_skl)))) ),
inference(paramodulation,[status(thm)],[f4038,f1306]) ).
fof(f4042,definition,
( sQ66_spl
<=> element(sK330_skl,powerset(powerset(the_carrier(sK329_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f4045,plain,
( sQ66_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f4041,f4028,f4042]) ).
fof(f4046,plain,
( sQ64_spl
| ~ element(sK330_skl,powerset(powerset(the_carrier(sK329_skl)))) ),
inference(resolution,[status(thm)],[f4030,f1306]) ).
fof(f4049,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4046,f2436]) ).
fof(f4050,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f4049]) ).
fof(f4051,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4027,f2435]) ).
fof(f4052,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f4051]) ).
fof(f4054,plain,
( complements_of_subsets(the_carrier(sK329_skl),sK330_skl) != empty_set
| sK330_skl = empty_set ),
inference(resolution,[status(thm)],[f2305,f2436]) ).
fof(f4057,definition,
( sQ67_spl
<=> sK330_skl = empty_set ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f4058,plain,
( ~ sQ67_spl
| sK330_skl = empty_set ),
inference(component_clause,[status(thm)],[f4057]) ).
fof(f4060,definition,
( sQ68_spl
<=> complements_of_subsets(the_carrier(sK329_skl),sK330_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f4063,plain,
( ~ sQ68_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f4054,f4057,f4060]) ).
fof(f4064,plain,
! [X0] :
( open_subsets(complements_of_subsets(the_carrier(sK329_skl),X0),sK329_skl)
| ~ closed_subsets(X0,sK329_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK329_skl)))) ),
inference(resolution,[status(thm)],[f2413,f2435]) ).
fof(f4067,plain,
! [X0] :
( ~ sQ67_spl
| complements_of_subsets(X0,empty_set) = sK330_skl
| ~ element(empty_set,powerset(powerset(X0))) ),
inference(backward_demodulation,[status(thm)],[f4058,f3892]) ).
fof(f4069,plain,
! [X0] :
( ~ sQ67_spl
| complements_of_subsets(X0,empty_set) = sK330_skl
| ~ element(sK330_skl,powerset(powerset(X0))) ),
inference(forward_demodulation,[status(thm)],[f4058,f4067]) ).
fof(f4070,plain,
! [X0] :
( ~ sQ67_spl
| complements_of_subsets(X0,sK330_skl) = sK330_skl
| ~ element(sK330_skl,powerset(powerset(X0))) ),
inference(forward_demodulation,[status(thm)],[f4058,f4069]) ).
fof(f4087,plain,
( ~ sQ64_spl
| complements_of_subsets(the_carrier(sK329_skl),complements_of_subsets(the_carrier(sK329_skl),sK330_skl)) != empty_set
| complements_of_subsets(the_carrier(sK329_skl),sK330_skl) = empty_set ),
inference(resolution,[status(thm)],[f4029,f2709]) ).
fof(f4089,definition,
( sQ71_spl
<=> complements_of_subsets(the_carrier(sK329_skl),complements_of_subsets(the_carrier(sK329_skl),sK330_skl)) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f4092,plain,
( ~ sQ64_spl
| ~ sQ71_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f4087,f4060,f4089,f4028]) ).
fof(f4094,plain,
( ~ sQ67_spl
| complements_of_subsets(the_carrier(sK329_skl),sK330_skl) = sK330_skl ),
inference(resolution,[status(thm)],[f4070,f2436]) ).
fof(f4110,definition,
( sQ72_spl
<=> complements_of_subsets(the_carrier(sK329_skl),complements_of_subsets(the_carrier(sK329_skl),sK330_skl)) = sK330_skl ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f4112,plain,
( sQ72_spl
| complements_of_subsets(the_carrier(sK329_skl),complements_of_subsets(the_carrier(sK329_skl),sK330_skl)) != sK330_skl ),
inference(component_clause,[status(thm)],[f4110]) ).
fof(f4115,plain,
( sQ72_spl
| sK330_skl != sK330_skl ),
inference(forward_demodulation,[status(thm)],[f4038,f4112]) ).
fof(f4116,plain,
( sQ72_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4115]) ).
fof(f4117,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f4116]) ).
fof(f4125,plain,
( ~ sQ32_spl
| ~ sQ67_spl
| closed_subsets(sK330_skl,sK329_skl) ),
inference(backward_demodulation,[status(thm)],[f4094,f3580]) ).
fof(f4147,plain,
! [X0,X1] :
( open_subset(X1,sK329_skl)
| ~ in(X1,complements_of_subsets(the_carrier(sK329_skl),X0))
| ~ element(complements_of_subsets(the_carrier(sK329_skl),X0),powerset(powerset(the_carrier(sK329_skl))))
| ~ top_str(sK329_skl)
| ~ closed_subsets(X0,sK329_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK329_skl)))) ),
inference(resolution,[status(thm)],[f4064,f4036]) ).
fof(f4148,plain,
( ~ sQ67_spl
| open_subsets(sK330_skl,sK329_skl)
| ~ closed_subsets(sK330_skl,sK329_skl)
| ~ element(sK330_skl,powerset(powerset(the_carrier(sK329_skl)))) ),
inference(paramodulation,[status(thm)],[f4094,f4064]) ).
fof(f4149,definition,
! [X0,X1] :
( sQ73_spl
<=> ( open_subset(X1,sK329_skl)
| ~ in(X1,complements_of_subsets(the_carrier(sK329_skl),X0))
| ~ element(complements_of_subsets(the_carrier(sK329_skl),X0),powerset(powerset(the_carrier(sK329_skl))))
| ~ closed_subsets(X0,sK329_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK329_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4152,plain,
( ~ sQ63_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f4147,f4149,f4025]) ).
fof(f4153,definition,
( sQ74_spl
<=> closed_subsets(sK330_skl,sK329_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f4155,plain,
( sQ74_spl
| ~ closed_subsets(sK330_skl,sK329_skl) ),
inference(component_clause,[status(thm)],[f4153]) ).
fof(f4156,plain,
( ~ sQ67_spl
| sQ31_spl
| ~ sQ74_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f4148,f4042,f4153,f3576,f4057]) ).
fof(f4159,plain,
( sQ74_spl
| ~ open_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl)
| ~ element(sK330_skl,powerset(powerset(the_carrier(sK329_skl))))
| ~ top_str(sK329_skl) ),
inference(resolution,[status(thm)],[f4155,f2414]) ).
fof(f4160,definition,
( sQ75_spl
<=> open_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f4162,plain,
( sQ75_spl
| ~ open_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl) ),
inference(component_clause,[status(thm)],[f4160]) ).
fof(f4163,plain,
( sQ74_spl
| ~ sQ75_spl
| ~ sQ66_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f4159,f4025,f4042,f4160,f4153]) ).
fof(f4164,plain,
( sQ75_spl
| ~ sQ67_spl
| ~ open_subsets(sK330_skl,sK329_skl) ),
inference(forward_demodulation,[status(thm)],[f4094,f4162]) ).
fof(f4165,plain,
! [X0] :
( ~ sQ31_spl
| open_subset(X0,sK329_skl)
| ~ in(X0,sK330_skl)
| ~ element(sK330_skl,powerset(powerset(the_carrier(sK329_skl))))
| ~ top_str(sK329_skl) ),
inference(resolution,[status(thm)],[f3577,f4036]) ).
fof(f4166,definition,
! [X0] :
( sQ76_spl
<=> ( open_subset(X0,sK329_skl)
| ~ in(X0,sK330_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f4169,plain,
( ~ sQ31_spl
| sQ76_spl
| ~ sQ66_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f4165,f4025,f4042,f4166,f3576]) ).
fof(f4173,plain,
( sQ74_spl
| ~ sQ32_spl
| ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4155,f4125]) ).
fof(f4174,plain,
( sQ74_spl
| ~ sQ32_spl
| ~ sQ67_spl ),
inference(contradiction_clause,[status(thm)],[f4173]) ).
fof(f4175,plain,
( sQ75_spl
| ~ sQ67_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f4164,f3576,f4057,f4160]) ).
fof(f4178,plain,
( sQ32_spl
| ~ open_subsets(complements_of_subsets(the_carrier(sK329_skl),complements_of_subsets(the_carrier(sK329_skl),sK330_skl)),sK329_skl)
| ~ element(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),powerset(powerset(the_carrier(sK329_skl))))
| ~ top_str(sK329_skl) ),
inference(resolution,[status(thm)],[f3581,f2414]) ).
fof(f4179,definition,
( sQ77_spl
<=> open_subsets(complements_of_subsets(the_carrier(sK329_skl),complements_of_subsets(the_carrier(sK329_skl),sK330_skl)),sK329_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f4181,plain,
( sQ77_spl
| ~ open_subsets(complements_of_subsets(the_carrier(sK329_skl),complements_of_subsets(the_carrier(sK329_skl),sK330_skl)),sK329_skl) ),
inference(component_clause,[status(thm)],[f4179]) ).
fof(f4182,plain,
( sQ32_spl
| ~ sQ77_spl
| ~ sQ64_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f4178,f4025,f4028,f4179,f3579]) ).
fof(f4190,plain,
( open_subsets(sK330_skl,sK329_skl)
| ~ closed_subsets(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),sK329_skl)
| ~ element(complements_of_subsets(the_carrier(sK329_skl),sK330_skl),powerset(powerset(the_carrier(sK329_skl)))) ),
inference(paramodulation,[status(thm)],[f4038,f4064]) ).
fof(f4192,plain,
( sQ31_spl
| ~ sQ32_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f4190,f4028,f3579,f3576]) ).
fof(f4198,plain,
( sQ77_spl
| ~ open_subsets(sK330_skl,sK329_skl) ),
inference(forward_demodulation,[status(thm)],[f4038,f4181]) ).
fof(f4199,plain,
( sQ77_spl
| ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4198,f3577]) ).
fof(f4200,plain,
( sQ77_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f4199]) ).
fof(f4201,plain,
$false,
inference(sat_refutation,[status(thm)],[f3582,f3583,f4045,f4050,f4052,f4063,f4092,f4117,f4152,f4156,f4163,f4169,f4174,f4175,f4182,f4192,f4200]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU337+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.56 % Computer : n019.cluster.edu
% 0.14/5.56 % Model : x86_64 x86_64
% 0.14/5.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.56 % Memory : 8046.5625MB
% 0.14/5.56 % OS : Linux 6.8.0-71-generic
% 0.14/5.56 % CPULimit : 300
% 0.14/5.56 % WCLimit : 300
% 0.14/5.56 % DateTime : Mon Sep 21 06:13:44 UTC 2026
% 0.14/5.56 % CPUTime :
% 0.19/5.67 % Drodi V4.1.1
% 0.19/5.76 % Refutation found
% 0.19/5.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/5.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/5.80 % Elapsed time: 0.223069 seconds
% 0.19/5.80 % CPU time: 0.737964 seconds
% 0.19/5.80 % Total memory used: 189.728 MB
% 0.19/5.80 % Net memory used: 188.701 MB
%------------------------------------------------------------------------------