%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU326+1 : 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:33:47 EST 2010
% Result : Theorem 0.99s
% Output : Solution 0.99s
% 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/SystemOnTPTP11181/SEU326+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP11181/SEU326+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP11181/SEU326+1.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 11277
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.016 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:(element(X2,powerset(powerset(X1)))=>element(complements_of_subsets(X1,X2),powerset(powerset(X1)))),file('/tmp/SRASS.s.p', dt_k7_setfam_1)).
% fof(3, axiom,![X1]:![X2]:(element(X2,powerset(powerset(X1)))=>complements_of_subsets(X1,complements_of_subsets(X1,X2))=X2),file('/tmp/SRASS.s.p', involutiveness_k7_setfam_1)).
% fof(4, axiom,![X1]:![X2]:(element(X2,powerset(powerset(X1)))=>~((~(X2=empty_set)&complements_of_subsets(X1,X2)=empty_set))),file('/tmp/SRASS.s.p', t46_setfam_1)).
% fof(5, axiom,![X1]:(empty(X1)=>X1=empty_set),file('/tmp/SRASS.s.p', t6_boole)).
% fof(7, axiom,![X1]:?[X2]:(element(X2,powerset(X1))&empty(X2)),file('/tmp/SRASS.s.p', rc2_subset_1)).
% fof(38, conjecture,![X1]:![X2]:(element(X2,powerset(powerset(X1)))=>(~((~(X2=empty_set)&complements_of_subsets(X1,X2)=empty_set))&~((~(complements_of_subsets(X1,X2)=empty_set)&X2=empty_set)))),file('/tmp/SRASS.s.p', t10_tops_2)).
% fof(39, negated_conjecture,~(![X1]:![X2]:(element(X2,powerset(powerset(X1)))=>(~((~(X2=empty_set)&complements_of_subsets(X1,X2)=empty_set))&~((~(complements_of_subsets(X1,X2)=empty_set)&X2=empty_set))))),inference(assume_negation,[status(cth)],[38])).
% fof(44, plain,![X1]:![X2]:(~(element(X2,powerset(powerset(X1))))|element(complements_of_subsets(X1,X2),powerset(powerset(X1)))),inference(fof_nnf,[status(thm)],[1])).
% fof(45, plain,![X3]:![X4]:(~(element(X4,powerset(powerset(X3))))|element(complements_of_subsets(X3,X4),powerset(powerset(X3)))),inference(variable_rename,[status(thm)],[44])).
% cnf(46,plain,(element(complements_of_subsets(X1,X2),powerset(powerset(X1)))|~element(X2,powerset(powerset(X1)))),inference(split_conjunct,[status(thm)],[45])).
% fof(50, plain,![X1]:![X2]:(~(element(X2,powerset(powerset(X1))))|complements_of_subsets(X1,complements_of_subsets(X1,X2))=X2),inference(fof_nnf,[status(thm)],[3])).
% fof(51, plain,![X3]:![X4]:(~(element(X4,powerset(powerset(X3))))|complements_of_subsets(X3,complements_of_subsets(X3,X4))=X4),inference(variable_rename,[status(thm)],[50])).
% cnf(52,plain,(complements_of_subsets(X1,complements_of_subsets(X1,X2))=X2|~element(X2,powerset(powerset(X1)))),inference(split_conjunct,[status(thm)],[51])).
% fof(53, plain,![X1]:![X2]:(~(element(X2,powerset(powerset(X1))))|(X2=empty_set|~(complements_of_subsets(X1,X2)=empty_set))),inference(fof_nnf,[status(thm)],[4])).
% fof(54, plain,![X3]:![X4]:(~(element(X4,powerset(powerset(X3))))|(X4=empty_set|~(complements_of_subsets(X3,X4)=empty_set))),inference(variable_rename,[status(thm)],[53])).
% cnf(55,plain,(X2=empty_set|complements_of_subsets(X1,X2)!=empty_set|~element(X2,powerset(powerset(X1)))),inference(split_conjunct,[status(thm)],[54])).
% fof(56, plain,![X1]:(~(empty(X1))|X1=empty_set),inference(fof_nnf,[status(thm)],[5])).
% fof(57, plain,![X2]:(~(empty(X2))|X2=empty_set),inference(variable_rename,[status(thm)],[56])).
% cnf(58,plain,(X1=empty_set|~empty(X1)),inference(split_conjunct,[status(thm)],[57])).
% fof(65, plain,![X3]:?[X4]:(element(X4,powerset(X3))&empty(X4)),inference(variable_rename,[status(thm)],[7])).
% fof(66, plain,![X3]:(element(esk3_1(X3),powerset(X3))&empty(esk3_1(X3))),inference(skolemize,[status(esa)],[65])).
% cnf(67,plain,(empty(esk3_1(X1))),inference(split_conjunct,[status(thm)],[66])).
% cnf(68,plain,(element(esk3_1(X1),powerset(X1))),inference(split_conjunct,[status(thm)],[66])).
% fof(203, negated_conjecture,?[X1]:?[X2]:(element(X2,powerset(powerset(X1)))&((~(X2=empty_set)&complements_of_subsets(X1,X2)=empty_set)|(~(complements_of_subsets(X1,X2)=empty_set)&X2=empty_set))),inference(fof_nnf,[status(thm)],[39])).
% fof(204, negated_conjecture,?[X3]:?[X4]:(element(X4,powerset(powerset(X3)))&((~(X4=empty_set)&complements_of_subsets(X3,X4)=empty_set)|(~(complements_of_subsets(X3,X4)=empty_set)&X4=empty_set))),inference(variable_rename,[status(thm)],[203])).
% fof(205, negated_conjecture,(element(esk6_0,powerset(powerset(esk5_0)))&((~(esk6_0=empty_set)&complements_of_subsets(esk5_0,esk6_0)=empty_set)|(~(complements_of_subsets(esk5_0,esk6_0)=empty_set)&esk6_0=empty_set))),inference(skolemize,[status(esa)],[204])).
% fof(206, negated_conjecture,(element(esk6_0,powerset(powerset(esk5_0)))&(((~(complements_of_subsets(esk5_0,esk6_0)=empty_set)|~(esk6_0=empty_set))&(esk6_0=empty_set|~(esk6_0=empty_set)))&((~(complements_of_subsets(esk5_0,esk6_0)=empty_set)|complements_of_subsets(esk5_0,esk6_0)=empty_set)&(esk6_0=empty_set|complements_of_subsets(esk5_0,esk6_0)=empty_set)))),inference(distribute,[status(thm)],[205])).
% cnf(207,negated_conjecture,(complements_of_subsets(esk5_0,esk6_0)=empty_set|esk6_0=empty_set),inference(split_conjunct,[status(thm)],[206])).
% cnf(210,negated_conjecture,(esk6_0!=empty_set|complements_of_subsets(esk5_0,esk6_0)!=empty_set),inference(split_conjunct,[status(thm)],[206])).
% cnf(211,negated_conjecture,(element(esk6_0,powerset(powerset(esk5_0)))),inference(split_conjunct,[status(thm)],[206])).
% cnf(222,plain,(empty_set=esk3_1(X1)),inference(pm,[status(thm)],[58,67,theory(equality)])).
% cnf(382,negated_conjecture,(empty_set=esk6_0|complements_of_subsets(esk5_0,esk6_0)!=empty_set),inference(pm,[status(thm)],[55,211,theory(equality)])).
% cnf(405,plain,(element(empty_set,powerset(X1))),inference(rw,[status(thm)],[68,222,theory(equality)])).
% cnf(423,plain,(complements_of_subsets(X1,complements_of_subsets(X1,empty_set))=empty_set),inference(pm,[status(thm)],[52,405,theory(equality)])).
% cnf(424,plain,(element(complements_of_subsets(X1,empty_set),powerset(powerset(X1)))),inference(pm,[status(thm)],[46,405,theory(equality)])).
% cnf(779,negated_conjecture,(esk6_0=empty_set),inference(pm,[status(thm)],[382,207,theory(equality)])).
% cnf(816,negated_conjecture,(complements_of_subsets(esk5_0,empty_set)!=empty_set|esk6_0!=empty_set),inference(rw,[status(thm)],[210,779,theory(equality)])).
% cnf(817,negated_conjecture,(complements_of_subsets(esk5_0,empty_set)!=empty_set|$false),inference(rw,[status(thm)],[816,779,theory(equality)])).
% cnf(818,negated_conjecture,(complements_of_subsets(esk5_0,empty_set)!=empty_set),inference(cn,[status(thm)],[817,theory(equality)])).
% cnf(1452,plain,(empty_set=complements_of_subsets(X1,empty_set)|complements_of_subsets(X1,complements_of_subsets(X1,empty_set))!=empty_set),inference(pm,[status(thm)],[55,424,theory(equality)])).
% cnf(1456,plain,(empty_set=complements_of_subsets(X1,empty_set)|$false),inference(rw,[status(thm)],[1452,423,theory(equality)])).
% cnf(1457,plain,(empty_set=complements_of_subsets(X1,empty_set)),inference(cn,[status(thm)],[1456,theory(equality)])).
% cnf(1462,negated_conjecture,($false),inference(rw,[status(thm)],[818,1457,theory(equality)])).
% cnf(1463,negated_conjecture,($false),inference(cn,[status(thm)],[1462,theory(equality)])).
% cnf(1464,negated_conjecture,($false),1463,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 465
% # ...of these trivial : 33
% # ...subsumed : 51
% # ...remaining for further processing: 381
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 47
% # Generated clauses : 951
% # ...of the previous two non-trivial : 775
% # Contextual simplify-reflections : 0
% # Paramodulations : 948
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 334
% # Positive orientable unit clauses: 78
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 7
% # Non-unit-clauses : 249
% # Current number of unprocessed clauses: 300
% # ...number of literals in the above : 604
% # Clause-clause subsumption calls (NU) : 318
% # Rec. Clause-clause subsumption calls : 316
% # Unit Clause-clause subsumption calls : 108
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 53
% # Indexed BW rewrite successes : 6
% # Backwards rewriting index: 192 leaves, 1.24+/-0.641 terms/leaf
% # Paramod-from index: 73 leaves, 1.22+/-0.579 terms/leaf
% # Paramod-into index: 134 leaves, 1.23+/-0.572 terms/leaf
% # -------------------------------------------------
% # User time : 0.044 s
% # System time : 0.005 s
% # Total time : 0.049 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.15 CPU 0.23 WC
% FINAL PrfWatch: 0.15 CPU 0.23 WC
% SZS output end Solution for /tmp/SystemOnTPTP11181/SEU326+1.tptp
%
%------------------------------------------------------------------------------