%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU323+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:43 PM UTC 2026
% Result : Theorem 33.82s 4.85s
% Output : Proof 33.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 7
% Syntax : Number of formulae : 77 ( 53 unt; 0 def)
% Number of atoms : 137 ( 52 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 102 ( 42 ~; 36 |; 14 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-4 aty)
% Number of variables : 70 ( 2 sgn 34 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& closed_subset(B,A)
& top_str(A)
& topological_space(A) )
=> open_subset(subset_complement(the_carrier(A),B),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_tops_1) ).
fof(f0_nnf,plain,
! [A,B] :
( open_subset(subset_complement(the_carrier(A),B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ closed_subset(B,A)
| ~ top_str(A)
| ~ topological_space(A) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( open_subset(subset_complement(the_carrier(A),B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ closed_subset(B,A)
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( open_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ closed_subset(X1,X0)
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t253,plain,
ifeq(topological_space(X1),true,ifeq(top_str(X1),true,ifeq(closed_subset(X2,X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,open_subset(subset_complement(the_carrier(X1),X2),X1),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t1249,plain,
ifeq(topological_space(X1),true,ifeq(top_str(X1),true,ifeq(closed_subset(X2,X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,open_subset(subset_complement(the_carrier(X1),X2),X1),true),true),true),true) = true,
inference(orient,[status(thm)],[t253]) ).
fof(f6,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A) )
=> element(topstr_closure(A,B),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_pre_topc) ).
fof(f6_nnf,plain,
! [A,B] :
( element(topstr_closure(A,B),powerset(the_carrier(A)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B] :
( element(topstr_closure(A,B),powerset(the_carrier(A)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c7,plain,
( element(topstr_closure(X0,X1),powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t196,plain,
ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,element(topstr_closure(X1,X2),powerset(the_carrier(X1))),true),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t975,plain,
ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,element(topstr_closure(X1,X2),powerset(the_carrier(X1))),true),true) = true,
inference(orient,[status(thm)],[t196]) ).
fof(f5,axiom,
! [A,B] :
( element(B,powerset(A))
=> element(subset_complement(A,B),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f5_nnf,plain,
! [A,B] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [B,A] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c6,plain,
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t131,plain,
ifeq(element(X1,powerset(X2)),true,element(subset_complement(X2,X1),powerset(X2)),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t815,plain,
ifeq(element(X1,powerset(X2)),true,element(subset_complement(X2,X1),powerset(X2)),true) = true,
inference(orient,[status(thm)],[t131]) ).
fof(f20,conjecture,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> open_subset(interior(A,B),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_tops_1) ).
fof(f20_neg,negated_conjecture,
~ ! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> open_subset(interior(A,B),A) ) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f20_nnf,plain,
? [A] :
( ? [B] :
( ~ open_subset(interior(A,B),A)
& element(B,powerset(the_carrier(A))) )
& top_str(A)
& topological_space(A) ),
inference(nnf_transformation,[status(thm)],[f20_neg]) ).
fof(f20_sk,plain,
( ~ open_subset(interior(sk5,sk6),sk5)
& element(sk6,powerset(the_carrier(sk5)))
& top_str(sk5)
& topological_space(sk5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5,sk6])],[f20_nnf]) ).
cnf(c25,plain,
element(sk6,powerset(the_carrier(sk5))),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t8,plain,
element(sk6,powerset(the_carrier(sk5))) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t694,plain,
element(sk6,powerset(the_carrier(sk5))) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t817,plain,
true = ifeq(true,true,element(subset_complement(the_carrier(sk5),sk6),powerset(the_carrier(sk5))),true),
inference(cp,[status(thm)],[t815,t694]) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t1754,plain,
true = element(subset_complement(the_carrier(sk5),sk6),powerset(the_carrier(sk5))),
inference(step,[status(thm)],[t817,t256]) ).
cnf(t1548,plain,
element(subset_complement(the_carrier(sk5),sk6),powerset(the_carrier(sk5))) = true,
inference(orient,[status(thm)],[t1754]) ).
cnf(t1551,plain,
true = ifeq(top_str(sk5),true,ifeq(true,true,element(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),powerset(the_carrier(sk5))),true),true),
inference(cp,[status(thm)],[t975,t1548]) ).
cnf(c24,plain,
top_str(sk5),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t4,plain,
top_str(sk5) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t1421,plain,
top_str(sk5) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t1843,plain,
true = ifeq(true,true,ifeq(true,true,element(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),powerset(the_carrier(sk5))),true),true),
inference(step,[status(thm)],[t1551,t1421]) ).
cnf(t1844,plain,
true = ifeq(true,true,element(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),powerset(the_carrier(sk5))),true),
inference(step,[status(thm)],[t1843,t256]) ).
cnf(t1845,plain,
true = element(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),powerset(the_carrier(sk5))),
inference(step,[status(thm)],[t1844,t256]) ).
cnf(t1675,plain,
element(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),powerset(the_carrier(sk5))) = true,
inference(orient,[status(thm)],[t1845]) ).
cnf(t1682,plain,
true = ifeq(topological_space(sk5),true,ifeq(top_str(sk5),true,ifeq(closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true,ifeq(true,true,open_subset(subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))),sk5),true),true),true),true),
inference(cp,[status(thm)],[t1249,t1675]) ).
cnf(c23,plain,
topological_space(sk5),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t5,plain,
topological_space(sk5) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t1445,plain,
topological_space(sk5) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t1846,plain,
true = ifeq(true,true,ifeq(top_str(sk5),true,ifeq(closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true,ifeq(true,true,open_subset(subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))),sk5),true),true),true),true),
inference(step,[status(thm)],[t1682,t1445]) ).
cnf(t1847,plain,
true = ifeq(top_str(sk5),true,ifeq(closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true,ifeq(true,true,open_subset(subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))),sk5),true),true),true),
inference(step,[status(thm)],[t1846,t256]) ).
cnf(t1848,plain,
true = ifeq(true,true,ifeq(closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true,ifeq(true,true,open_subset(subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))),sk5),true),true),true),
inference(step,[status(thm)],[t1847,t1421]) ).
cnf(t1849,plain,
true = ifeq(closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true,ifeq(true,true,open_subset(subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))),sk5),true),true),
inference(step,[status(thm)],[t1848,t256]) ).
fof(f8,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) )
=> closed_subset(topstr_closure(A,B),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_tops_1) ).
fof(f8_nnf,plain,
! [A,B] :
( closed_subset(topstr_closure(A,B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B] :
( closed_subset(topstr_closure(A,B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c9,plain,
( closed_subset(topstr_closure(X0,X1),X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t210,plain,
ifeq(topological_space(X1),true,ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,closed_subset(topstr_closure(X1,X2),X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t1034,plain,
ifeq(topological_space(X1),true,ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,closed_subset(topstr_closure(X1,X2),X1),true),true),true) = true,
inference(orient,[status(thm)],[t210]) ).
cnf(t1552,plain,
true = ifeq(topological_space(sk5),true,ifeq(top_str(sk5),true,ifeq(true,true,closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true),true),true),
inference(cp,[status(thm)],[t1034,t1548]) ).
cnf(t1772,plain,
true = ifeq(true,true,ifeq(top_str(sk5),true,ifeq(true,true,closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true),true),true),
inference(step,[status(thm)],[t1552,t1445]) ).
cnf(t1773,plain,
true = ifeq(top_str(sk5),true,ifeq(true,true,closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true),true),
inference(step,[status(thm)],[t1772,t256]) ).
cnf(t1774,plain,
true = ifeq(true,true,ifeq(true,true,closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true),true),
inference(step,[status(thm)],[t1773,t1421]) ).
cnf(t1775,plain,
true = ifeq(true,true,closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),true),
inference(step,[status(thm)],[t1774,t256]) ).
cnf(t1776,plain,
true = closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5),
inference(step,[status(thm)],[t1775,t256]) ).
cnf(t1605,plain,
closed_subset(topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6)),sk5) = true,
inference(orient,[status(thm)],[t1776]) ).
cnf(t1850,plain,
true = ifeq(true,true,ifeq(true,true,open_subset(subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))),sk5),true),true),
inference(step,[status(thm)],[t1849,t1605]) ).
cnf(t1851,plain,
true = ifeq(true,true,open_subset(subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))),sk5),true),
inference(step,[status(thm)],[t1850,t256]) ).
cnf(t1852,plain,
true = open_subset(subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))),sk5),
inference(step,[status(thm)],[t1851,t256]) ).
fof(f19,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tops_1) ).
fof(f19_nnf,plain,
! [A] :
( ! [B] :
( interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B)))
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A,B] :
( interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c22,plain,
( interior(X0,X1) = subset_complement(the_carrier(X0),topstr_closure(X0,subset_complement(the_carrier(X0),X1)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(hi18,axiom,
ifeq(top_str(X0),true,ifeq(element(X1,powerset(the_carrier(X0))),true,interior(X0,X1),subset_complement(the_carrier(X0),topstr_closure(X0,subset_complement(the_carrier(X0),X1)))),subset_complement(the_carrier(X0),topstr_closure(X0,subset_complement(the_carrier(X0),X1)))) = subset_complement(the_carrier(X0),topstr_closure(X0,subset_complement(the_carrier(X0),X1))),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(hi20,negated_conjecture,
top_str(sk5) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(hi21,negated_conjecture,
element(sk6,powerset(the_carrier(sk5))) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t63,plain,
subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))) = interior(sk5,sk6),
inference(hyper_resolution,[status(thm)],[hi18,hi20,hi21]) ).
cnf(t370,plain,
subset_complement(the_carrier(sk5),topstr_closure(sk5,subset_complement(the_carrier(sk5),sk6))) = interior(sk5,sk6),
inference(orient,[status(thm)],[t63]) ).
cnf(t1853,plain,
true = open_subset(interior(sk5,sk6),sk5),
inference(step,[status(thm)],[t1852,t370]) ).
cnf(t1684,plain,
open_subset(interior(sk5,sk6),sk5) = true,
inference(orient,[status(thm)],[t1853]) ).
cnf(c26,plain,
~ open_subset(interior(sk5,sk6),sk5),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(goal_0,negated_conjecture,
open_subset(interior(sk5,sk6),sk5) != true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1684]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU323+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/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:41:51 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 33.82/4.85 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.82/4.85 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------