%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU323+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 : Sun Sep 27 08:45:48 AM UTC 2026
% Result : Theorem 0.17s 0.47s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 32 ( 11 unt; 0 def)
% Number of atoms : 79 ( 4 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 76 ( 29 ~; 23 |; 14 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 32 ( 0 sgn 14 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fc3_tops_1,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('theBenchmark.p',fc3_tops_1) ).
fof(dt_k3_subset_1,axiom,
! [A,B] :
( element(B,powerset(A))
=> element(subset_complement(A,B),powerset(A)) ),
file('theBenchmark.p',dt_k3_subset_1) ).
fof(dt_k6_pre_topc,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A) )
=> element(topstr_closure(A,B),powerset(the_carrier(A))) ),
file('theBenchmark.p',dt_k6_pre_topc) ).
fof(fc2_tops_1,axiom,
! [A,B] :
( ( element(B,powerset(the_carrier(A)))
& top_str(A)
& topological_space(A) )
=> closed_subset(topstr_closure(A,B),A) ),
file('theBenchmark.p',fc2_tops_1) ).
fof(d1_tops_1,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('theBenchmark.p',d1_tops_1) ).
fof(t51_tops_1,conjecture,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> open_subset(interior(A,B),A) ) ),
file('theBenchmark.p',t51_tops_1) ).
fof(t51_tops_1_neg,negated_conjecture,
~ ! [A] :
( ( top_str(A)
& topological_space(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> open_subset(interior(A,B),A) ) ),
inference(assume_negation,[status(cth)],[t51_tops_1]) ).
fof(nnf_21,plain,
? [A] :
( ? [B] :
( ~ open_subset(interior(A,B),A)
& element(B,powerset(the_carrier(A))) )
& top_str(A)
& topological_space(A) ),
inference(fof_nnf,[status(thm)],[t51_tops_1_neg]) ).
fof(sk_t51_tops_1_neg,plain,
( ~ open_subset(interior(sK0,sK1),sK0)
& element(sK1,powerset(the_carrier(sK0)))
& top_str(sK0)
& topological_space(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_21]) ).
cnf(c_22,negated_conjecture,
topological_space(sK0),
inference(split_conjunct,[status(thm)],[sk_t51_tops_1_neg]) ).
cnf(c_26,plain,
( closed_subset(topstr_closure(A,B),A)
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(clausify,[status(thm)],[fc2_tops_1]) ).
cnf(c_29,plain,
( 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(clausify,[status(thm)],[fc3_tops_1]) ).
cnf(c_33,negated_conjecture,
( open_subset(subset_complement(the_carrier(sK0),A),sK0)
| ~ element(A,powerset(the_carrier(sK0)))
| ~ closed_subset(A,sK0)
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_22,c_29]) ).
cnf(c_36,negated_conjecture,
( closed_subset(topstr_closure(sK0,A),sK0)
| ~ element(A,powerset(the_carrier(sK0)))
| ~ top_str(sK0) ),
inference(resolve,[status(thm)],[c_22,c_26]) ).
cnf(c_40,negated_conjecture,
~ open_subset(interior(sK0,sK1),sK0),
inference(split_conjunct,[status(thm)],[sk_t51_tops_1_neg]) ).
cnf(c_41,negated_conjecture,
element(sK1,powerset(the_carrier(sK0))),
inference(split_conjunct,[status(thm)],[sk_t51_tops_1_neg]) ).
cnf(c_42,negated_conjecture,
top_str(sK0),
inference(split_conjunct,[status(thm)],[sk_t51_tops_1_neg]) ).
cnf(c_43,plain,
( 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(clausify,[status(thm)],[d1_tops_1]) ).
cnf(c_47,plain,
( element(topstr_closure(A,B),powerset(the_carrier(A)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(clausify,[status(thm)],[dt_k6_pre_topc]) ).
cnf(c_48,plain,
( element(subset_complement(B,A),powerset(B))
| ~ element(A,powerset(B)) ),
inference(clausify,[status(thm)],[dt_k3_subset_1]) ).
cnf(c_174,negated_conjecture,
( interior(sK0,A) = subset_complement(the_carrier(sK0),topstr_closure(sK0,subset_complement(the_carrier(sK0),A)))
| ~ element(A,powerset(the_carrier(sK0))) ),
inference(resolve,[status(thm)],[c_43,c_42]) ).
cnf(c_56,negated_conjecture,
interior(sK0,sK1) = subset_complement(the_carrier(sK0),topstr_closure(sK0,subset_complement(the_carrier(sK0),sK1))),
inference(resolve,[status(thm)],[c_174,c_41]) ).
cnf(c_57,negated_conjecture,
~ open_subset(subset_complement(the_carrier(sK0),topstr_closure(sK0,subset_complement(the_carrier(sK0),sK1))),sK0),
inference(paramod,[status(thm)],[c_56,c_40]) ).
cnf(c_70,negated_conjecture,
element(subset_complement(the_carrier(sK0),sK1),powerset(the_carrier(sK0))),
inference(resolve,[status(thm)],[c_48,c_41]) ).
cnf(c_175,negated_conjecture,
( element(topstr_closure(sK0,A),powerset(the_carrier(sK0)))
| ~ element(A,powerset(the_carrier(sK0))) ),
inference(resolve,[status(thm)],[c_47,c_42]) ).
cnf(c_133,negated_conjecture,
element(topstr_closure(sK0,subset_complement(the_carrier(sK0),sK1)),powerset(the_carrier(sK0))),
inference(resolve,[status(thm)],[c_175,c_70]) ).
cnf(c_176,negated_conjecture,
( closed_subset(topstr_closure(sK0,A),sK0)
| ~ element(A,powerset(the_carrier(sK0))) ),
inference(resolve,[status(thm)],[c_36,c_42]) ).
cnf(c_136,negated_conjecture,
closed_subset(topstr_closure(sK0,subset_complement(the_carrier(sK0),sK1)),sK0),
inference(resolve,[status(thm)],[c_176,c_70]) ).
cnf(c_177,negated_conjecture,
( open_subset(subset_complement(the_carrier(sK0),A),sK0)
| ~ element(A,powerset(the_carrier(sK0)))
| ~ closed_subset(A,sK0) ),
inference(resolve,[status(thm)],[c_33,c_42]) ).
cnf(c_178,negated_conjecture,
( open_subset(subset_complement(the_carrier(sK0),topstr_closure(sK0,subset_complement(the_carrier(sK0),sK1))),sK0)
| ~ element(topstr_closure(sK0,subset_complement(the_carrier(sK0),sK1)),powerset(the_carrier(sK0))) ),
inference(resolve,[status(thm)],[c_177,c_136]) ).
cnf(c_172,negated_conjecture,
~ element(topstr_closure(sK0,subset_complement(the_carrier(sK0),sK1)),powerset(the_carrier(sK0))),
inference(resolve,[status(thm)],[c_178,c_57]) ).
cnf(c_173,plain,
$false,
inference(resolve,[status(thm)],[c_172,c_133]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU323+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n008.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sat Sep 26 09:13:09 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.42 % Process 3277768 was started by sandbox2 on n008,
% 0.17/0.42 % Sat Sep 26 09:13:09 2026
% 0.17/0.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.43
% 0.17/0.43 % From the command line: assign(max_seconds, 300).
% 0.17/0.47
% 0.17/0.47 % SZS status Theorem for theBenchmark
% 0.17/0.47
% 0.17/0.47 % Proof 1 at 0.02 (+ 0.00) seconds.
% 0.17/0.47 % Length of proof is 24.
% 0.17/0.47 % Level of proof is 5.
% 0.17/0.47 % Maximum clause weight is 20.000.
% 0.17/0.47 % Given clauses 47.
% 0.17/0.47
% 0.17/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------