%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU309+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 : art07.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:22:18 EST 2010
% Result : Theorem 1.63s
% Output : Solution 1.63s
% 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/SystemOnTPTP5693/SEU309+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP5693/SEU309+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP5693/SEU309+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 5789
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.021 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(one_sorted_str(X1)=>cast_as_carrier_subset(X1)=the_carrier(X1)),file('/tmp/SRASS.s.p', d3_pre_topc)).
% fof(2, axiom,![X1]:(one_sorted_str(X1)=>element(cast_as_carrier_subset(X1),powerset(the_carrier(X1)))),file('/tmp/SRASS.s.p', dt_k2_pre_topc)).
% fof(3, axiom,![X1]:![X2]:![X3]:((element(X2,powerset(X1))&element(X3,powerset(X1)))=>element(subset_difference(X1,X2,X3),powerset(X1))),file('/tmp/SRASS.s.p', dt_k6_subset_1)).
% fof(6, axiom,![X1]:(one_sorted_str(X1)=>![X2]:(element(X2,powerset(the_carrier(X1)))=>subset_intersection2(the_carrier(X1),X2,cast_as_carrier_subset(X1))=X2)),file('/tmp/SRASS.s.p', t15_pre_topc)).
% fof(7, axiom,![X1]:![X2]:![X3]:((element(X2,powerset(X1))&element(X3,powerset(X1)))=>subset_difference(X1,X2,X3)=set_difference(X2,X3)),file('/tmp/SRASS.s.p', redefinition_k6_subset_1)).
% fof(8, axiom,![X1]:![X2]:![X3]:((element(X2,powerset(X1))&element(X3,powerset(X1)))=>subset_intersection2(X1,X2,X3)=subset_intersection2(X1,X3,X2)),file('/tmp/SRASS.s.p', commutativity_k5_subset_1)).
% fof(16, axiom,![X1]:![X2]:![X3]:((element(X2,powerset(X1))&element(X3,powerset(X1)))=>subset_intersection2(X1,X2,X3)=set_intersection2(X2,X3)),file('/tmp/SRASS.s.p', redefinition_k5_subset_1)).
% fof(20, axiom,![X1]:![X2]:set_intersection2(X1,X2)=set_intersection2(X2,X1),file('/tmp/SRASS.s.p', commutativity_k3_xboole_0)).
% fof(28, axiom,![X1]:![X2]:set_difference(X1,set_difference(X1,X2))=set_intersection2(X1,X2),file('/tmp/SRASS.s.p', t48_xboole_1)).
% fof(70, conjecture,![X1]:(one_sorted_str(X1)=>![X2]:(element(X2,powerset(the_carrier(X1)))=>subset_difference(the_carrier(X1),cast_as_carrier_subset(X1),subset_difference(the_carrier(X1),cast_as_carrier_subset(X1),X2))=X2)),file('/tmp/SRASS.s.p', t22_pre_topc)).
% fof(71, negated_conjecture,~(![X1]:(one_sorted_str(X1)=>![X2]:(element(X2,powerset(the_carrier(X1)))=>subset_difference(the_carrier(X1),cast_as_carrier_subset(X1),subset_difference(the_carrier(X1),cast_as_carrier_subset(X1),X2))=X2))),inference(assume_negation,[status(cth)],[70])).
% fof(76, plain,![X1]:(~(one_sorted_str(X1))|cast_as_carrier_subset(X1)=the_carrier(X1)),inference(fof_nnf,[status(thm)],[1])).
% fof(77, plain,![X2]:(~(one_sorted_str(X2))|cast_as_carrier_subset(X2)=the_carrier(X2)),inference(variable_rename,[status(thm)],[76])).
% cnf(78,plain,(cast_as_carrier_subset(X1)=the_carrier(X1)|~one_sorted_str(X1)),inference(split_conjunct,[status(thm)],[77])).
% fof(79, plain,![X1]:(~(one_sorted_str(X1))|element(cast_as_carrier_subset(X1),powerset(the_carrier(X1)))),inference(fof_nnf,[status(thm)],[2])).
% fof(80, plain,![X2]:(~(one_sorted_str(X2))|element(cast_as_carrier_subset(X2),powerset(the_carrier(X2)))),inference(variable_rename,[status(thm)],[79])).
% cnf(81,plain,(element(cast_as_carrier_subset(X1),powerset(the_carrier(X1)))|~one_sorted_str(X1)),inference(split_conjunct,[status(thm)],[80])).
% fof(82, plain,![X1]:![X2]:![X3]:((~(element(X2,powerset(X1)))|~(element(X3,powerset(X1))))|element(subset_difference(X1,X2,X3),powerset(X1))),inference(fof_nnf,[status(thm)],[3])).
% fof(83, plain,![X4]:![X5]:![X6]:((~(element(X5,powerset(X4)))|~(element(X6,powerset(X4))))|element(subset_difference(X4,X5,X6),powerset(X4))),inference(variable_rename,[status(thm)],[82])).
% cnf(84,plain,(element(subset_difference(X1,X2,X3),powerset(X1))|~element(X3,powerset(X1))|~element(X2,powerset(X1))),inference(split_conjunct,[status(thm)],[83])).
% fof(91, plain,![X1]:(~(one_sorted_str(X1))|![X2]:(~(element(X2,powerset(the_carrier(X1))))|subset_intersection2(the_carrier(X1),X2,cast_as_carrier_subset(X1))=X2)),inference(fof_nnf,[status(thm)],[6])).
% fof(92, plain,![X3]:(~(one_sorted_str(X3))|![X4]:(~(element(X4,powerset(the_carrier(X3))))|subset_intersection2(the_carrier(X3),X4,cast_as_carrier_subset(X3))=X4)),inference(variable_rename,[status(thm)],[91])).
% fof(93, plain,![X3]:![X4]:((~(element(X4,powerset(the_carrier(X3))))|subset_intersection2(the_carrier(X3),X4,cast_as_carrier_subset(X3))=X4)|~(one_sorted_str(X3))),inference(shift_quantors,[status(thm)],[92])).
% cnf(94,plain,(subset_intersection2(the_carrier(X1),X2,cast_as_carrier_subset(X1))=X2|~one_sorted_str(X1)|~element(X2,powerset(the_carrier(X1)))),inference(split_conjunct,[status(thm)],[93])).
% fof(95, plain,![X1]:![X2]:![X3]:((~(element(X2,powerset(X1)))|~(element(X3,powerset(X1))))|subset_difference(X1,X2,X3)=set_difference(X2,X3)),inference(fof_nnf,[status(thm)],[7])).
% fof(96, plain,![X4]:![X5]:![X6]:((~(element(X5,powerset(X4)))|~(element(X6,powerset(X4))))|subset_difference(X4,X5,X6)=set_difference(X5,X6)),inference(variable_rename,[status(thm)],[95])).
% cnf(97,plain,(subset_difference(X1,X2,X3)=set_difference(X2,X3)|~element(X3,powerset(X1))|~element(X2,powerset(X1))),inference(split_conjunct,[status(thm)],[96])).
% fof(98, plain,![X1]:![X2]:![X3]:((~(element(X2,powerset(X1)))|~(element(X3,powerset(X1))))|subset_intersection2(X1,X2,X3)=subset_intersection2(X1,X3,X2)),inference(fof_nnf,[status(thm)],[8])).
% fof(99, plain,![X4]:![X5]:![X6]:((~(element(X5,powerset(X4)))|~(element(X6,powerset(X4))))|subset_intersection2(X4,X5,X6)=subset_intersection2(X4,X6,X5)),inference(variable_rename,[status(thm)],[98])).
% cnf(100,plain,(subset_intersection2(X1,X2,X3)=subset_intersection2(X1,X3,X2)|~element(X3,powerset(X1))|~element(X2,powerset(X1))),inference(split_conjunct,[status(thm)],[99])).
% fof(128, plain,![X1]:![X2]:![X3]:((~(element(X2,powerset(X1)))|~(element(X3,powerset(X1))))|subset_intersection2(X1,X2,X3)=set_intersection2(X2,X3)),inference(fof_nnf,[status(thm)],[16])).
% fof(129, plain,![X4]:![X5]:![X6]:((~(element(X5,powerset(X4)))|~(element(X6,powerset(X4))))|subset_intersection2(X4,X5,X6)=set_intersection2(X5,X6)),inference(variable_rename,[status(thm)],[128])).
% cnf(130,plain,(subset_intersection2(X1,X2,X3)=set_intersection2(X2,X3)|~element(X3,powerset(X1))|~element(X2,powerset(X1))),inference(split_conjunct,[status(thm)],[129])).
% fof(143, plain,![X3]:![X4]:set_intersection2(X3,X4)=set_intersection2(X4,X3),inference(variable_rename,[status(thm)],[20])).
% cnf(144,plain,(set_intersection2(X1,X2)=set_intersection2(X2,X1)),inference(split_conjunct,[status(thm)],[143])).
% fof(167, plain,![X3]:![X4]:set_difference(X3,set_difference(X3,X4))=set_intersection2(X3,X4),inference(variable_rename,[status(thm)],[28])).
% cnf(168,plain,(set_difference(X1,set_difference(X1,X2))=set_intersection2(X1,X2)),inference(split_conjunct,[status(thm)],[167])).
% fof(360, negated_conjecture,?[X1]:(one_sorted_str(X1)&?[X2]:(element(X2,powerset(the_carrier(X1)))&~(subset_difference(the_carrier(X1),cast_as_carrier_subset(X1),subset_difference(the_carrier(X1),cast_as_carrier_subset(X1),X2))=X2))),inference(fof_nnf,[status(thm)],[71])).
% fof(361, negated_conjecture,?[X3]:(one_sorted_str(X3)&?[X4]:(element(X4,powerset(the_carrier(X3)))&~(subset_difference(the_carrier(X3),cast_as_carrier_subset(X3),subset_difference(the_carrier(X3),cast_as_carrier_subset(X3),X4))=X4))),inference(variable_rename,[status(thm)],[360])).
% fof(362, negated_conjecture,(one_sorted_str(esk6_0)&(element(esk7_0,powerset(the_carrier(esk6_0)))&~(subset_difference(the_carrier(esk6_0),cast_as_carrier_subset(esk6_0),subset_difference(the_carrier(esk6_0),cast_as_carrier_subset(esk6_0),esk7_0))=esk7_0))),inference(skolemize,[status(esa)],[361])).
% cnf(363,negated_conjecture,(subset_difference(the_carrier(esk6_0),cast_as_carrier_subset(esk6_0),subset_difference(the_carrier(esk6_0),cast_as_carrier_subset(esk6_0),esk7_0))!=esk7_0),inference(split_conjunct,[status(thm)],[362])).
% cnf(364,negated_conjecture,(element(esk7_0,powerset(the_carrier(esk6_0)))),inference(split_conjunct,[status(thm)],[362])).
% cnf(365,negated_conjecture,(one_sorted_str(esk6_0)),inference(split_conjunct,[status(thm)],[362])).
% cnf(368,plain,(set_difference(X1,set_difference(X1,X2))=set_difference(X2,set_difference(X2,X1))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[144,168,theory(equality)]),168,theory(equality)]),['unfolding']).
% cnf(399,plain,(subset_intersection2(X1,X2,X3)=set_difference(X2,set_difference(X2,X3))|~element(X3,powerset(X1))|~element(X2,powerset(X1))),inference(rw,[status(thm)],[130,168,theory(equality)]),['unfolding']).
% cnf(402,negated_conjecture,(cast_as_carrier_subset(esk6_0)=the_carrier(esk6_0)),inference(spm,[status(thm)],[78,365,theory(equality)])).
% cnf(1112,negated_conjecture,(subset_difference(the_carrier(esk6_0),X1,esk7_0)=set_difference(X1,esk7_0)|~element(X1,powerset(the_carrier(esk6_0)))),inference(spm,[status(thm)],[97,364,theory(equality)])).
% cnf(1121,negated_conjecture,(subset_intersection2(the_carrier(esk6_0),X1,esk7_0)=subset_intersection2(the_carrier(esk6_0),esk7_0,X1)|~element(X1,powerset(the_carrier(esk6_0)))),inference(spm,[status(thm)],[100,364,theory(equality)])).
% cnf(1130,negated_conjecture,(set_difference(X1,set_difference(X1,esk7_0))=subset_intersection2(the_carrier(esk6_0),X1,esk7_0)|~element(X1,powerset(the_carrier(esk6_0)))),inference(spm,[status(thm)],[399,364,theory(equality)])).
% cnf(1141,negated_conjecture,(element(the_carrier(esk6_0),powerset(the_carrier(esk6_0)))|~one_sorted_str(esk6_0)),inference(spm,[status(thm)],[81,402,theory(equality)])).
% cnf(1142,negated_conjecture,(subset_intersection2(the_carrier(esk6_0),X1,the_carrier(esk6_0))=X1|~element(X1,powerset(the_carrier(esk6_0)))|~one_sorted_str(esk6_0)),inference(spm,[status(thm)],[94,402,theory(equality)])).
% cnf(1143,negated_conjecture,(subset_difference(the_carrier(esk6_0),the_carrier(esk6_0),subset_difference(the_carrier(esk6_0),the_carrier(esk6_0),esk7_0))!=esk7_0),inference(rw,[status(thm)],[inference(rw,[status(thm)],[363,402,theory(equality)]),402,theory(equality)])).
% cnf(1144,negated_conjecture,(element(the_carrier(esk6_0),powerset(the_carrier(esk6_0)))|$false),inference(rw,[status(thm)],[1141,365,theory(equality)])).
% cnf(1145,negated_conjecture,(element(the_carrier(esk6_0),powerset(the_carrier(esk6_0)))),inference(cn,[status(thm)],[1144,theory(equality)])).
% cnf(1146,negated_conjecture,(subset_intersection2(the_carrier(esk6_0),X1,the_carrier(esk6_0))=X1|~element(X1,powerset(the_carrier(esk6_0)))|$false),inference(rw,[status(thm)],[1142,365,theory(equality)])).
% cnf(1147,negated_conjecture,(subset_intersection2(the_carrier(esk6_0),X1,the_carrier(esk6_0))=X1|~element(X1,powerset(the_carrier(esk6_0)))),inference(cn,[status(thm)],[1146,theory(equality)])).
% cnf(2056,negated_conjecture,(subset_difference(the_carrier(esk6_0),the_carrier(esk6_0),esk7_0)=set_difference(the_carrier(esk6_0),esk7_0)),inference(spm,[status(thm)],[1112,1145,theory(equality)])).
% cnf(2116,negated_conjecture,(element(set_difference(the_carrier(esk6_0),esk7_0),powerset(the_carrier(esk6_0)))|~element(esk7_0,powerset(the_carrier(esk6_0)))|~element(the_carrier(esk6_0),powerset(the_carrier(esk6_0)))),inference(spm,[status(thm)],[84,2056,theory(equality)])).
% cnf(2121,negated_conjecture,(subset_difference(the_carrier(esk6_0),the_carrier(esk6_0),set_difference(the_carrier(esk6_0),esk7_0))!=esk7_0),inference(rw,[status(thm)],[1143,2056,theory(equality)])).
% cnf(2125,negated_conjecture,(element(set_difference(the_carrier(esk6_0),esk7_0),powerset(the_carrier(esk6_0)))|$false|~element(the_carrier(esk6_0),powerset(the_carrier(esk6_0)))),inference(rw,[status(thm)],[2116,364,theory(equality)])).
% cnf(2126,negated_conjecture,(element(set_difference(the_carrier(esk6_0),esk7_0),powerset(the_carrier(esk6_0)))|$false|$false),inference(rw,[status(thm)],[2125,1145,theory(equality)])).
% cnf(2127,negated_conjecture,(element(set_difference(the_carrier(esk6_0),esk7_0),powerset(the_carrier(esk6_0)))),inference(cn,[status(thm)],[2126,theory(equality)])).
% cnf(2176,negated_conjecture,(subset_difference(the_carrier(esk6_0),X1,set_difference(the_carrier(esk6_0),esk7_0))=set_difference(X1,set_difference(the_carrier(esk6_0),esk7_0))|~element(X1,powerset(the_carrier(esk6_0)))),inference(spm,[status(thm)],[97,2127,theory(equality)])).
% cnf(10452,negated_conjecture,(subset_intersection2(the_carrier(esk6_0),the_carrier(esk6_0),esk7_0)=subset_intersection2(the_carrier(esk6_0),esk7_0,the_carrier(esk6_0))),inference(spm,[status(thm)],[1121,1145,theory(equality)])).
% cnf(12038,negated_conjecture,(set_difference(the_carrier(esk6_0),set_difference(the_carrier(esk6_0),esk7_0))=subset_intersection2(the_carrier(esk6_0),the_carrier(esk6_0),esk7_0)),inference(spm,[status(thm)],[1130,1145,theory(equality)])).
% cnf(12047,negated_conjecture,(set_difference(esk7_0,set_difference(esk7_0,the_carrier(esk6_0)))=subset_intersection2(the_carrier(esk6_0),the_carrier(esk6_0),esk7_0)),inference(rw,[status(thm)],[12038,368,theory(equality)])).
% cnf(12048,negated_conjecture,(set_difference(esk7_0,set_difference(esk7_0,the_carrier(esk6_0)))=subset_intersection2(the_carrier(esk6_0),esk7_0,the_carrier(esk6_0))),inference(rw,[status(thm)],[12047,10452,theory(equality)])).
% cnf(12746,negated_conjecture,(set_difference(esk7_0,set_difference(esk7_0,the_carrier(esk6_0)))=esk7_0|~element(esk7_0,powerset(the_carrier(esk6_0)))),inference(spm,[status(thm)],[1147,12048,theory(equality)])).
% cnf(12882,negated_conjecture,(set_difference(esk7_0,set_difference(esk7_0,the_carrier(esk6_0)))=esk7_0|$false),inference(rw,[status(thm)],[12746,364,theory(equality)])).
% cnf(12883,negated_conjecture,(set_difference(esk7_0,set_difference(esk7_0,the_carrier(esk6_0)))=esk7_0),inference(cn,[status(thm)],[12882,theory(equality)])).
% cnf(18699,negated_conjecture,(set_difference(the_carrier(esk6_0),set_difference(the_carrier(esk6_0),esk7_0))!=esk7_0|~element(the_carrier(esk6_0),powerset(the_carrier(esk6_0)))),inference(spm,[status(thm)],[2121,2176,theory(equality)])).
% cnf(18787,negated_conjecture,($false|~element(the_carrier(esk6_0),powerset(the_carrier(esk6_0)))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[18699,368,theory(equality)]),12883,theory(equality)])).
% cnf(18788,negated_conjecture,($false|$false),inference(rw,[status(thm)],[18787,1145,theory(equality)])).
% cnf(18789,negated_conjecture,($false),inference(cn,[status(thm)],[18788,theory(equality)])).
% cnf(18790,negated_conjecture,($false),18789,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 3357
% # ...of these trivial : 11
% # ...subsumed : 2308
% # ...remaining for further processing: 1038
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 32
% # Backward-rewritten : 38
% # Generated clauses : 9087
% # ...of the previous two non-trivial : 7781
% # Contextual simplify-reflections : 304
% # Paramodulations : 9083
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 851
% # Positive orientable unit clauses: 76
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 16
% # Non-unit-clauses : 758
% # Current number of unprocessed clauses: 4199
% # ...number of literals in the above : 15356
% # Clause-clause subsumption calls (NU) : 8553
% # Rec. Clause-clause subsumption calls : 8400
% # Unit Clause-clause subsumption calls : 502
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 50
% # Indexed BW rewrite successes : 9
% # Backwards rewriting index: 379 leaves, 1.31+/-1.089 terms/leaf
% # Paramod-from index: 245 leaves, 1.18+/-0.680 terms/leaf
% # Paramod-into index: 333 leaves, 1.23+/-0.867 terms/leaf
% # -------------------------------------------------
% # User time : 0.410 s
% # System time : 0.010 s
% # Total time : 0.420 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.68 CPU 0.77 WC
% FINAL PrfWatch: 0.68 CPU 0.77 WC
% SZS output end Solution for /tmp/SystemOnTPTP5693/SEU309+1.tptp
%
%------------------------------------------------------------------------------