%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : ALG227+1 : TPTP v5.0.0. Released v3.4.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 : Tue Dec 28 21:34:08 EST 2010
% Result : Theorem 0.92s
% Output : Solution 0.92s
% 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/SystemOnTPTP8078/ALG227+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP8078/ALG227+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP8078/ALG227+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 8174
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.014 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(10, axiom,![X1]:(v1_xboole_0(X1)=>X1=k1_xboole_0),file('/tmp/SRASS.s.p', t6_boole)).
% fof(13, axiom,![X1]:![X2]:![X3]:((~(v1_xboole_0(X2))&m1_pboole(X3,X2))=>(r2_hidden(X1,a_2_0_closure3(X2,X3))<=>?[X4]:((m1_subset_1(X4,X2)&X1=X4)&~(k1_funct_1(X3,X4)=k1_xboole_0)))),file('/tmp/SRASS.s.p', fraenkel_a_2_0_closure3)).
% fof(14, axiom,![X1]:(~(v1_xboole_0(X1))=>![X2]:(m1_pboole(X2,X1)=>![X3]:(X3=k1_closure3(X1,X2)<=>X3=a_2_0_closure3(X1,X2)))),file('/tmp/SRASS.s.p', d3_closure3)).
% fof(24, axiom,?[X1]:(((((v1_xboole_0(X1)&v1_relat_1(X1))&v1_funct_1(X1))&v2_funct_1(X1))&v1_finset_1(X1))&v1_fraenkel(X1)),file('/tmp/SRASS.s.p', rc1_closure2)).
% fof(29, conjecture,![X1]:(~(v1_xboole_0(X1))=>![X2]:(m1_pboole(X2,X1)=>![X3]:(m1_subset_1(X3,X1)=>(~(r2_hidden(X3,k1_closure3(X1,X2)))=>k1_funct_1(X2,X3)=k1_xboole_0)))),file('/tmp/SRASS.s.p', t8_closure3)).
% fof(30, negated_conjecture,~(![X1]:(~(v1_xboole_0(X1))=>![X2]:(m1_pboole(X2,X1)=>![X3]:(m1_subset_1(X3,X1)=>(~(r2_hidden(X3,k1_closure3(X1,X2)))=>k1_funct_1(X2,X3)=k1_xboole_0))))),inference(assume_negation,[status(cth)],[29])).
% fof(33, plain,![X1]:![X2]:![X3]:((~(v1_xboole_0(X2))&m1_pboole(X3,X2))=>(r2_hidden(X1,a_2_0_closure3(X2,X3))<=>?[X4]:((m1_subset_1(X4,X2)&X1=X4)&~(k1_funct_1(X3,X4)=k1_xboole_0)))),inference(fof_simplification,[status(thm)],[13,theory(equality)])).
% fof(34, plain,![X1]:(~(v1_xboole_0(X1))=>![X2]:(m1_pboole(X2,X1)=>![X3]:(X3=k1_closure3(X1,X2)<=>X3=a_2_0_closure3(X1,X2)))),inference(fof_simplification,[status(thm)],[14,theory(equality)])).
% fof(36, negated_conjecture,~(![X1]:(~(v1_xboole_0(X1))=>![X2]:(m1_pboole(X2,X1)=>![X3]:(m1_subset_1(X3,X1)=>(~(r2_hidden(X3,k1_closure3(X1,X2)))=>k1_funct_1(X2,X3)=k1_xboole_0))))),inference(fof_simplification,[status(thm)],[30,theory(equality)])).
% fof(65, plain,![X1]:(~(v1_xboole_0(X1))|X1=k1_xboole_0),inference(fof_nnf,[status(thm)],[10])).
% fof(66, plain,![X2]:(~(v1_xboole_0(X2))|X2=k1_xboole_0),inference(variable_rename,[status(thm)],[65])).
% cnf(67,plain,(X1=k1_xboole_0|~v1_xboole_0(X1)),inference(split_conjunct,[status(thm)],[66])).
% fof(74, plain,![X1]:![X2]:![X3]:((v1_xboole_0(X2)|~(m1_pboole(X3,X2)))|((~(r2_hidden(X1,a_2_0_closure3(X2,X3)))|?[X4]:((m1_subset_1(X4,X2)&X1=X4)&~(k1_funct_1(X3,X4)=k1_xboole_0)))&(![X4]:((~(m1_subset_1(X4,X2))|~(X1=X4))|k1_funct_1(X3,X4)=k1_xboole_0)|r2_hidden(X1,a_2_0_closure3(X2,X3))))),inference(fof_nnf,[status(thm)],[33])).
% fof(75, plain,![X5]:![X6]:![X7]:((v1_xboole_0(X6)|~(m1_pboole(X7,X6)))|((~(r2_hidden(X5,a_2_0_closure3(X6,X7)))|?[X8]:((m1_subset_1(X8,X6)&X5=X8)&~(k1_funct_1(X7,X8)=k1_xboole_0)))&(![X9]:((~(m1_subset_1(X9,X6))|~(X5=X9))|k1_funct_1(X7,X9)=k1_xboole_0)|r2_hidden(X5,a_2_0_closure3(X6,X7))))),inference(variable_rename,[status(thm)],[74])).
% fof(76, plain,![X5]:![X6]:![X7]:((v1_xboole_0(X6)|~(m1_pboole(X7,X6)))|((~(r2_hidden(X5,a_2_0_closure3(X6,X7)))|((m1_subset_1(esk6_3(X5,X6,X7),X6)&X5=esk6_3(X5,X6,X7))&~(k1_funct_1(X7,esk6_3(X5,X6,X7))=k1_xboole_0)))&(![X9]:((~(m1_subset_1(X9,X6))|~(X5=X9))|k1_funct_1(X7,X9)=k1_xboole_0)|r2_hidden(X5,a_2_0_closure3(X6,X7))))),inference(skolemize,[status(esa)],[75])).
% fof(77, plain,![X5]:![X6]:![X7]:![X9]:(((((~(m1_subset_1(X9,X6))|~(X5=X9))|k1_funct_1(X7,X9)=k1_xboole_0)|r2_hidden(X5,a_2_0_closure3(X6,X7)))&(~(r2_hidden(X5,a_2_0_closure3(X6,X7)))|((m1_subset_1(esk6_3(X5,X6,X7),X6)&X5=esk6_3(X5,X6,X7))&~(k1_funct_1(X7,esk6_3(X5,X6,X7))=k1_xboole_0))))|(v1_xboole_0(X6)|~(m1_pboole(X7,X6)))),inference(shift_quantors,[status(thm)],[76])).
% fof(78, plain,![X5]:![X6]:![X7]:![X9]:(((((~(m1_subset_1(X9,X6))|~(X5=X9))|k1_funct_1(X7,X9)=k1_xboole_0)|r2_hidden(X5,a_2_0_closure3(X6,X7)))|(v1_xboole_0(X6)|~(m1_pboole(X7,X6))))&((((m1_subset_1(esk6_3(X5,X6,X7),X6)|~(r2_hidden(X5,a_2_0_closure3(X6,X7))))|(v1_xboole_0(X6)|~(m1_pboole(X7,X6))))&((X5=esk6_3(X5,X6,X7)|~(r2_hidden(X5,a_2_0_closure3(X6,X7))))|(v1_xboole_0(X6)|~(m1_pboole(X7,X6)))))&((~(k1_funct_1(X7,esk6_3(X5,X6,X7))=k1_xboole_0)|~(r2_hidden(X5,a_2_0_closure3(X6,X7))))|(v1_xboole_0(X6)|~(m1_pboole(X7,X6)))))),inference(distribute,[status(thm)],[77])).
% cnf(82,plain,(v1_xboole_0(X2)|r2_hidden(X3,a_2_0_closure3(X2,X1))|k1_funct_1(X1,X4)=k1_xboole_0|~m1_pboole(X1,X2)|X3!=X4|~m1_subset_1(X4,X2)),inference(split_conjunct,[status(thm)],[78])).
% fof(83, plain,![X1]:(v1_xboole_0(X1)|![X2]:(~(m1_pboole(X2,X1))|![X3]:((~(X3=k1_closure3(X1,X2))|X3=a_2_0_closure3(X1,X2))&(~(X3=a_2_0_closure3(X1,X2))|X3=k1_closure3(X1,X2))))),inference(fof_nnf,[status(thm)],[34])).
% fof(84, plain,![X4]:(v1_xboole_0(X4)|![X5]:(~(m1_pboole(X5,X4))|![X6]:((~(X6=k1_closure3(X4,X5))|X6=a_2_0_closure3(X4,X5))&(~(X6=a_2_0_closure3(X4,X5))|X6=k1_closure3(X4,X5))))),inference(variable_rename,[status(thm)],[83])).
% fof(85, plain,![X4]:![X5]:![X6]:((((~(X6=k1_closure3(X4,X5))|X6=a_2_0_closure3(X4,X5))&(~(X6=a_2_0_closure3(X4,X5))|X6=k1_closure3(X4,X5)))|~(m1_pboole(X5,X4)))|v1_xboole_0(X4)),inference(shift_quantors,[status(thm)],[84])).
% fof(86, plain,![X4]:![X5]:![X6]:((((~(X6=k1_closure3(X4,X5))|X6=a_2_0_closure3(X4,X5))|~(m1_pboole(X5,X4)))|v1_xboole_0(X4))&(((~(X6=a_2_0_closure3(X4,X5))|X6=k1_closure3(X4,X5))|~(m1_pboole(X5,X4)))|v1_xboole_0(X4))),inference(distribute,[status(thm)],[85])).
% cnf(88,plain,(v1_xboole_0(X1)|X3=a_2_0_closure3(X1,X2)|~m1_pboole(X2,X1)|X3!=k1_closure3(X1,X2)),inference(split_conjunct,[status(thm)],[86])).
% fof(127, plain,?[X2]:(((((v1_xboole_0(X2)&v1_relat_1(X2))&v1_funct_1(X2))&v2_funct_1(X2))&v1_finset_1(X2))&v1_fraenkel(X2)),inference(variable_rename,[status(thm)],[24])).
% fof(128, plain,(((((v1_xboole_0(esk11_0)&v1_relat_1(esk11_0))&v1_funct_1(esk11_0))&v2_funct_1(esk11_0))&v1_finset_1(esk11_0))&v1_fraenkel(esk11_0)),inference(skolemize,[status(esa)],[127])).
% cnf(134,plain,(v1_xboole_0(esk11_0)),inference(split_conjunct,[status(thm)],[128])).
% fof(139, negated_conjecture,?[X1]:(~(v1_xboole_0(X1))&?[X2]:(m1_pboole(X2,X1)&?[X3]:(m1_subset_1(X3,X1)&(~(r2_hidden(X3,k1_closure3(X1,X2)))&~(k1_funct_1(X2,X3)=k1_xboole_0))))),inference(fof_nnf,[status(thm)],[36])).
% fof(140, negated_conjecture,?[X4]:(~(v1_xboole_0(X4))&?[X5]:(m1_pboole(X5,X4)&?[X6]:(m1_subset_1(X6,X4)&(~(r2_hidden(X6,k1_closure3(X4,X5)))&~(k1_funct_1(X5,X6)=k1_xboole_0))))),inference(variable_rename,[status(thm)],[139])).
% fof(141, negated_conjecture,(~(v1_xboole_0(esk12_0))&(m1_pboole(esk13_0,esk12_0)&(m1_subset_1(esk14_0,esk12_0)&(~(r2_hidden(esk14_0,k1_closure3(esk12_0,esk13_0)))&~(k1_funct_1(esk13_0,esk14_0)=k1_xboole_0))))),inference(skolemize,[status(esa)],[140])).
% cnf(142,negated_conjecture,(k1_funct_1(esk13_0,esk14_0)!=k1_xboole_0),inference(split_conjunct,[status(thm)],[141])).
% cnf(143,negated_conjecture,(~r2_hidden(esk14_0,k1_closure3(esk12_0,esk13_0))),inference(split_conjunct,[status(thm)],[141])).
% cnf(144,negated_conjecture,(m1_subset_1(esk14_0,esk12_0)),inference(split_conjunct,[status(thm)],[141])).
% cnf(145,negated_conjecture,(m1_pboole(esk13_0,esk12_0)),inference(split_conjunct,[status(thm)],[141])).
% cnf(146,negated_conjecture,(~v1_xboole_0(esk12_0)),inference(split_conjunct,[status(thm)],[141])).
% cnf(148,plain,(k1_funct_1(X1,X2)=k1_xboole_0|v1_xboole_0(X3)|r2_hidden(X2,a_2_0_closure3(X3,X1))|~m1_subset_1(X2,X3)|~m1_pboole(X1,X3)),inference(er,[status(thm)],[82,theory(equality)])).
% cnf(149,plain,(k1_xboole_0=esk11_0),inference(spm,[status(thm)],[67,134,theory(equality)])).
% cnf(164,plain,(a_2_0_closure3(X1,X2)=k1_closure3(X1,X2)|v1_xboole_0(X1)|~m1_pboole(X2,X1)),inference(er,[status(thm)],[88,theory(equality)])).
% cnf(184,negated_conjecture,(k1_funct_1(esk13_0,esk14_0)!=esk11_0),inference(rw,[status(thm)],[142,149,theory(equality)])).
% cnf(186,plain,(k1_funct_1(X1,X2)=esk11_0|v1_xboole_0(X3)|r2_hidden(X2,a_2_0_closure3(X3,X1))|~m1_subset_1(X2,X3)|~m1_pboole(X1,X3)),inference(rw,[status(thm)],[148,149,theory(equality)])).
% cnf(198,negated_conjecture,(k1_funct_1(X1,esk14_0)=esk11_0|v1_xboole_0(esk12_0)|r2_hidden(esk14_0,a_2_0_closure3(esk12_0,X1))|~m1_pboole(X1,esk12_0)),inference(spm,[status(thm)],[186,144,theory(equality)])).
% cnf(202,negated_conjecture,(k1_funct_1(X1,esk14_0)=esk11_0|r2_hidden(esk14_0,a_2_0_closure3(esk12_0,X1))|~m1_pboole(X1,esk12_0)),inference(sr,[status(thm)],[198,146,theory(equality)])).
% cnf(208,negated_conjecture,(v1_xboole_0(esk12_0)|~r2_hidden(esk14_0,a_2_0_closure3(esk12_0,esk13_0))|~m1_pboole(esk13_0,esk12_0)),inference(spm,[status(thm)],[143,164,theory(equality)])).
% cnf(210,negated_conjecture,(v1_xboole_0(esk12_0)|~r2_hidden(esk14_0,a_2_0_closure3(esk12_0,esk13_0))|$false),inference(rw,[status(thm)],[208,145,theory(equality)])).
% cnf(211,negated_conjecture,(v1_xboole_0(esk12_0)|~r2_hidden(esk14_0,a_2_0_closure3(esk12_0,esk13_0))),inference(cn,[status(thm)],[210,theory(equality)])).
% cnf(212,negated_conjecture,(~r2_hidden(esk14_0,a_2_0_closure3(esk12_0,esk13_0))),inference(sr,[status(thm)],[211,146,theory(equality)])).
% cnf(213,negated_conjecture,(r2_hidden(esk14_0,a_2_0_closure3(esk12_0,esk13_0))|~m1_pboole(esk13_0,esk12_0)),inference(spm,[status(thm)],[184,202,theory(equality)])).
% cnf(214,negated_conjecture,(r2_hidden(esk14_0,a_2_0_closure3(esk12_0,esk13_0))|$false),inference(rw,[status(thm)],[213,145,theory(equality)])).
% cnf(215,negated_conjecture,(r2_hidden(esk14_0,a_2_0_closure3(esk12_0,esk13_0))),inference(cn,[status(thm)],[214,theory(equality)])).
% cnf(216,negated_conjecture,($false),inference(sr,[status(thm)],[215,212,theory(equality)])).
% cnf(217,negated_conjecture,($false),216,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 120
% # ...of these trivial : 0
% # ...subsumed : 5
% # ...remaining for further processing: 115
% # Other redundant clauses eliminated : 1
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 9
% # Generated clauses : 50
% # ...of the previous two non-trivial : 47
% # Contextual simplify-reflections : 2
% # Paramodulations : 45
% # Factorizations : 2
% # Equation resolutions : 3
% # Current number of processed clauses: 59
% # Positive orientable unit clauses: 24
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 7
% # Non-unit-clauses : 28
% # Current number of unprocessed clauses: 9
% # ...number of literals in the above : 36
% # Clause-clause subsumption calls (NU) : 67
% # Rec. Clause-clause subsumption calls : 66
% # Unit Clause-clause subsumption calls : 1
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 3
% # Indexed BW rewrite successes : 3
% # Backwards rewriting index: 69 leaves, 1.28+/-0.796 terms/leaf
% # Paramod-from index: 35 leaves, 1.03+/-0.167 terms/leaf
% # Paramod-into index: 62 leaves, 1.13+/-0.421 terms/leaf
% # -------------------------------------------------
% # User time : 0.017 s
% # System time : 0.004 s
% # Total time : 0.021 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.10 CPU 0.18 WC
% FINAL PrfWatch: 0.10 CPU 0.18 WC
% SZS output end Solution for /tmp/SystemOnTPTP8078/ALG227+1.tptp
%
%------------------------------------------------------------------------------