%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SET935+1 : TPTP v5.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art05.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 00:20:47 EST 2010
% Result : Theorem 1.02s
% Output : Solution 1.02s
% 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/SystemOnTPTP2871/SET935+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP2871/SET935+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP2871/SET935+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 2967
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.013 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:set_union2(X1,X2)=set_union2(X2,X1),file('/tmp/SRASS.s.p', commutativity_k2_xboole_0)).
% fof(5, axiom,![X1]:![X2]:![X3]:(X3=set_union2(X1,X2)<=>![X4]:(in(X4,X3)<=>(in(X4,X1)|in(X4,X2)))),file('/tmp/SRASS.s.p', d2_xboole_0)).
% fof(6, axiom,![X1]:![X2]:(inclusion_comparable(X1,X2)<=>(subset(X1,X2)|subset(X2,X1))),file('/tmp/SRASS.s.p', d9_xboole_0)).
% fof(7, axiom,![X1]:![X2]:(X2=powerset(X1)<=>![X3]:(in(X3,X2)<=>subset(X3,X1))),file('/tmp/SRASS.s.p', d1_zfmisc_1)).
% fof(9, axiom,![X1]:![X2]:(X1=X2<=>(subset(X1,X2)&subset(X2,X1))),file('/tmp/SRASS.s.p', d10_xboole_0)).
% fof(12, axiom,![X1]:![X2]:subset(X1,X1),file('/tmp/SRASS.s.p', reflexivity_r1_tarski)).
% fof(13, axiom,![X1]:![X2]:subset(X1,set_union2(X1,X2)),file('/tmp/SRASS.s.p', t7_xboole_1)).
% fof(16, conjecture,![X1]:![X2]:(set_union2(powerset(X1),powerset(X2))=powerset(set_union2(X1,X2))=>inclusion_comparable(X1,X2)),file('/tmp/SRASS.s.p', t82_zfmisc_1)).
% fof(17, negated_conjecture,~(![X1]:![X2]:(set_union2(powerset(X1),powerset(X2))=powerset(set_union2(X1,X2))=>inclusion_comparable(X1,X2))),inference(assume_negation,[status(cth)],[16])).
% fof(22, plain,![X3]:![X4]:set_union2(X3,X4)=set_union2(X4,X3),inference(variable_rename,[status(thm)],[1])).
% cnf(23,plain,(set_union2(X1,X2)=set_union2(X2,X1)),inference(split_conjunct,[status(thm)],[22])).
% fof(31, plain,![X1]:![X2]:![X3]:((~(X3=set_union2(X1,X2))|![X4]:((~(in(X4,X3))|(in(X4,X1)|in(X4,X2)))&((~(in(X4,X1))&~(in(X4,X2)))|in(X4,X3))))&(?[X4]:((~(in(X4,X3))|(~(in(X4,X1))&~(in(X4,X2))))&(in(X4,X3)|(in(X4,X1)|in(X4,X2))))|X3=set_union2(X1,X2))),inference(fof_nnf,[status(thm)],[5])).
% fof(32, plain,![X5]:![X6]:![X7]:((~(X7=set_union2(X5,X6))|![X8]:((~(in(X8,X7))|(in(X8,X5)|in(X8,X6)))&((~(in(X8,X5))&~(in(X8,X6)))|in(X8,X7))))&(?[X9]:((~(in(X9,X7))|(~(in(X9,X5))&~(in(X9,X6))))&(in(X9,X7)|(in(X9,X5)|in(X9,X6))))|X7=set_union2(X5,X6))),inference(variable_rename,[status(thm)],[31])).
% fof(33, plain,![X5]:![X6]:![X7]:((~(X7=set_union2(X5,X6))|![X8]:((~(in(X8,X7))|(in(X8,X5)|in(X8,X6)))&((~(in(X8,X5))&~(in(X8,X6)))|in(X8,X7))))&(((~(in(esk1_3(X5,X6,X7),X7))|(~(in(esk1_3(X5,X6,X7),X5))&~(in(esk1_3(X5,X6,X7),X6))))&(in(esk1_3(X5,X6,X7),X7)|(in(esk1_3(X5,X6,X7),X5)|in(esk1_3(X5,X6,X7),X6))))|X7=set_union2(X5,X6))),inference(skolemize,[status(esa)],[32])).
% fof(34, plain,![X5]:![X6]:![X7]:![X8]:((((~(in(X8,X7))|(in(X8,X5)|in(X8,X6)))&((~(in(X8,X5))&~(in(X8,X6)))|in(X8,X7)))|~(X7=set_union2(X5,X6)))&(((~(in(esk1_3(X5,X6,X7),X7))|(~(in(esk1_3(X5,X6,X7),X5))&~(in(esk1_3(X5,X6,X7),X6))))&(in(esk1_3(X5,X6,X7),X7)|(in(esk1_3(X5,X6,X7),X5)|in(esk1_3(X5,X6,X7),X6))))|X7=set_union2(X5,X6))),inference(shift_quantors,[status(thm)],[33])).
% fof(35, plain,![X5]:![X6]:![X7]:![X8]:((((~(in(X8,X7))|(in(X8,X5)|in(X8,X6)))|~(X7=set_union2(X5,X6)))&(((~(in(X8,X5))|in(X8,X7))|~(X7=set_union2(X5,X6)))&((~(in(X8,X6))|in(X8,X7))|~(X7=set_union2(X5,X6)))))&((((~(in(esk1_3(X5,X6,X7),X5))|~(in(esk1_3(X5,X6,X7),X7)))|X7=set_union2(X5,X6))&((~(in(esk1_3(X5,X6,X7),X6))|~(in(esk1_3(X5,X6,X7),X7)))|X7=set_union2(X5,X6)))&((in(esk1_3(X5,X6,X7),X7)|(in(esk1_3(X5,X6,X7),X5)|in(esk1_3(X5,X6,X7),X6)))|X7=set_union2(X5,X6)))),inference(distribute,[status(thm)],[34])).
% cnf(41,plain,(in(X4,X3)|in(X4,X2)|X1!=set_union2(X2,X3)|~in(X4,X1)),inference(split_conjunct,[status(thm)],[35])).
% fof(42, plain,![X1]:![X2]:((~(inclusion_comparable(X1,X2))|(subset(X1,X2)|subset(X2,X1)))&((~(subset(X1,X2))&~(subset(X2,X1)))|inclusion_comparable(X1,X2))),inference(fof_nnf,[status(thm)],[6])).
% fof(43, plain,![X3]:![X4]:((~(inclusion_comparable(X3,X4))|(subset(X3,X4)|subset(X4,X3)))&((~(subset(X3,X4))&~(subset(X4,X3)))|inclusion_comparable(X3,X4))),inference(variable_rename,[status(thm)],[42])).
% fof(44, plain,![X3]:![X4]:((~(inclusion_comparable(X3,X4))|(subset(X3,X4)|subset(X4,X3)))&((~(subset(X3,X4))|inclusion_comparable(X3,X4))&(~(subset(X4,X3))|inclusion_comparable(X3,X4)))),inference(distribute,[status(thm)],[43])).
% cnf(45,plain,(inclusion_comparable(X1,X2)|~subset(X2,X1)),inference(split_conjunct,[status(thm)],[44])).
% cnf(46,plain,(inclusion_comparable(X1,X2)|~subset(X1,X2)),inference(split_conjunct,[status(thm)],[44])).
% fof(48, 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)],[7])).
% fof(49, 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)],[48])).
% fof(50, plain,![X4]:![X5]:((~(X5=powerset(X4))|![X6]:((~(in(X6,X5))|subset(X6,X4))&(~(subset(X6,X4))|in(X6,X5))))&(((~(in(esk2_2(X4,X5),X5))|~(subset(esk2_2(X4,X5),X4)))&(in(esk2_2(X4,X5),X5)|subset(esk2_2(X4,X5),X4)))|X5=powerset(X4))),inference(skolemize,[status(esa)],[49])).
% fof(51, plain,![X4]:![X5]:![X6]:((((~(in(X6,X5))|subset(X6,X4))&(~(subset(X6,X4))|in(X6,X5)))|~(X5=powerset(X4)))&(((~(in(esk2_2(X4,X5),X5))|~(subset(esk2_2(X4,X5),X4)))&(in(esk2_2(X4,X5),X5)|subset(esk2_2(X4,X5),X4)))|X5=powerset(X4))),inference(shift_quantors,[status(thm)],[50])).
% fof(52, plain,![X4]:![X5]:![X6]:((((~(in(X6,X5))|subset(X6,X4))|~(X5=powerset(X4)))&((~(subset(X6,X4))|in(X6,X5))|~(X5=powerset(X4))))&(((~(in(esk2_2(X4,X5),X5))|~(subset(esk2_2(X4,X5),X4)))|X5=powerset(X4))&((in(esk2_2(X4,X5),X5)|subset(esk2_2(X4,X5),X4))|X5=powerset(X4)))),inference(distribute,[status(thm)],[51])).
% cnf(55,plain,(in(X3,X1)|X1!=powerset(X2)|~subset(X3,X2)),inference(split_conjunct,[status(thm)],[52])).
% cnf(56,plain,(subset(X3,X2)|X1!=powerset(X2)|~in(X3,X1)),inference(split_conjunct,[status(thm)],[52])).
% fof(60, plain,![X1]:![X2]:((~(X1=X2)|(subset(X1,X2)&subset(X2,X1)))&((~(subset(X1,X2))|~(subset(X2,X1)))|X1=X2)),inference(fof_nnf,[status(thm)],[9])).
% fof(61, plain,![X3]:![X4]:((~(X3=X4)|(subset(X3,X4)&subset(X4,X3)))&((~(subset(X3,X4))|~(subset(X4,X3)))|X3=X4)),inference(variable_rename,[status(thm)],[60])).
% fof(62, plain,![X3]:![X4]:(((subset(X3,X4)|~(X3=X4))&(subset(X4,X3)|~(X3=X4)))&((~(subset(X3,X4))|~(subset(X4,X3)))|X3=X4)),inference(distribute,[status(thm)],[61])).
% cnf(63,plain,(X1=X2|~subset(X2,X1)|~subset(X1,X2)),inference(split_conjunct,[status(thm)],[62])).
% fof(72, plain,![X3]:![X4]:subset(X3,X3),inference(variable_rename,[status(thm)],[12])).
% cnf(73,plain,(subset(X1,X1)),inference(split_conjunct,[status(thm)],[72])).
% fof(74, plain,![X3]:![X4]:subset(X3,set_union2(X3,X4)),inference(variable_rename,[status(thm)],[13])).
% cnf(75,plain,(subset(X1,set_union2(X1,X2))),inference(split_conjunct,[status(thm)],[74])).
% fof(82, negated_conjecture,?[X1]:?[X2]:(set_union2(powerset(X1),powerset(X2))=powerset(set_union2(X1,X2))&~(inclusion_comparable(X1,X2))),inference(fof_nnf,[status(thm)],[17])).
% fof(83, negated_conjecture,?[X3]:?[X4]:(set_union2(powerset(X3),powerset(X4))=powerset(set_union2(X3,X4))&~(inclusion_comparable(X3,X4))),inference(variable_rename,[status(thm)],[82])).
% fof(84, negated_conjecture,(set_union2(powerset(esk5_0),powerset(esk6_0))=powerset(set_union2(esk5_0,esk6_0))&~(inclusion_comparable(esk5_0,esk6_0))),inference(skolemize,[status(esa)],[83])).
% cnf(85,negated_conjecture,(~inclusion_comparable(esk5_0,esk6_0)),inference(split_conjunct,[status(thm)],[84])).
% cnf(86,negated_conjecture,(set_union2(powerset(esk5_0),powerset(esk6_0))=powerset(set_union2(esk5_0,esk6_0))),inference(split_conjunct,[status(thm)],[84])).
% cnf(96,plain,(subset(X1,set_union2(X2,X1))),inference(spm,[status(thm)],[75,23,theory(equality)])).
% cnf(99,negated_conjecture,(~subset(esk6_0,esk5_0)),inference(spm,[status(thm)],[85,45,theory(equality)])).
% cnf(100,negated_conjecture,(~subset(esk5_0,esk6_0)),inference(spm,[status(thm)],[85,46,theory(equality)])).
% cnf(112,plain,(in(X1,X2)|powerset(X1)!=X2),inference(spm,[status(thm)],[55,73,theory(equality)])).
% cnf(154,plain,(in(X1,X2)|in(X1,X3)|~in(X1,set_union2(X3,X2))),inference(er,[status(thm)],[41,theory(equality)])).
% cnf(267,plain,(in(X1,powerset(X1))),inference(er,[status(thm)],[112,theory(equality)])).
% cnf(277,negated_conjecture,(in(set_union2(esk5_0,esk6_0),set_union2(powerset(esk5_0),powerset(esk6_0)))),inference(spm,[status(thm)],[267,86,theory(equality)])).
% cnf(1964,negated_conjecture,(in(set_union2(esk5_0,esk6_0),powerset(esk5_0))|in(set_union2(esk5_0,esk6_0),powerset(esk6_0))),inference(spm,[status(thm)],[154,277,theory(equality)])).
% cnf(2041,negated_conjecture,(subset(set_union2(esk5_0,esk6_0),X1)|in(set_union2(esk5_0,esk6_0),powerset(esk5_0))|powerset(X1)!=powerset(esk6_0)),inference(spm,[status(thm)],[56,1964,theory(equality)])).
% cnf(2164,negated_conjecture,(subset(set_union2(esk5_0,esk6_0),esk6_0)|in(set_union2(esk5_0,esk6_0),powerset(esk5_0))),inference(er,[status(thm)],[2041,theory(equality)])).
% cnf(2190,negated_conjecture,(esk6_0=set_union2(esk5_0,esk6_0)|in(set_union2(esk5_0,esk6_0),powerset(esk5_0))|~subset(esk6_0,set_union2(esk5_0,esk6_0))),inference(spm,[status(thm)],[63,2164,theory(equality)])).
% cnf(2211,negated_conjecture,(esk6_0=set_union2(esk5_0,esk6_0)|in(set_union2(esk5_0,esk6_0),powerset(esk5_0))|$false),inference(rw,[status(thm)],[2190,96,theory(equality)])).
% cnf(2212,negated_conjecture,(esk6_0=set_union2(esk5_0,esk6_0)|in(set_union2(esk5_0,esk6_0),powerset(esk5_0))),inference(cn,[status(thm)],[2211,theory(equality)])).
% cnf(2214,negated_conjecture,(subset(set_union2(esk5_0,esk6_0),X1)|set_union2(esk5_0,esk6_0)=esk6_0|powerset(X1)!=powerset(esk5_0)),inference(spm,[status(thm)],[56,2212,theory(equality)])).
% cnf(2376,negated_conjecture,(set_union2(esk5_0,esk6_0)=esk6_0|subset(set_union2(esk5_0,esk6_0),esk5_0)),inference(er,[status(thm)],[2214,theory(equality)])).
% cnf(2455,negated_conjecture,(esk5_0=set_union2(esk5_0,esk6_0)|set_union2(esk5_0,esk6_0)=esk6_0|~subset(esk5_0,set_union2(esk5_0,esk6_0))),inference(spm,[status(thm)],[63,2376,theory(equality)])).
% cnf(2476,negated_conjecture,(esk5_0=set_union2(esk5_0,esk6_0)|set_union2(esk5_0,esk6_0)=esk6_0|$false),inference(rw,[status(thm)],[2455,75,theory(equality)])).
% cnf(2477,negated_conjecture,(esk5_0=set_union2(esk5_0,esk6_0)|set_union2(esk5_0,esk6_0)=esk6_0),inference(cn,[status(thm)],[2476,theory(equality)])).
% cnf(2479,negated_conjecture,(subset(esk5_0,esk6_0)|set_union2(esk5_0,esk6_0)=esk5_0),inference(spm,[status(thm)],[75,2477,theory(equality)])).
% cnf(2533,negated_conjecture,(set_union2(esk5_0,esk6_0)=esk5_0),inference(sr,[status(thm)],[2479,100,theory(equality)])).
% cnf(2554,negated_conjecture,(subset(esk6_0,esk5_0)),inference(spm,[status(thm)],[96,2533,theory(equality)])).
% cnf(2617,negated_conjecture,($false),inference(sr,[status(thm)],[2554,99,theory(equality)])).
% cnf(2618,negated_conjecture,($false),2617,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 277
% # ...of these trivial : 2
% # ...subsumed : 138
% # ...remaining for further processing: 137
% # Other redundant clauses eliminated : 23
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 19
% # Generated clauses : 2416
% # ...of the previous two non-trivial : 2289
% # Contextual simplify-reflections : 2
% # Paramodulations : 2373
% # Factorizations : 5
% # Equation resolutions : 38
% # Current number of processed clauses: 89
% # Positive orientable unit clauses: 12
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 22
% # Non-unit-clauses : 54
% # Current number of unprocessed clauses: 1360
% # ...number of literals in the above : 6319
% # Clause-clause subsumption calls (NU) : 651
% # Rec. Clause-clause subsumption calls : 587
% # Unit Clause-clause subsumption calls : 57
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 17
% # Indexed BW rewrite successes : 13
% # Backwards rewriting index: 83 leaves, 1.77+/-1.935 terms/leaf
% # Paramod-from index: 24 leaves, 1.46+/-0.763 terms/leaf
% # Paramod-into index: 66 leaves, 1.74+/-1.885 terms/leaf
% # -------------------------------------------------
% # User time : 0.094 s
% # System time : 0.006 s
% # Total time : 0.100 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.23 CPU 0.29 WC
% FINAL PrfWatch: 0.23 CPU 0.29 WC
% SZS output end Solution for /tmp/SystemOnTPTP2871/SET935+1.tptp
%
%------------------------------------------------------------------------------