%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU323+2 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art09.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Thu Dec 30 03:32:25 EST 2010
% Result : Theorem 36.86s
% Output : Solution 36.86s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP10627/SEU323+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP10627/SEU323+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP10627/SEU323+2.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 10723
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.91 CPU 2.01 WC
% PrfWatch: 3.59 CPU 4.01 WC
% PrfWatch: 5.17 CPU 6.02 WC
% PrfWatch: 7.17 CPU 8.02 WC
% PrfWatch: 9.15 CPU 10.03 WC
% PrfWatch: 11.14 CPU 12.03 WC
% PrfWatch: 13.14 CPU 14.04 WC
% PrfWatch: 15.13 CPU 16.04 WC
% # Preprocessing time : 0.239 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 17.13 CPU 18.05 WC
% PrfWatch: 19.12 CPU 20.05 WC
% PrfWatch: 21.12 CPU 22.06 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:((top_str(X1)&element(X2,powerset(the_carrier(X1))))=>element(interior(X1,X2),powerset(the_carrier(X1)))),file('/tmp/SRASS.s.p', dt_k1_tops_1)).
% fof(7, axiom,![X1]:![X2]:((top_str(X1)&element(X2,powerset(the_carrier(X1))))=>element(topstr_closure(X1,X2),powerset(the_carrier(X1)))),file('/tmp/SRASS.s.p', dt_k6_pre_topc)).
% fof(15, axiom,![X1]:(top_str(X1)=>![X2]:(element(X2,powerset(the_carrier(X1)))=>(open_subset(X2,X1)<=>closed_subset(subset_complement(the_carrier(X1),X2),X1)))),file('/tmp/SRASS.s.p', t30_tops_1)).
% fof(16, axiom,![X1]:![X2]:![X3]:((in(X1,X2)&element(X2,powerset(X3)))=>element(X1,X3)),file('/tmp/SRASS.s.p', t4_subset)).
% fof(17, axiom,![X1]:![X2]:(((topological_space(X1)&top_str(X1))&element(X2,powerset(the_carrier(X1))))=>closed_subset(topstr_closure(X1,X2),X1)),file('/tmp/SRASS.s.p', fc2_tops_1)).
% fof(18, axiom,![X1]:![X2]:(element(X1,powerset(X2))<=>subset(X1,X2)),file('/tmp/SRASS.s.p', t3_subset)).
% fof(24, axiom,![X1]:(top_str(X1)=>![X2]:(element(X2,powerset(the_carrier(X1)))=>interior(X1,X2)=subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2))))),file('/tmp/SRASS.s.p', d1_tops_1)).
% fof(29, axiom,![X1]:![X2]:(element(X2,powerset(X1))=>element(subset_complement(X1,X2),powerset(X1))),file('/tmp/SRASS.s.p', dt_k3_subset_1)).
% fof(51, axiom,![X1]:![X2]:(X2=powerset(X1)<=>![X3]:(in(X3,X2)<=>subset(X3,X1))),file('/tmp/SRASS.s.p', d1_zfmisc_1)).
% fof(57, axiom,![X1]:![X2]:(element(X2,powerset(X1))=>subset_complement(X1,subset_complement(X1,X2))=X2),file('/tmp/SRASS.s.p', involutiveness_k3_subset_1)).
% fof(61, axiom,![X1]:![X2]:subset(X1,X1),file('/tmp/SRASS.s.p', reflexivity_r1_tarski)).
% fof(82, axiom,![X1]:![X2]:(element(X2,powerset(X1))=>subset_complement(X1,X2)=set_difference(X1,X2)),file('/tmp/SRASS.s.p', d5_subset_1)).
% fof(532, conjecture,![X1]:((topological_space(X1)&top_str(X1))=>![X2]:(element(X2,powerset(the_carrier(X1)))=>open_subset(interior(X1,X2),X1))),file('/tmp/SRASS.s.p', t51_tops_1)).
% fof(533, negated_conjecture,~(![X1]:((topological_space(X1)&top_str(X1))=>![X2]:(element(X2,powerset(the_carrier(X1)))=>open_subset(interior(X1,X2),X1)))),inference(assume_negation,[status(cth)],[532])).
% fof(614, plain,![X1]:![X2]:((~(top_str(X1))|~(element(X2,powerset(the_carrier(X1)))))|element(interior(X1,X2),powerset(the_carrier(X1)))),inference(fof_nnf,[status(thm)],[1])).
% fof(615, plain,![X3]:![X4]:((~(top_str(X3))|~(element(X4,powerset(the_carrier(X3)))))|element(interior(X3,X4),powerset(the_carrier(X3)))),inference(variable_rename,[status(thm)],[614])).
% cnf(616,plain,(element(interior(X1,X2),powerset(the_carrier(X1)))|~element(X2,powerset(the_carrier(X1)))|~top_str(X1)),inference(split_conjunct,[status(thm)],[615])).
% fof(639, plain,![X1]:![X2]:((~(top_str(X1))|~(element(X2,powerset(the_carrier(X1)))))|element(topstr_closure(X1,X2),powerset(the_carrier(X1)))),inference(fof_nnf,[status(thm)],[7])).
% fof(640, plain,![X3]:![X4]:((~(top_str(X3))|~(element(X4,powerset(the_carrier(X3)))))|element(topstr_closure(X3,X4),powerset(the_carrier(X3)))),inference(variable_rename,[status(thm)],[639])).
% cnf(641,plain,(element(topstr_closure(X1,X2),powerset(the_carrier(X1)))|~element(X2,powerset(the_carrier(X1)))|~top_str(X1)),inference(split_conjunct,[status(thm)],[640])).
% fof(673, plain,![X1]:(~(top_str(X1))|![X2]:(~(element(X2,powerset(the_carrier(X1))))|((~(open_subset(X2,X1))|closed_subset(subset_complement(the_carrier(X1),X2),X1))&(~(closed_subset(subset_complement(the_carrier(X1),X2),X1))|open_subset(X2,X1))))),inference(fof_nnf,[status(thm)],[15])).
% fof(674, plain,![X3]:(~(top_str(X3))|![X4]:(~(element(X4,powerset(the_carrier(X3))))|((~(open_subset(X4,X3))|closed_subset(subset_complement(the_carrier(X3),X4),X3))&(~(closed_subset(subset_complement(the_carrier(X3),X4),X3))|open_subset(X4,X3))))),inference(variable_rename,[status(thm)],[673])).
% fof(675, plain,![X3]:![X4]:((~(element(X4,powerset(the_carrier(X3))))|((~(open_subset(X4,X3))|closed_subset(subset_complement(the_carrier(X3),X4),X3))&(~(closed_subset(subset_complement(the_carrier(X3),X4),X3))|open_subset(X4,X3))))|~(top_str(X3))),inference(shift_quantors,[status(thm)],[674])).
% fof(676, plain,![X3]:![X4]:((((~(open_subset(X4,X3))|closed_subset(subset_complement(the_carrier(X3),X4),X3))|~(element(X4,powerset(the_carrier(X3)))))|~(top_str(X3)))&(((~(closed_subset(subset_complement(the_carrier(X3),X4),X3))|open_subset(X4,X3))|~(element(X4,powerset(the_carrier(X3)))))|~(top_str(X3)))),inference(distribute,[status(thm)],[675])).
% cnf(677,plain,(open_subset(X2,X1)|~top_str(X1)|~element(X2,powerset(the_carrier(X1)))|~closed_subset(subset_complement(the_carrier(X1),X2),X1)),inference(split_conjunct,[status(thm)],[676])).
% fof(679, plain,![X1]:![X2]:![X3]:((~(in(X1,X2))|~(element(X2,powerset(X3))))|element(X1,X3)),inference(fof_nnf,[status(thm)],[16])).
% fof(680, plain,![X4]:![X5]:![X6]:((~(in(X4,X5))|~(element(X5,powerset(X6))))|element(X4,X6)),inference(variable_rename,[status(thm)],[679])).
% cnf(681,plain,(element(X1,X2)|~element(X3,powerset(X2))|~in(X1,X3)),inference(split_conjunct,[status(thm)],[680])).
% fof(682, plain,![X1]:![X2]:(((~(topological_space(X1))|~(top_str(X1)))|~(element(X2,powerset(the_carrier(X1)))))|closed_subset(topstr_closure(X1,X2),X1)),inference(fof_nnf,[status(thm)],[17])).
% fof(683, plain,![X3]:![X4]:(((~(topological_space(X3))|~(top_str(X3)))|~(element(X4,powerset(the_carrier(X3)))))|closed_subset(topstr_closure(X3,X4),X3)),inference(variable_rename,[status(thm)],[682])).
% cnf(684,plain,(closed_subset(topstr_closure(X1,X2),X1)|~element(X2,powerset(the_carrier(X1)))|~top_str(X1)|~topological_space(X1)),inference(split_conjunct,[status(thm)],[683])).
% fof(685, plain,![X1]:![X2]:((~(element(X1,powerset(X2)))|subset(X1,X2))&(~(subset(X1,X2))|element(X1,powerset(X2)))),inference(fof_nnf,[status(thm)],[18])).
% fof(686, plain,![X3]:![X4]:((~(element(X3,powerset(X4)))|subset(X3,X4))&(~(subset(X3,X4))|element(X3,powerset(X4)))),inference(variable_rename,[status(thm)],[685])).
% cnf(687,plain,(element(X1,powerset(X2))|~subset(X1,X2)),inference(split_conjunct,[status(thm)],[686])).
% cnf(688,plain,(subset(X1,X2)|~element(X1,powerset(X2))),inference(split_conjunct,[status(thm)],[686])).
% fof(711, plain,![X1]:(~(top_str(X1))|![X2]:(~(element(X2,powerset(the_carrier(X1))))|interior(X1,X2)=subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2))))),inference(fof_nnf,[status(thm)],[24])).
% fof(712, plain,![X3]:(~(top_str(X3))|![X4]:(~(element(X4,powerset(the_carrier(X3))))|interior(X3,X4)=subset_complement(the_carrier(X3),topstr_closure(X3,subset_complement(the_carrier(X3),X4))))),inference(variable_rename,[status(thm)],[711])).
% fof(713, plain,![X3]:![X4]:((~(element(X4,powerset(the_carrier(X3))))|interior(X3,X4)=subset_complement(the_carrier(X3),topstr_closure(X3,subset_complement(the_carrier(X3),X4))))|~(top_str(X3))),inference(shift_quantors,[status(thm)],[712])).
% cnf(714,plain,(interior(X1,X2)=subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2)))|~top_str(X1)|~element(X2,powerset(the_carrier(X1)))),inference(split_conjunct,[status(thm)],[713])).
% fof(739, plain,![X1]:![X2]:(~(element(X2,powerset(X1)))|element(subset_complement(X1,X2),powerset(X1))),inference(fof_nnf,[status(thm)],[29])).
% fof(740, plain,![X3]:![X4]:(~(element(X4,powerset(X3)))|element(subset_complement(X3,X4),powerset(X3))),inference(variable_rename,[status(thm)],[739])).
% cnf(741,plain,(element(subset_complement(X1,X2),powerset(X1))|~element(X2,powerset(X1))),inference(split_conjunct,[status(thm)],[740])).
% fof(966, plain,![X1]:![X2]:((~(X2=powerset(X1))|![X3]:((~(in(X3,X2))|subset(X3,X1))&(~(subset(X3,X1))|in(X3,X2))))&(?[X3]:((~(in(X3,X2))|~(subset(X3,X1)))&(in(X3,X2)|subset(X3,X1)))|X2=powerset(X1))),inference(fof_nnf,[status(thm)],[51])).
% fof(967, plain,![X4]:![X5]:((~(X5=powerset(X4))|![X6]:((~(in(X6,X5))|subset(X6,X4))&(~(subset(X6,X4))|in(X6,X5))))&(?[X7]:((~(in(X7,X5))|~(subset(X7,X4)))&(in(X7,X5)|subset(X7,X4)))|X5=powerset(X4))),inference(variable_rename,[status(thm)],[966])).
% fof(968, plain,![X4]:![X5]:((~(X5=powerset(X4))|![X6]:((~(in(X6,X5))|subset(X6,X4))&(~(subset(X6,X4))|in(X6,X5))))&(((~(in(esk34_2(X4,X5),X5))|~(subset(esk34_2(X4,X5),X4)))&(in(esk34_2(X4,X5),X5)|subset(esk34_2(X4,X5),X4)))|X5=powerset(X4))),inference(skolemize,[status(esa)],[967])).
% fof(969, plain,![X4]:![X5]:![X6]:((((~(in(X6,X5))|subset(X6,X4))&(~(subset(X6,X4))|in(X6,X5)))|~(X5=powerset(X4)))&(((~(in(esk34_2(X4,X5),X5))|~(subset(esk34_2(X4,X5),X4)))&(in(esk34_2(X4,X5),X5)|subset(esk34_2(X4,X5),X4)))|X5=powerset(X4))),inference(shift_quantors,[status(thm)],[968])).
% fof(970, plain,![X4]:![X5]:![X6]:((((~(in(X6,X5))|subset(X6,X4))|~(X5=powerset(X4)))&((~(subset(X6,X4))|in(X6,X5))|~(X5=powerset(X4))))&(((~(in(esk34_2(X4,X5),X5))|~(subset(esk34_2(X4,X5),X4)))|X5=powerset(X4))&((in(esk34_2(X4,X5),X5)|subset(esk34_2(X4,X5),X4))|X5=powerset(X4)))),inference(distribute,[status(thm)],[969])).
% cnf(973,plain,(in(X3,X1)|X1!=powerset(X2)|~subset(X3,X2)),inference(split_conjunct,[status(thm)],[970])).
% fof(995, plain,![X1]:![X2]:(~(element(X2,powerset(X1)))|subset_complement(X1,subset_complement(X1,X2))=X2),inference(fof_nnf,[status(thm)],[57])).
% fof(996, plain,![X3]:![X4]:(~(element(X4,powerset(X3)))|subset_complement(X3,subset_complement(X3,X4))=X4),inference(variable_rename,[status(thm)],[995])).
% cnf(997,plain,(subset_complement(X1,subset_complement(X1,X2))=X2|~element(X2,powerset(X1))),inference(split_conjunct,[status(thm)],[996])).
% fof(1007, plain,![X3]:![X4]:subset(X3,X3),inference(variable_rename,[status(thm)],[61])).
% cnf(1008,plain,(subset(X1,X1)),inference(split_conjunct,[status(thm)],[1007])).
% fof(1109, plain,![X1]:![X2]:(~(element(X2,powerset(X1)))|subset_complement(X1,X2)=set_difference(X1,X2)),inference(fof_nnf,[status(thm)],[82])).
% fof(1110, plain,![X3]:![X4]:(~(element(X4,powerset(X3)))|subset_complement(X3,X4)=set_difference(X3,X4)),inference(variable_rename,[status(thm)],[1109])).
% cnf(1111,plain,(subset_complement(X1,X2)=set_difference(X1,X2)|~element(X2,powerset(X1))),inference(split_conjunct,[status(thm)],[1110])).
% fof(4054, negated_conjecture,?[X1]:((topological_space(X1)&top_str(X1))&?[X2]:(element(X2,powerset(the_carrier(X1)))&~(open_subset(interior(X1,X2),X1)))),inference(fof_nnf,[status(thm)],[533])).
% fof(4055, negated_conjecture,?[X3]:((topological_space(X3)&top_str(X3))&?[X4]:(element(X4,powerset(the_carrier(X3)))&~(open_subset(interior(X3,X4),X3)))),inference(variable_rename,[status(thm)],[4054])).
% fof(4056, negated_conjecture,((topological_space(esk341_0)&top_str(esk341_0))&(element(esk342_0,powerset(the_carrier(esk341_0)))&~(open_subset(interior(esk341_0,esk342_0),esk341_0)))),inference(skolemize,[status(esa)],[4055])).
% cnf(4057,negated_conjecture,(~open_subset(interior(esk341_0,esk342_0),esk341_0)),inference(split_conjunct,[status(thm)],[4056])).
% cnf(4058,negated_conjecture,(element(esk342_0,powerset(the_carrier(esk341_0)))),inference(split_conjunct,[status(thm)],[4056])).
% cnf(4059,negated_conjecture,(top_str(esk341_0)),inference(split_conjunct,[status(thm)],[4056])).
% cnf(4060,negated_conjecture,(topological_space(esk341_0)),inference(split_conjunct,[status(thm)],[4056])).
% cnf(6107,negated_conjecture,(subset_complement(the_carrier(esk341_0),esk342_0)=set_difference(the_carrier(esk341_0),esk342_0)),inference(spm,[status(thm)],[1111,4058,theory(equality)])).
% cnf(6942,plain,(subset(interior(X1,X2),the_carrier(X1))|~element(X2,powerset(the_carrier(X1)))|~top_str(X1)),inference(spm,[status(thm)],[688,616,theory(equality)])).
% cnf(6943,plain,(subset_complement(the_carrier(X1),interior(X1,X2))=set_difference(the_carrier(X1),interior(X1,X2))|~element(X2,powerset(the_carrier(X1)))|~top_str(X1)),inference(spm,[status(thm)],[1111,616,theory(equality)])).
% cnf(7447,plain,(element(X1,X2)|~in(X1,X3)|~subset(X3,X2)),inference(spm,[status(thm)],[681,687,theory(equality)])).
% cnf(7717,plain,(subset_complement(the_carrier(X1),subset_complement(the_carrier(X1),topstr_closure(X1,X2)))=topstr_closure(X1,X2)|~element(X2,powerset(the_carrier(X1)))|~top_str(X1)),inference(spm,[status(thm)],[997,641,theory(equality)])).
% cnf(14553,negated_conjecture,(subset_complement(the_carrier(esk341_0),topstr_closure(esk341_0,subset_complement(the_carrier(esk341_0),esk342_0)))=interior(esk341_0,esk342_0)|~top_str(esk341_0)),inference(spm,[status(thm)],[714,4058,theory(equality)])).
% cnf(14576,negated_conjecture,(subset_complement(the_carrier(esk341_0),topstr_closure(esk341_0,subset_complement(the_carrier(esk341_0),esk342_0)))=interior(esk341_0,esk342_0)|$false),inference(rw,[status(thm)],[14553,4059,theory(equality)])).
% cnf(14577,negated_conjecture,(subset_complement(the_carrier(esk341_0),topstr_closure(esk341_0,subset_complement(the_carrier(esk341_0),esk342_0)))=interior(esk341_0,esk342_0)),inference(cn,[status(thm)],[14576,theory(equality)])).
% cnf(108279,negated_conjecture,(element(set_difference(the_carrier(esk341_0),esk342_0),powerset(the_carrier(esk341_0)))|~element(esk342_0,powerset(the_carrier(esk341_0)))),inference(spm,[status(thm)],[741,6107,theory(equality)])).
% cnf(108287,negated_conjecture,(element(set_difference(the_carrier(esk341_0),esk342_0),powerset(the_carrier(esk341_0)))|$false),inference(rw,[status(thm)],[108279,4058,theory(equality)])).
% cnf(108288,negated_conjecture,(element(set_difference(the_carrier(esk341_0),esk342_0),powerset(the_carrier(esk341_0)))),inference(cn,[status(thm)],[108287,theory(equality)])).
% cnf(117791,negated_conjecture,(closed_subset(topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0)),esk341_0)|~topological_space(esk341_0)|~top_str(esk341_0)),inference(spm,[status(thm)],[684,108288,theory(equality)])).
% cnf(117922,negated_conjecture,(closed_subset(topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0)),esk341_0)|$false|~top_str(esk341_0)),inference(rw,[status(thm)],[117791,4060,theory(equality)])).
% cnf(117923,negated_conjecture,(closed_subset(topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0)),esk341_0)|$false|$false),inference(rw,[status(thm)],[117922,4059,theory(equality)])).
% cnf(117924,negated_conjecture,(closed_subset(topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0)),esk341_0)),inference(cn,[status(thm)],[117923,theory(equality)])).
% cnf(141241,negated_conjecture,(subset_complement(the_carrier(esk341_0),topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0)))=interior(esk341_0,esk342_0)),inference(rw,[status(thm)],[14577,6107,theory(equality)])).
% cnf(191794,negated_conjecture,(subset(interior(esk341_0,esk342_0),the_carrier(esk341_0))|~top_str(esk341_0)),inference(spm,[status(thm)],[6942,4058,theory(equality)])).
% cnf(191869,negated_conjecture,(subset(interior(esk341_0,esk342_0),the_carrier(esk341_0))|$false),inference(rw,[status(thm)],[191794,4059,theory(equality)])).
% cnf(191870,negated_conjecture,(subset(interior(esk341_0,esk342_0),the_carrier(esk341_0))),inference(cn,[status(thm)],[191869,theory(equality)])).
% cnf(191905,negated_conjecture,(in(interior(esk341_0,esk342_0),X1)|powerset(the_carrier(esk341_0))!=X1),inference(spm,[status(thm)],[973,191870,theory(equality)])).
% cnf(191945,negated_conjecture,(subset_complement(the_carrier(esk341_0),interior(esk341_0,esk342_0))=set_difference(the_carrier(esk341_0),interior(esk341_0,esk342_0))|~top_str(esk341_0)),inference(spm,[status(thm)],[6943,4058,theory(equality)])).
% cnf(192021,negated_conjecture,(subset_complement(the_carrier(esk341_0),interior(esk341_0,esk342_0))=set_difference(the_carrier(esk341_0),interior(esk341_0,esk342_0))|$false),inference(rw,[status(thm)],[191945,4059,theory(equality)])).
% cnf(192022,negated_conjecture,(subset_complement(the_carrier(esk341_0),interior(esk341_0,esk342_0))=set_difference(the_carrier(esk341_0),interior(esk341_0,esk342_0))),inference(cn,[status(thm)],[192021,theory(equality)])).
% cnf(195598,negated_conjecture,(in(interior(esk341_0,esk342_0),powerset(the_carrier(esk341_0)))),inference(er,[status(thm)],[191905,theory(equality)])).
% cnf(232934,negated_conjecture,(element(interior(esk341_0,esk342_0),X1)|~subset(powerset(the_carrier(esk341_0)),X1)),inference(spm,[status(thm)],[7447,195598,theory(equality)])).
% cnf(240237,negated_conjecture,(element(interior(esk341_0,esk342_0),powerset(the_carrier(esk341_0)))),inference(spm,[status(thm)],[232934,1008,theory(equality)])).
% cnf(283162,negated_conjecture,(subset_complement(the_carrier(esk341_0),subset_complement(the_carrier(esk341_0),topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0))))=topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0))|~top_str(esk341_0)),inference(spm,[status(thm)],[7717,108288,theory(equality)])).
% cnf(283196,negated_conjecture,(set_difference(the_carrier(esk341_0),interior(esk341_0,esk342_0))=topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0))|~top_str(esk341_0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[283162,141241,theory(equality)]),192022,theory(equality)])).
% cnf(283197,negated_conjecture,(set_difference(the_carrier(esk341_0),interior(esk341_0,esk342_0))=topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0))|$false),inference(rw,[status(thm)],[283196,4059,theory(equality)])).
% cnf(283198,negated_conjecture,(set_difference(the_carrier(esk341_0),interior(esk341_0,esk342_0))=topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0))),inference(cn,[status(thm)],[283197,theory(equality)])).
% cnf(283400,negated_conjecture,(subset_complement(the_carrier(esk341_0),interior(esk341_0,esk342_0))=topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0))),inference(rw,[status(thm)],[192022,283198,theory(equality)])).
% cnf(283464,negated_conjecture,(open_subset(interior(esk341_0,esk342_0),esk341_0)|~closed_subset(topstr_closure(esk341_0,set_difference(the_carrier(esk341_0),esk342_0)),esk341_0)|~element(interior(esk341_0,esk342_0),powerset(the_carrier(esk341_0)))|~top_str(esk341_0)),inference(spm,[status(thm)],[677,283400,theory(equality)])).
% cnf(283498,negated_conjecture,(open_subset(interior(esk341_0,esk342_0),esk341_0)|$false|~element(interior(esk341_0,esk342_0),powerset(the_carrier(esk341_0)))|~top_str(esk341_0)),inference(rw,[status(thm)],[283464,117924,theory(equality)])).
% cnf(283499,negated_conjecture,(open_subset(interior(esk341_0,esk342_0),esk341_0)|$false|$false|~top_str(esk341_0)),inference(rw,[status(thm)],[283498,240237,theory(equality)])).
% cnf(283500,negated_conjecture,(open_subset(interior(esk341_0,esk342_0),esk341_0)|$false|$false|$false),inference(rw,[status(thm)],[283499,4059,theory(equality)])).
% cnf(283501,negated_conjecture,(open_subset(interior(esk341_0,esk342_0),esk341_0)),inference(cn,[status(thm)],[283500,theory(equality)])).
% cnf(283502,negated_conjecture,($false),inference(sr,[status(thm)],[283501,4057,theory(equality)])).
% cnf(283503,negated_conjecture,($false),283502,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 14867
% # ...of these trivial : 180
% # ...subsumed : 7283
% # ...remaining for further processing: 7404
% # Other redundant clauses eliminated : 675
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 45
% # Backward-rewritten : 164
% # Generated clauses : 246664
% # ...of the previous two non-trivial : 235451
% # Contextual simplify-reflections : 2089
% # Paramodulations : 245887
% # Factorizations : 14
% # Equation resolutions : 821
% # Current number of processed clauses: 5109
% # Positive orientable unit clauses: 687
% # Positive unorientable unit clauses: 4
% # Negative unit clauses : 206
% # Non-unit-clauses : 4212
% # Current number of unprocessed clauses: 215376
% # ...number of literals in the above : 1158750
% # Clause-clause subsumption calls (NU) : 3997526
% # Rec. Clause-clause subsumption calls : 1009845
% # Unit Clause-clause subsumption calls : 185176
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 301
% # Indexed BW rewrite successes : 91
% # Backwards rewriting index: 3435 leaves, 1.41+/-2.620 terms/leaf
% # Paramod-from index: 1487 leaves, 1.11+/-1.122 terms/leaf
% # Paramod-into index: 2702 leaves, 1.29+/-2.186 terms/leaf
% # -------------------------------------------------
% # User time : 16.419 s
% # System time : 0.401 s
% # Total time : 16.819 s
% # Maximum resident set size: 0 pages
% PrfWatch: 21.58 CPU 22.55 WC
% FINAL PrfWatch: 21.58 CPU 22.55 WC
% SZS output end Solution for /tmp/SystemOnTPTP10627/SEU323+2.tptp
%
%------------------------------------------------------------------------------