%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU337+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n004.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 : Fri Sep 25 02:51:46 PM UTC 2026
% Result : Theorem 54.83s 8.81s
% Output : Proof 54.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 9
% Syntax : Number of formulae : 102 ( 8 unt; 0 def)
% Number of atoms : 374 ( 14 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 441 ( 169 ~; 208 |; 34 &)
% ( 8 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-3 aty)
% Number of variables : 128 ( 0 sgn 64 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ! [C] :
( element(C,powerset(powerset(A)))
=> ( C = complements_of_subsets(A,B)
<=> ! [D] :
( element(D,powerset(A))
=> ( in(D,C)
<=> in(subset_complement(A,D),B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_setfam_1) ).
fof(f18_nnf,plain,
! [A,B] :
( ! [C] :
( ( ( ? [D] :
( ( ( in(subset_complement(A,D),B)
& ~ in(D,C) )
| ( ~ in(subset_complement(A,D),B)
& in(D,C) ) )
& element(D,powerset(A)) )
| C = complements_of_subsets(A,B) )
& ( ! [D] :
( ( ( ~ in(subset_complement(A,D),B)
| in(D,C) )
& ( in(subset_complement(A,D),B)
| ~ in(D,C) ) )
| ~ element(D,powerset(A)) )
| C != complements_of_subsets(A,B) ) )
| ~ element(C,powerset(powerset(A))) )
| ~ element(B,powerset(powerset(A))) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [B,A,C,D] :
( ( ( ( ( ( in(subset_complement(A,sk2(A,B,C)),B)
& ~ in(sk2(A,B,C),C) )
| ( ~ in(subset_complement(A,sk2(A,B,C)),B)
& in(sk2(A,B,C),C) ) )
& element(sk2(A,B,C),powerset(A)) )
| C = complements_of_subsets(A,B) )
& ( ( ( ~ in(subset_complement(A,D),B)
| in(D,C) )
& ( in(subset_complement(A,D),B)
| ~ in(D,C) ) )
| ~ element(D,powerset(A))
| C != complements_of_subsets(A,B) ) )
| ~ element(C,powerset(powerset(A)))
| ~ element(B,powerset(powerset(A))) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f18_nnf]) ).
cnf(c48,plain,
( in(subset_complement(X0,X3),X1)
| ~ in(X3,X2)
| ~ element(X3,powerset(X0))
| X2 != complements_of_subsets(X0,X1)
| ~ element(X2,powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p275,plain,
( in(subset_complement(X1,X2),X0)
| ~ in(X2,complements_of_subsets(X1,X0))
| ~ element(X2,powerset(X1))
| ~ element(complements_of_subsets(X1,X0),powerset(powerset(X1)))
| ~ element(X0,powerset(powerset(X1))) ),
inference(equality_resolution,[status(thm)],[c48]) ).
fof(f38,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',t17_tops_2) ).
fof(f38_neg,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)],[f38]) ).
fof(f38_nnf,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)],[f38_neg]) ).
fof(f38_sk,plain,
( ( ( closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
& ~ open_subsets(sk10,sk9) )
| ( ~ closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
& open_subsets(sk10,sk9) ) )
& element(sk10,powerset(powerset(the_carrier(sk9))))
& top_str(sk9) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9,sk10])],[f38_nnf]) ).
cnf(c87,plain,
element(sk10,powerset(powerset(the_carrier(sk9)))),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p1068,plain,
( in(subset_complement(the_carrier(sk9),X0),sk10)
| ~ in(X0,complements_of_subsets(the_carrier(sk9),sk10))
| ~ element(X0,powerset(the_carrier(sk9)))
| ~ element(complements_of_subsets(the_carrier(sk9),sk10),powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[p275,c87]) ).
fof(f22,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(complements_of_subsets(A,B),powerset(powerset(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_setfam_1) ).
fof(f22_nnf,plain,
! [A,B] :
( element(complements_of_subsets(A,B),powerset(powerset(A)))
| ~ element(B,powerset(powerset(A))) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [B,A] :
( element(complements_of_subsets(A,B),powerset(powerset(A)))
| ~ element(B,powerset(powerset(A))) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c58,plain,
( element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p361,plain,
element(complements_of_subsets(the_carrier(sk9),sk10),powerset(powerset(the_carrier(sk9)))),
inference(resolution,[status(thm)],[c58,c87]) ).
cnf(p6099,plain,
( in(subset_complement(the_carrier(sk9),X0),sk10)
| ~ in(X0,complements_of_subsets(the_carrier(sk9),sk10))
| ~ element(X0,powerset(the_carrier(sk9))) ),
inference(resolution,[status(thm)],[p1068,p361]) ).
fof(f17,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ( closed_subsets(B,A)
<=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ( in(C,B)
=> closed_subset(C,A) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_tops_2) ).
fof(f17_nnf,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ~ closed_subset(C,A)
& in(C,B)
& element(C,powerset(the_carrier(A))) )
| closed_subsets(B,A) )
& ( ! [C] :
( closed_subset(C,A)
| ~ in(C,B)
| ~ element(C,powerset(the_carrier(A))) )
| ~ closed_subsets(B,A) ) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A,B,C] :
( ( ( ( ~ closed_subset(sk1(A,B),A)
& in(sk1(A,B),B)
& element(sk1(A,B),powerset(the_carrier(A))) )
| closed_subsets(B,A) )
& ( closed_subset(C,A)
| ~ in(C,B)
| ~ element(C,powerset(the_carrier(A)))
| ~ closed_subsets(B,A) ) )
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f17_nnf]) ).
cnf(c45,plain,
( element(sk1(X0,X1),powerset(the_carrier(X0)))
| closed_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(c86,plain,
top_str(sk9),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p255,plain,
( element(sk1(sk9,X0),powerset(the_carrier(sk9)))
| closed_subsets(X0,sk9)
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[c45,c86]) ).
cnf(p377,plain,
( element(sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10)),powerset(the_carrier(sk9)))
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p361,p255]) ).
cnf(p6131,plain,
( closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| in(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),sk10)
| ~ in(sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10)),complements_of_subsets(the_carrier(sk9),sk10)) ),
inference(resolution,[status(thm)],[p6099,p377]) ).
cnf(c46,plain,
( in(sk1(X0,X1),X1)
| closed_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p258,plain,
( in(sk1(sk9,X0),X0)
| closed_subsets(X0,sk9)
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[c46,c86]) ).
cnf(p372,plain,
( in(sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10)),complements_of_subsets(the_carrier(sk9),sk10))
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p361,p258]) ).
cnf(p7789,plain,
( closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| in(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),sk10) ),
inference(resolution,[status(thm)],[p6131,p372]) ).
cnf(p7790,plain,
( closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| in(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),sk10) ),
inference(factoring,[status(thm)],[p7789]) ).
cnf(c44,plain,
( closed_subset(X2,X0)
| ~ in(X2,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ closed_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p247,plain,
( closed_subset(X1,sk9)
| ~ in(X1,X0)
| ~ element(X1,powerset(the_carrier(sk9)))
| ~ closed_subsets(X0,sk9)
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[c44,c86]) ).
cnf(p929,plain,
( closed_subset(X0,sk9)
| ~ in(X0,complements_of_subsets(the_carrier(sk9),sk10))
| ~ element(X0,powerset(the_carrier(sk9)))
| ~ closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p247,p361]) ).
cnf(c89,plain,
( closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| open_subsets(sk10,sk9) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p1685,plain,
( open_subsets(sk10,sk9)
| closed_subset(X0,sk9)
| ~ in(X0,complements_of_subsets(the_carrier(sk9),sk10))
| ~ element(X0,powerset(the_carrier(sk9))) ),
inference(resolution,[status(thm)],[p929,c89]) ).
fof(f21,axiom,
! [A,B] :
( element(B,powerset(A))
=> element(subset_complement(A,B),powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f21_nnf,plain,
! [A,B] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [B,A] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c57,plain,
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
fof(f16,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',d1_tops_2) ).
fof(f16_nnf,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)],[f16]) ).
fof(f16_sk,plain,
! [A,B,C] :
( ( ( ( ~ open_subset(sk0(A,B),A)
& in(sk0(A,B),B)
& element(sk0(A,B),powerset(the_carrier(A))) )
| open_subsets(B,A) )
& ( 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(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f16_nnf]) ).
cnf(c41,plain,
( element(sk0(X0,X1),powerset(the_carrier(X0)))
| open_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p221,plain,
( element(sk0(sk9,X0),powerset(the_carrier(sk9)))
| open_subsets(X0,sk9)
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[c41,c86]) ).
cnf(p223,plain,
( element(sk0(sk9,sk10),powerset(the_carrier(sk9)))
| open_subsets(sk10,sk9) ),
inference(resolution,[status(thm)],[p221,c87]) ).
cnf(p338,plain,
( open_subsets(sk10,sk9)
| element(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),powerset(the_carrier(sk9))) ),
inference(resolution,[status(thm)],[c57,p223]) ).
cnf(p1711,plain,
( open_subsets(sk10,sk9)
| open_subsets(sk10,sk9)
| closed_subset(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),sk9)
| ~ in(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),complements_of_subsets(the_carrier(sk9),sk10)) ),
inference(resolution,[status(thm)],[p1685,p338]) ).
cnf(p5313,plain,
( open_subsets(sk10,sk9)
| closed_subset(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),sk9)
| ~ in(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),complements_of_subsets(the_carrier(sk9),sk10)) ),
inference(factoring,[status(thm)],[p1711]) ).
fof(f33,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',involutiveness_k7_setfam_1) ).
fof(f33_nnf,plain,
! [A,B] :
( complements_of_subsets(A,complements_of_subsets(A,B)) = B
| ~ element(B,powerset(powerset(A))) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [B,A] :
( complements_of_subsets(A,complements_of_subsets(A,B)) = B
| ~ element(B,powerset(powerset(A))) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c74,plain,
( complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p428,plain,
complements_of_subsets(the_carrier(sk9),complements_of_subsets(the_carrier(sk9),sk10)) = sk10,
inference(resolution,[status(thm)],[c74,c87]) ).
cnf(p373,plain,
( in(subset_complement(the_carrier(sk9),X1),complements_of_subsets(the_carrier(sk9),sk10))
| ~ in(X1,X0)
| ~ element(X1,powerset(the_carrier(sk9)))
| X0 != complements_of_subsets(the_carrier(sk9),complements_of_subsets(the_carrier(sk9),sk10))
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[p361,c48]) ).
cnf(p429,plain,
( in(subset_complement(the_carrier(sk9),X1),complements_of_subsets(the_carrier(sk9),sk10))
| ~ in(X1,X0)
| ~ element(X1,powerset(the_carrier(sk9)))
| X0 != sk10
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(demodulation,[status(thm)],[p428,p373]) ).
cnf(p2840,plain,
( in(subset_complement(the_carrier(sk9),X0),complements_of_subsets(the_carrier(sk9),sk10))
| ~ in(X0,sk10)
| ~ element(X0,powerset(the_carrier(sk9)))
| sk10 != sk10 ),
inference(resolution,[status(thm)],[p429,c87]) ).
cnf(p2862,plain,
( in(subset_complement(the_carrier(sk9),X0),complements_of_subsets(the_carrier(sk9),sk10))
| ~ in(X0,sk10)
| ~ element(X0,powerset(the_carrier(sk9))) ),
inference(equality_resolution,[status(thm)],[p2840]) ).
cnf(p2867,plain,
( open_subsets(sk10,sk9)
| in(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),complements_of_subsets(the_carrier(sk9),sk10))
| ~ in(sk0(sk9,sk10),sk10) ),
inference(resolution,[status(thm)],[p2862,p223]) ).
cnf(c42,plain,
( in(sk0(X0,X1),X1)
| open_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p230,plain,
( in(sk0(sk9,X0),X0)
| open_subsets(X0,sk9)
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[c42,c86]) ).
cnf(p233,plain,
( in(sk0(sk9,sk10),sk10)
| open_subsets(sk10,sk9) ),
inference(resolution,[status(thm)],[p230,c87]) ).
cnf(p2984,plain,
( open_subsets(sk10,sk9)
| open_subsets(sk10,sk9)
| in(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),complements_of_subsets(the_carrier(sk9),sk10)) ),
inference(resolution,[status(thm)],[p2867,p233]) ).
cnf(p2985,plain,
( open_subsets(sk10,sk9)
| in(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),complements_of_subsets(the_carrier(sk9),sk10)) ),
inference(factoring,[status(thm)],[p2984]) ).
cnf(p5314,plain,
( open_subsets(sk10,sk9)
| open_subsets(sk10,sk9)
| closed_subset(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),sk9) ),
inference(resolution,[status(thm)],[p5313,p2985]) ).
cnf(p5315,plain,
( open_subsets(sk10,sk9)
| closed_subset(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),sk9) ),
inference(factoring,[status(thm)],[p5314]) ).
fof(f42,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( open_subset(B,A)
<=> closed_subset(subset_complement(the_carrier(A),B),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_tops_1) ).
fof(f42_nnf,plain,
! [A] :
( ! [B] :
( ( ( ~ closed_subset(subset_complement(the_carrier(A),B),A)
| open_subset(B,A) )
& ( closed_subset(subset_complement(the_carrier(A),B),A)
| ~ open_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [A,B] :
( ( ( ~ closed_subset(subset_complement(the_carrier(A),B),A)
| open_subset(B,A) )
& ( closed_subset(subset_complement(the_carrier(A),B),A)
| ~ open_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c97,plain,
( ~ closed_subset(subset_complement(the_carrier(X0),X1),X0)
| open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p529,plain,
( ~ closed_subset(subset_complement(the_carrier(sk9),X0),sk9)
| open_subset(X0,sk9)
| ~ element(X0,powerset(the_carrier(sk9))) ),
inference(resolution,[status(thm)],[c97,c86]) ).
cnf(p569,plain,
( open_subsets(sk10,sk9)
| ~ closed_subset(subset_complement(the_carrier(sk9),sk0(sk9,sk10)),sk9)
| open_subset(sk0(sk9,sk10),sk9) ),
inference(resolution,[status(thm)],[p529,p223]) ).
cnf(p5316,plain,
( open_subsets(sk10,sk9)
| open_subset(sk0(sk9,sk10),sk9)
| open_subsets(sk10,sk9) ),
inference(resolution,[status(thm)],[p5315,p569]) ).
cnf(p5319,plain,
( open_subset(sk0(sk9,sk10),sk9)
| open_subsets(sk10,sk9) ),
inference(factoring,[status(thm)],[p5316]) ).
cnf(c43,plain,
( ~ open_subset(sk0(X0,X1),X0)
| open_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p238,plain,
( ~ open_subset(sk0(sk9,X0),sk9)
| open_subsets(X0,sk9)
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[c43,c86]) ).
cnf(p260,plain,
( ~ open_subset(sk0(sk9,sk10),sk9)
| open_subsets(sk10,sk9) ),
inference(resolution,[status(thm)],[p238,c87]) ).
cnf(p5320,plain,
( open_subsets(sk10,sk9)
| open_subsets(sk10,sk9) ),
inference(resolution,[status(thm)],[p5319,p260]) ).
cnf(p5321,plain,
open_subsets(sk10,sk9),
inference(factoring,[status(thm)],[p5320]) ).
cnf(c40,plain,
( 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(esa)],[f16_sk]) ).
cnf(p214,plain,
( open_subset(X1,sk9)
| ~ in(X1,X0)
| ~ element(X1,powerset(the_carrier(sk9)))
| ~ open_subsets(X0,sk9)
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[c40,c86]) ).
cnf(p216,plain,
( open_subset(X0,sk9)
| ~ in(X0,sk10)
| ~ element(X0,powerset(the_carrier(sk9)))
| ~ open_subsets(sk10,sk9) ),
inference(resolution,[status(thm)],[p214,c87]) ).
cnf(p5322,plain,
( open_subset(X0,sk9)
| ~ in(X0,sk10)
| ~ element(X0,powerset(the_carrier(sk9))) ),
inference(resolution,[status(thm)],[p5321,p216]) ).
cnf(p602,plain,
( element(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),powerset(the_carrier(sk9)))
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p377,c57]) ).
cnf(p5347,plain,
( closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| open_subset(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),sk9)
| ~ in(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),sk10) ),
inference(resolution,[status(thm)],[p5322,p602]) ).
cnf(p7796,plain,
( closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| open_subset(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p7790,p5347]) ).
cnf(p7803,plain,
( open_subset(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(factoring,[status(thm)],[p7796]) ).
fof(f40,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( closed_subset(B,A)
<=> open_subset(subset_complement(the_carrier(A),B),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_tops_1) ).
fof(f40_nnf,plain,
! [A] :
( ! [B] :
( ( ( ~ open_subset(subset_complement(the_carrier(A),B),A)
| closed_subset(B,A) )
& ( open_subset(subset_complement(the_carrier(A),B),A)
| ~ closed_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [A,B] :
( ( ( ~ open_subset(subset_complement(the_carrier(A),B),A)
| closed_subset(B,A) )
& ( open_subset(subset_complement(the_carrier(A),B),A)
| ~ closed_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c94,plain,
( ~ open_subset(subset_complement(the_carrier(X0),X1),X0)
| closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p469,plain,
( ~ open_subset(subset_complement(the_carrier(sk9),X0),sk9)
| closed_subset(X0,sk9)
| ~ element(X0,powerset(the_carrier(sk9))) ),
inference(resolution,[status(thm)],[c94,c86]) ).
cnf(p605,plain,
( ~ open_subset(subset_complement(the_carrier(sk9),sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10))),sk9)
| closed_subset(sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10)),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p377,p469]) ).
cnf(p7804,plain,
( closed_subset(sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10)),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p7803,p605]) ).
cnf(p7806,plain,
( closed_subset(sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10)),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(factoring,[status(thm)],[p7804]) ).
cnf(c47,plain,
( ~ closed_subset(sk1(X0,X1),X0)
| closed_subsets(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p264,plain,
( ~ closed_subset(sk1(sk9,X0),sk9)
| closed_subsets(X0,sk9)
| ~ element(X0,powerset(powerset(the_carrier(sk9)))) ),
inference(resolution,[status(thm)],[c47,c86]) ).
cnf(p376,plain,
( ~ closed_subset(sk1(sk9,complements_of_subsets(the_carrier(sk9),sk10)),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p361,p264]) ).
cnf(p7807,plain,
( closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9)
| closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(resolution,[status(thm)],[p7806,p376]) ).
cnf(p7808,plain,
closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9),
inference(factoring,[status(thm)],[p7807]) ).
cnf(c90,plain,
( ~ open_subsets(sk10,sk9)
| ~ closed_subsets(complements_of_subsets(the_carrier(sk9),sk10),sk9) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p7809,plain,
~ open_subsets(sk10,sk9),
inference(resolution,[status(thm)],[p7808,c90]) ).
cnf(p7811,plain,
$false,
inference(resolution,[status(thm)],[p7809,p5321]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU337+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.38 % Computer : n004.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Thu Sep 24 13:45:06 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 54.83/8.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 54.83/8.81 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------