%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU101+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 : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Thu Dec 30 01:07:26 EST 2010
% Result : Theorem 9.60s
% Output : Solution 9.60s
% 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/SystemOnTPTP10426/SEU101+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP10426/SEU101+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP10426/SEU101+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 10558
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.94 CPU 2.03 WC
% PrfWatch: 3.94 CPU 4.03 WC
% # Preprocessing time : 0.015 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 5.76 CPU 6.04 WC
% PrfWatch: 7.61 CPU 8.05 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,![X1]:(diff_closed(X1)<=>![X2]:![X3]:((in(X2,X1)&in(X3,X1))=>in(set_difference(X2,X3),X1))),file('/tmp/SRASS.s.p', d3_finsub_1)).
% fof(3, axiom,![X1]:(cup_closed(X1)<=>![X2]:![X3]:((in(X2,X1)&in(X3,X1))=>in(set_union2(X2,X3),X1))),file('/tmp/SRASS.s.p', d1_finsub_1)).
% fof(10, axiom,![X1]:![X2]:set_union2(X1,X2)=set_union2(X2,X1),file('/tmp/SRASS.s.p', commutativity_k2_xboole_0)).
% fof(18, axiom,![X1]:(preboolean(X1)=>(cup_closed(X1)&diff_closed(X1))),file('/tmp/SRASS.s.p', cc1_finsub_1)).
% fof(19, axiom,![X1]:((cup_closed(X1)&diff_closed(X1))=>preboolean(X1)),file('/tmp/SRASS.s.p', cc2_finsub_1)).
% fof(39, conjecture,![X1]:(preboolean(X1)<=>![X2]:![X3]:((in(X2,X1)&in(X3,X1))=>(in(set_union2(X2,X3),X1)&in(set_difference(X2,X3),X1)))),file('/tmp/SRASS.s.p', t10_finsub_1)).
% fof(40, negated_conjecture,~(![X1]:(preboolean(X1)<=>![X2]:![X3]:((in(X2,X1)&in(X3,X1))=>(in(set_union2(X2,X3),X1)&in(set_difference(X2,X3),X1))))),inference(assume_negation,[status(cth)],[39])).
% fof(54, plain,![X1]:((~(diff_closed(X1))|![X2]:![X3]:((~(in(X2,X1))|~(in(X3,X1)))|in(set_difference(X2,X3),X1)))&(?[X2]:?[X3]:((in(X2,X1)&in(X3,X1))&~(in(set_difference(X2,X3),X1)))|diff_closed(X1))),inference(fof_nnf,[status(thm)],[2])).
% fof(55, plain,![X4]:((~(diff_closed(X4))|![X5]:![X6]:((~(in(X5,X4))|~(in(X6,X4)))|in(set_difference(X5,X6),X4)))&(?[X7]:?[X8]:((in(X7,X4)&in(X8,X4))&~(in(set_difference(X7,X8),X4)))|diff_closed(X4))),inference(variable_rename,[status(thm)],[54])).
% fof(56, plain,![X4]:((~(diff_closed(X4))|![X5]:![X6]:((~(in(X5,X4))|~(in(X6,X4)))|in(set_difference(X5,X6),X4)))&(((in(esk1_1(X4),X4)&in(esk2_1(X4),X4))&~(in(set_difference(esk1_1(X4),esk2_1(X4)),X4)))|diff_closed(X4))),inference(skolemize,[status(esa)],[55])).
% fof(57, plain,![X4]:![X5]:![X6]:((((~(in(X5,X4))|~(in(X6,X4)))|in(set_difference(X5,X6),X4))|~(diff_closed(X4)))&(((in(esk1_1(X4),X4)&in(esk2_1(X4),X4))&~(in(set_difference(esk1_1(X4),esk2_1(X4)),X4)))|diff_closed(X4))),inference(shift_quantors,[status(thm)],[56])).
% fof(58, plain,![X4]:![X5]:![X6]:((((~(in(X5,X4))|~(in(X6,X4)))|in(set_difference(X5,X6),X4))|~(diff_closed(X4)))&(((in(esk1_1(X4),X4)|diff_closed(X4))&(in(esk2_1(X4),X4)|diff_closed(X4)))&(~(in(set_difference(esk1_1(X4),esk2_1(X4)),X4))|diff_closed(X4)))),inference(distribute,[status(thm)],[57])).
% cnf(59,plain,(diff_closed(X1)|~in(set_difference(esk1_1(X1),esk2_1(X1)),X1)),inference(split_conjunct,[status(thm)],[58])).
% cnf(60,plain,(diff_closed(X1)|in(esk2_1(X1),X1)),inference(split_conjunct,[status(thm)],[58])).
% cnf(61,plain,(diff_closed(X1)|in(esk1_1(X1),X1)),inference(split_conjunct,[status(thm)],[58])).
% cnf(62,plain,(in(set_difference(X2,X3),X1)|~diff_closed(X1)|~in(X3,X1)|~in(X2,X1)),inference(split_conjunct,[status(thm)],[58])).
% fof(63, plain,![X1]:((~(cup_closed(X1))|![X2]:![X3]:((~(in(X2,X1))|~(in(X3,X1)))|in(set_union2(X2,X3),X1)))&(?[X2]:?[X3]:((in(X2,X1)&in(X3,X1))&~(in(set_union2(X2,X3),X1)))|cup_closed(X1))),inference(fof_nnf,[status(thm)],[3])).
% fof(64, plain,![X4]:((~(cup_closed(X4))|![X5]:![X6]:((~(in(X5,X4))|~(in(X6,X4)))|in(set_union2(X5,X6),X4)))&(?[X7]:?[X8]:((in(X7,X4)&in(X8,X4))&~(in(set_union2(X7,X8),X4)))|cup_closed(X4))),inference(variable_rename,[status(thm)],[63])).
% fof(65, plain,![X4]:((~(cup_closed(X4))|![X5]:![X6]:((~(in(X5,X4))|~(in(X6,X4)))|in(set_union2(X5,X6),X4)))&(((in(esk3_1(X4),X4)&in(esk4_1(X4),X4))&~(in(set_union2(esk3_1(X4),esk4_1(X4)),X4)))|cup_closed(X4))),inference(skolemize,[status(esa)],[64])).
% fof(66, plain,![X4]:![X5]:![X6]:((((~(in(X5,X4))|~(in(X6,X4)))|in(set_union2(X5,X6),X4))|~(cup_closed(X4)))&(((in(esk3_1(X4),X4)&in(esk4_1(X4),X4))&~(in(set_union2(esk3_1(X4),esk4_1(X4)),X4)))|cup_closed(X4))),inference(shift_quantors,[status(thm)],[65])).
% fof(67, plain,![X4]:![X5]:![X6]:((((~(in(X5,X4))|~(in(X6,X4)))|in(set_union2(X5,X6),X4))|~(cup_closed(X4)))&(((in(esk3_1(X4),X4)|cup_closed(X4))&(in(esk4_1(X4),X4)|cup_closed(X4)))&(~(in(set_union2(esk3_1(X4),esk4_1(X4)),X4))|cup_closed(X4)))),inference(distribute,[status(thm)],[66])).
% cnf(68,plain,(cup_closed(X1)|~in(set_union2(esk3_1(X1),esk4_1(X1)),X1)),inference(split_conjunct,[status(thm)],[67])).
% cnf(69,plain,(cup_closed(X1)|in(esk4_1(X1),X1)),inference(split_conjunct,[status(thm)],[67])).
% cnf(70,plain,(cup_closed(X1)|in(esk3_1(X1),X1)),inference(split_conjunct,[status(thm)],[67])).
% cnf(71,plain,(in(set_union2(X2,X3),X1)|~cup_closed(X1)|~in(X3,X1)|~in(X2,X1)),inference(split_conjunct,[status(thm)],[67])).
% fof(90, plain,![X3]:![X4]:set_union2(X3,X4)=set_union2(X4,X3),inference(variable_rename,[status(thm)],[10])).
% cnf(91,plain,(set_union2(X1,X2)=set_union2(X2,X1)),inference(split_conjunct,[status(thm)],[90])).
% fof(110, plain,![X1]:(~(preboolean(X1))|(cup_closed(X1)&diff_closed(X1))),inference(fof_nnf,[status(thm)],[18])).
% fof(111, plain,![X2]:(~(preboolean(X2))|(cup_closed(X2)&diff_closed(X2))),inference(variable_rename,[status(thm)],[110])).
% fof(112, plain,![X2]:((cup_closed(X2)|~(preboolean(X2)))&(diff_closed(X2)|~(preboolean(X2)))),inference(distribute,[status(thm)],[111])).
% cnf(113,plain,(diff_closed(X1)|~preboolean(X1)),inference(split_conjunct,[status(thm)],[112])).
% cnf(114,plain,(cup_closed(X1)|~preboolean(X1)),inference(split_conjunct,[status(thm)],[112])).
% fof(115, plain,![X1]:((~(cup_closed(X1))|~(diff_closed(X1)))|preboolean(X1)),inference(fof_nnf,[status(thm)],[19])).
% fof(116, plain,![X2]:((~(cup_closed(X2))|~(diff_closed(X2)))|preboolean(X2)),inference(variable_rename,[status(thm)],[115])).
% cnf(117,plain,(preboolean(X1)|~diff_closed(X1)|~cup_closed(X1)),inference(split_conjunct,[status(thm)],[116])).
% fof(201, negated_conjecture,?[X1]:((~(preboolean(X1))|?[X2]:?[X3]:((in(X2,X1)&in(X3,X1))&(~(in(set_union2(X2,X3),X1))|~(in(set_difference(X2,X3),X1)))))&(preboolean(X1)|![X2]:![X3]:((~(in(X2,X1))|~(in(X3,X1)))|(in(set_union2(X2,X3),X1)&in(set_difference(X2,X3),X1))))),inference(fof_nnf,[status(thm)],[40])).
% fof(202, negated_conjecture,?[X4]:((~(preboolean(X4))|?[X5]:?[X6]:((in(X5,X4)&in(X6,X4))&(~(in(set_union2(X5,X6),X4))|~(in(set_difference(X5,X6),X4)))))&(preboolean(X4)|![X7]:![X8]:((~(in(X7,X4))|~(in(X8,X4)))|(in(set_union2(X7,X8),X4)&in(set_difference(X7,X8),X4))))),inference(variable_rename,[status(thm)],[201])).
% fof(203, negated_conjecture,((~(preboolean(esk15_0))|((in(esk16_0,esk15_0)&in(esk17_0,esk15_0))&(~(in(set_union2(esk16_0,esk17_0),esk15_0))|~(in(set_difference(esk16_0,esk17_0),esk15_0)))))&(preboolean(esk15_0)|![X7]:![X8]:((~(in(X7,esk15_0))|~(in(X8,esk15_0)))|(in(set_union2(X7,X8),esk15_0)&in(set_difference(X7,X8),esk15_0))))),inference(skolemize,[status(esa)],[202])).
% fof(204, negated_conjecture,![X7]:![X8]:((((~(in(X7,esk15_0))|~(in(X8,esk15_0)))|(in(set_union2(X7,X8),esk15_0)&in(set_difference(X7,X8),esk15_0)))|preboolean(esk15_0))&(~(preboolean(esk15_0))|((in(esk16_0,esk15_0)&in(esk17_0,esk15_0))&(~(in(set_union2(esk16_0,esk17_0),esk15_0))|~(in(set_difference(esk16_0,esk17_0),esk15_0)))))),inference(shift_quantors,[status(thm)],[203])).
% fof(205, negated_conjecture,![X7]:![X8]:((((in(set_union2(X7,X8),esk15_0)|(~(in(X7,esk15_0))|~(in(X8,esk15_0))))|preboolean(esk15_0))&((in(set_difference(X7,X8),esk15_0)|(~(in(X7,esk15_0))|~(in(X8,esk15_0))))|preboolean(esk15_0)))&(((in(esk16_0,esk15_0)|~(preboolean(esk15_0)))&(in(esk17_0,esk15_0)|~(preboolean(esk15_0))))&((~(in(set_union2(esk16_0,esk17_0),esk15_0))|~(in(set_difference(esk16_0,esk17_0),esk15_0)))|~(preboolean(esk15_0))))),inference(distribute,[status(thm)],[204])).
% cnf(206,negated_conjecture,(~preboolean(esk15_0)|~in(set_difference(esk16_0,esk17_0),esk15_0)|~in(set_union2(esk16_0,esk17_0),esk15_0)),inference(split_conjunct,[status(thm)],[205])).
% cnf(207,negated_conjecture,(in(esk17_0,esk15_0)|~preboolean(esk15_0)),inference(split_conjunct,[status(thm)],[205])).
% cnf(208,negated_conjecture,(in(esk16_0,esk15_0)|~preboolean(esk15_0)),inference(split_conjunct,[status(thm)],[205])).
% cnf(209,negated_conjecture,(preboolean(esk15_0)|in(set_difference(X2,X1),esk15_0)|~in(X1,esk15_0)|~in(X2,esk15_0)),inference(split_conjunct,[status(thm)],[205])).
% cnf(210,negated_conjecture,(preboolean(esk15_0)|in(set_union2(X2,X1),esk15_0)|~in(X1,esk15_0)|~in(X2,esk15_0)),inference(split_conjunct,[status(thm)],[205])).
% cnf(306,negated_conjecture,(preboolean(esk15_0)|in(set_difference(esk1_1(esk15_0),X1),esk15_0)|diff_closed(esk15_0)|~in(X1,esk15_0)),inference(pm,[status(thm)],[209,61,theory(equality)])).
% cnf(315,negated_conjecture,(preboolean(esk15_0)|in(set_union2(esk4_1(esk15_0),X1),esk15_0)|cup_closed(esk15_0)|~in(X1,esk15_0)),inference(pm,[status(thm)],[210,69,theory(equality)])).
% cnf(1218,negated_conjecture,(preboolean(esk15_0)|diff_closed(esk15_0)|in(set_difference(esk1_1(esk15_0),esk2_1(esk15_0)),esk15_0)),inference(pm,[status(thm)],[306,60,theory(equality)])).
% cnf(1570,negated_conjecture,(preboolean(esk15_0)|cup_closed(esk15_0)|in(set_union2(esk4_1(esk15_0),esk3_1(esk15_0)),esk15_0)),inference(pm,[status(thm)],[315,70,theory(equality)])).
% cnf(220944,negated_conjecture,(diff_closed(esk15_0)|preboolean(esk15_0)),inference(pm,[status(thm)],[59,1218,theory(equality)])).
% cnf(223138,negated_conjecture,(preboolean(esk15_0)|cup_closed(esk15_0)|in(set_union2(esk3_1(esk15_0),esk4_1(esk15_0)),esk15_0)),inference(rw,[status(thm)],[1570,91,theory(equality)])).
% cnf(223158,negated_conjecture,(cup_closed(esk15_0)|preboolean(esk15_0)),inference(pm,[status(thm)],[68,223138,theory(equality)])).
% cnf(223159,negated_conjecture,(preboolean(esk15_0)|~diff_closed(esk15_0)),inference(pm,[status(thm)],[117,223158,theory(equality)])).
% cnf(223163,negated_conjecture,(preboolean(esk15_0)),inference(pm,[status(thm)],[223159,220944,theory(equality)])).
% cnf(224619,negated_conjecture,(diff_closed(esk15_0)),inference(pm,[status(thm)],[113,223163,theory(equality)])).
% cnf(224620,negated_conjecture,(cup_closed(esk15_0)),inference(pm,[status(thm)],[114,223163,theory(equality)])).
% cnf(224626,negated_conjecture,($false|~in(set_difference(esk16_0,esk17_0),esk15_0)|~in(set_union2(esk16_0,esk17_0),esk15_0)),inference(rw,[status(thm)],[206,223163,theory(equality)])).
% cnf(224627,negated_conjecture,(~in(set_difference(esk16_0,esk17_0),esk15_0)|~in(set_union2(esk16_0,esk17_0),esk15_0)),inference(cn,[status(thm)],[224626,theory(equality)])).
% cnf(224630,negated_conjecture,(in(esk17_0,esk15_0)|$false),inference(rw,[status(thm)],[207,223163,theory(equality)])).
% cnf(224631,negated_conjecture,(in(esk17_0,esk15_0)),inference(cn,[status(thm)],[224630,theory(equality)])).
% cnf(224632,negated_conjecture,(in(esk16_0,esk15_0)|$false),inference(rw,[status(thm)],[208,223163,theory(equality)])).
% cnf(224633,negated_conjecture,(in(esk16_0,esk15_0)),inference(cn,[status(thm)],[224632,theory(equality)])).
% cnf(224662,negated_conjecture,(in(set_difference(X1,esk17_0),esk15_0)|~diff_closed(esk15_0)|~in(X1,esk15_0)),inference(pm,[status(thm)],[62,224631,theory(equality)])).
% cnf(224663,negated_conjecture,(in(set_union2(X1,esk17_0),esk15_0)|~cup_closed(esk15_0)|~in(X1,esk15_0)),inference(pm,[status(thm)],[71,224631,theory(equality)])).
% cnf(224680,negated_conjecture,(in(set_difference(X1,esk17_0),esk15_0)|$false|~in(X1,esk15_0)),inference(rw,[status(thm)],[224662,224619,theory(equality)])).
% cnf(224681,negated_conjecture,(in(set_difference(X1,esk17_0),esk15_0)|~in(X1,esk15_0)),inference(cn,[status(thm)],[224680,theory(equality)])).
% cnf(224682,negated_conjecture,(in(set_union2(X1,esk17_0),esk15_0)|$false|~in(X1,esk15_0)),inference(rw,[status(thm)],[224663,224620,theory(equality)])).
% cnf(224683,negated_conjecture,(in(set_union2(X1,esk17_0),esk15_0)|~in(X1,esk15_0)),inference(cn,[status(thm)],[224682,theory(equality)])).
% cnf(224720,negated_conjecture,(in(set_difference(esk16_0,esk17_0),esk15_0)),inference(pm,[status(thm)],[224681,224633,theory(equality)])).
% cnf(225205,negated_conjecture,($false|~in(set_union2(esk16_0,esk17_0),esk15_0)),inference(rw,[status(thm)],[224627,224720,theory(equality)])).
% cnf(225206,negated_conjecture,(~in(set_union2(esk16_0,esk17_0),esk15_0)),inference(cn,[status(thm)],[225205,theory(equality)])).
% cnf(225691,negated_conjecture,(in(set_union2(esk16_0,esk17_0),esk15_0)),inference(pm,[status(thm)],[224683,224633,theory(equality)])).
% cnf(225716,negated_conjecture,($false),inference(sr,[status(thm)],[225691,225206,theory(equality)])).
% cnf(225717,negated_conjecture,($false),225716,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2435
% # ...of these trivial : 126
% # ...subsumed : 731
% # ...remaining for further processing: 1578
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 40
% # Backward-rewritten : 127
% # Generated clauses : 223125
% # ...of the previous two non-trivial : 221983
% # Contextual simplify-reflections : 0
% # Paramodulations : 223122
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1411
% # Positive orientable unit clauses: 295
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 18
% # Non-unit-clauses : 1097
% # Current number of unprocessed clauses: 216209
% # ...number of literals in the above : 473230
% # Clause-clause subsumption calls (NU) : 28946
% # Rec. Clause-clause subsumption calls : 22538
% # Unit Clause-clause subsumption calls : 3970
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 3211
% # Indexed BW rewrite successes : 25
% # Backwards rewriting index: 1073 leaves, 2.83+/-7.571 terms/leaf
% # Paramod-from index: 270 leaves, 2.86+/-6.769 terms/leaf
% # Paramod-into index: 748 leaves, 2.26+/-4.495 terms/leaf
% # -------------------------------------------------
% # User time : 4.701 s
% # System time : 0.226 s
% # Total time : 4.927 s
% # Maximum resident set size: 0 pages
% PrfWatch: 8.52 CPU 8.96 WC
% FINAL PrfWatch: 8.52 CPU 8.96 WC
% SZS output end Solution for /tmp/SystemOnTPTP10426/SEU101+1.tptp
%
%------------------------------------------------------------------------------