%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU413+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 : 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 05:14:53 EST 2010
% Result : Theorem 1.87s
% Output : Solution 1.87s
% 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/SystemOnTPTP916/SEU413+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP916/SEU413+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP916/SEU413+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 1012
% 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(6, axiom,![X1]:(l1_orders_2(X1)=>![X2]:(l1_orders_2(X2)=>![X3]:![X4]:((((v12_waybel_0(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),X2)&m1_subset_1(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),k1_zfmisc_1(u1_struct_0(X2))))&r2_hidden(k4_tarski(X3,X4),u1_orders_2(k1_latsum_1(X1,X2))))&r2_hidden(X4,u1_struct_0(X1)))=>r2_hidden(X3,u1_struct_0(X1))))),file('/tmp/SRASS.s.p', t21_latsum_1)).
% fof(8, axiom,![X1]:(l1_orders_2(X1)=>![X2]:(m1_subset_1(X2,u1_struct_0(X1))=>![X3]:(m1_subset_1(X3,u1_struct_0(X1))=>(r1_orders_2(X1,X2,X3)<=>r2_hidden(k4_tarski(X2,X3),u1_orders_2(X1)))))),file('/tmp/SRASS.s.p', d9_orders_2)).
% fof(10, axiom,![X1]:![X2]:((l1_orders_2(X1)&l1_orders_2(X2))=>(v1_orders_2(k1_latsum_1(X1,X2))&l1_orders_2(k1_latsum_1(X1,X2)))),file('/tmp/SRASS.s.p', dt_k1_latsum_1)).
% fof(42, conjecture,![X1]:(l1_orders_2(X1)=>![X2]:(l1_orders_2(X2)=>![X3]:(m1_subset_1(X3,u1_struct_0(k1_latsum_1(X1,X2)))=>![X4]:(m1_subset_1(X4,u1_struct_0(k1_latsum_1(X1,X2)))=>((((v12_waybel_0(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),X2)&m1_subset_1(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),k1_zfmisc_1(u1_struct_0(X2))))&r1_orders_2(k1_latsum_1(X1,X2),X3,X4))&r2_hidden(X4,u1_struct_0(X1)))=>r2_hidden(X3,u1_struct_0(X1))))))),file('/tmp/SRASS.s.p', t23_latsum_1)).
% fof(43, negated_conjecture,~(![X1]:(l1_orders_2(X1)=>![X2]:(l1_orders_2(X2)=>![X3]:(m1_subset_1(X3,u1_struct_0(k1_latsum_1(X1,X2)))=>![X4]:(m1_subset_1(X4,u1_struct_0(k1_latsum_1(X1,X2)))=>((((v12_waybel_0(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),X2)&m1_subset_1(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),k1_zfmisc_1(u1_struct_0(X2))))&r1_orders_2(k1_latsum_1(X1,X2),X3,X4))&r2_hidden(X4,u1_struct_0(X1)))=>r2_hidden(X3,u1_struct_0(X1)))))))),inference(assume_negation,[status(cth)],[42])).
% fof(61, plain,![X1]:(~(l1_orders_2(X1))|![X2]:(~(l1_orders_2(X2))|![X3]:![X4]:((((~(v12_waybel_0(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),X2))|~(m1_subset_1(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),k1_zfmisc_1(u1_struct_0(X2)))))|~(r2_hidden(k4_tarski(X3,X4),u1_orders_2(k1_latsum_1(X1,X2)))))|~(r2_hidden(X4,u1_struct_0(X1))))|r2_hidden(X3,u1_struct_0(X1))))),inference(fof_nnf,[status(thm)],[6])).
% fof(62, plain,![X5]:(~(l1_orders_2(X5))|![X6]:(~(l1_orders_2(X6))|![X7]:![X8]:((((~(v12_waybel_0(k3_xboole_0(u1_struct_0(X5),u1_struct_0(X6)),X6))|~(m1_subset_1(k3_xboole_0(u1_struct_0(X5),u1_struct_0(X6)),k1_zfmisc_1(u1_struct_0(X6)))))|~(r2_hidden(k4_tarski(X7,X8),u1_orders_2(k1_latsum_1(X5,X6)))))|~(r2_hidden(X8,u1_struct_0(X5))))|r2_hidden(X7,u1_struct_0(X5))))),inference(variable_rename,[status(thm)],[61])).
% fof(63, plain,![X5]:![X6]:![X7]:![X8]:((((((~(v12_waybel_0(k3_xboole_0(u1_struct_0(X5),u1_struct_0(X6)),X6))|~(m1_subset_1(k3_xboole_0(u1_struct_0(X5),u1_struct_0(X6)),k1_zfmisc_1(u1_struct_0(X6)))))|~(r2_hidden(k4_tarski(X7,X8),u1_orders_2(k1_latsum_1(X5,X6)))))|~(r2_hidden(X8,u1_struct_0(X5))))|r2_hidden(X7,u1_struct_0(X5)))|~(l1_orders_2(X6)))|~(l1_orders_2(X5))),inference(shift_quantors,[status(thm)],[62])).
% cnf(64,plain,(r2_hidden(X3,u1_struct_0(X1))|~l1_orders_2(X1)|~l1_orders_2(X2)|~r2_hidden(X4,u1_struct_0(X1))|~r2_hidden(k4_tarski(X3,X4),u1_orders_2(k1_latsum_1(X1,X2)))|~m1_subset_1(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),k1_zfmisc_1(u1_struct_0(X2)))|~v12_waybel_0(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),X2)),inference(split_conjunct,[status(thm)],[63])).
% fof(68, plain,![X1]:(~(l1_orders_2(X1))|![X2]:(~(m1_subset_1(X2,u1_struct_0(X1)))|![X3]:(~(m1_subset_1(X3,u1_struct_0(X1)))|((~(r1_orders_2(X1,X2,X3))|r2_hidden(k4_tarski(X2,X3),u1_orders_2(X1)))&(~(r2_hidden(k4_tarski(X2,X3),u1_orders_2(X1)))|r1_orders_2(X1,X2,X3)))))),inference(fof_nnf,[status(thm)],[8])).
% fof(69, plain,![X4]:(~(l1_orders_2(X4))|![X5]:(~(m1_subset_1(X5,u1_struct_0(X4)))|![X6]:(~(m1_subset_1(X6,u1_struct_0(X4)))|((~(r1_orders_2(X4,X5,X6))|r2_hidden(k4_tarski(X5,X6),u1_orders_2(X4)))&(~(r2_hidden(k4_tarski(X5,X6),u1_orders_2(X4)))|r1_orders_2(X4,X5,X6)))))),inference(variable_rename,[status(thm)],[68])).
% fof(70, plain,![X4]:![X5]:![X6]:(((~(m1_subset_1(X6,u1_struct_0(X4)))|((~(r1_orders_2(X4,X5,X6))|r2_hidden(k4_tarski(X5,X6),u1_orders_2(X4)))&(~(r2_hidden(k4_tarski(X5,X6),u1_orders_2(X4)))|r1_orders_2(X4,X5,X6))))|~(m1_subset_1(X5,u1_struct_0(X4))))|~(l1_orders_2(X4))),inference(shift_quantors,[status(thm)],[69])).
% fof(71, plain,![X4]:![X5]:![X6]:(((((~(r1_orders_2(X4,X5,X6))|r2_hidden(k4_tarski(X5,X6),u1_orders_2(X4)))|~(m1_subset_1(X6,u1_struct_0(X4))))|~(m1_subset_1(X5,u1_struct_0(X4))))|~(l1_orders_2(X4)))&((((~(r2_hidden(k4_tarski(X5,X6),u1_orders_2(X4)))|r1_orders_2(X4,X5,X6))|~(m1_subset_1(X6,u1_struct_0(X4))))|~(m1_subset_1(X5,u1_struct_0(X4))))|~(l1_orders_2(X4)))),inference(distribute,[status(thm)],[70])).
% cnf(73,plain,(r2_hidden(k4_tarski(X2,X3),u1_orders_2(X1))|~l1_orders_2(X1)|~m1_subset_1(X2,u1_struct_0(X1))|~m1_subset_1(X3,u1_struct_0(X1))|~r1_orders_2(X1,X2,X3)),inference(split_conjunct,[status(thm)],[71])).
% fof(77, plain,![X1]:![X2]:((~(l1_orders_2(X1))|~(l1_orders_2(X2)))|(v1_orders_2(k1_latsum_1(X1,X2))&l1_orders_2(k1_latsum_1(X1,X2)))),inference(fof_nnf,[status(thm)],[10])).
% fof(78, plain,![X3]:![X4]:((~(l1_orders_2(X3))|~(l1_orders_2(X4)))|(v1_orders_2(k1_latsum_1(X3,X4))&l1_orders_2(k1_latsum_1(X3,X4)))),inference(variable_rename,[status(thm)],[77])).
% fof(79, plain,![X3]:![X4]:((v1_orders_2(k1_latsum_1(X3,X4))|(~(l1_orders_2(X3))|~(l1_orders_2(X4))))&(l1_orders_2(k1_latsum_1(X3,X4))|(~(l1_orders_2(X3))|~(l1_orders_2(X4))))),inference(distribute,[status(thm)],[78])).
% cnf(80,plain,(l1_orders_2(k1_latsum_1(X2,X1))|~l1_orders_2(X1)|~l1_orders_2(X2)),inference(split_conjunct,[status(thm)],[79])).
% fof(158, negated_conjecture,?[X1]:(l1_orders_2(X1)&?[X2]:(l1_orders_2(X2)&?[X3]:(m1_subset_1(X3,u1_struct_0(k1_latsum_1(X1,X2)))&?[X4]:(m1_subset_1(X4,u1_struct_0(k1_latsum_1(X1,X2)))&((((v12_waybel_0(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),X2)&m1_subset_1(k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2)),k1_zfmisc_1(u1_struct_0(X2))))&r1_orders_2(k1_latsum_1(X1,X2),X3,X4))&r2_hidden(X4,u1_struct_0(X1)))&~(r2_hidden(X3,u1_struct_0(X1)))))))),inference(fof_nnf,[status(thm)],[43])).
% fof(159, negated_conjecture,?[X5]:(l1_orders_2(X5)&?[X6]:(l1_orders_2(X6)&?[X7]:(m1_subset_1(X7,u1_struct_0(k1_latsum_1(X5,X6)))&?[X8]:(m1_subset_1(X8,u1_struct_0(k1_latsum_1(X5,X6)))&((((v12_waybel_0(k3_xboole_0(u1_struct_0(X5),u1_struct_0(X6)),X6)&m1_subset_1(k3_xboole_0(u1_struct_0(X5),u1_struct_0(X6)),k1_zfmisc_1(u1_struct_0(X6))))&r1_orders_2(k1_latsum_1(X5,X6),X7,X8))&r2_hidden(X8,u1_struct_0(X5)))&~(r2_hidden(X7,u1_struct_0(X5)))))))),inference(variable_rename,[status(thm)],[158])).
% fof(160, negated_conjecture,(l1_orders_2(esk8_0)&(l1_orders_2(esk9_0)&(m1_subset_1(esk10_0,u1_struct_0(k1_latsum_1(esk8_0,esk9_0)))&(m1_subset_1(esk11_0,u1_struct_0(k1_latsum_1(esk8_0,esk9_0)))&((((v12_waybel_0(k3_xboole_0(u1_struct_0(esk8_0),u1_struct_0(esk9_0)),esk9_0)&m1_subset_1(k3_xboole_0(u1_struct_0(esk8_0),u1_struct_0(esk9_0)),k1_zfmisc_1(u1_struct_0(esk9_0))))&r1_orders_2(k1_latsum_1(esk8_0,esk9_0),esk10_0,esk11_0))&r2_hidden(esk11_0,u1_struct_0(esk8_0)))&~(r2_hidden(esk10_0,u1_struct_0(esk8_0)))))))),inference(skolemize,[status(esa)],[159])).
% cnf(161,negated_conjecture,(~r2_hidden(esk10_0,u1_struct_0(esk8_0))),inference(split_conjunct,[status(thm)],[160])).
% cnf(162,negated_conjecture,(r2_hidden(esk11_0,u1_struct_0(esk8_0))),inference(split_conjunct,[status(thm)],[160])).
% cnf(163,negated_conjecture,(r1_orders_2(k1_latsum_1(esk8_0,esk9_0),esk10_0,esk11_0)),inference(split_conjunct,[status(thm)],[160])).
% cnf(164,negated_conjecture,(m1_subset_1(k3_xboole_0(u1_struct_0(esk8_0),u1_struct_0(esk9_0)),k1_zfmisc_1(u1_struct_0(esk9_0)))),inference(split_conjunct,[status(thm)],[160])).
% cnf(165,negated_conjecture,(v12_waybel_0(k3_xboole_0(u1_struct_0(esk8_0),u1_struct_0(esk9_0)),esk9_0)),inference(split_conjunct,[status(thm)],[160])).
% cnf(166,negated_conjecture,(m1_subset_1(esk11_0,u1_struct_0(k1_latsum_1(esk8_0,esk9_0)))),inference(split_conjunct,[status(thm)],[160])).
% cnf(167,negated_conjecture,(m1_subset_1(esk10_0,u1_struct_0(k1_latsum_1(esk8_0,esk9_0)))),inference(split_conjunct,[status(thm)],[160])).
% cnf(168,negated_conjecture,(l1_orders_2(esk9_0)),inference(split_conjunct,[status(thm)],[160])).
% cnf(169,negated_conjecture,(l1_orders_2(esk8_0)),inference(split_conjunct,[status(thm)],[160])).
% cnf(184,negated_conjecture,(l1_orders_2(k1_latsum_1(esk8_0,X1))|~l1_orders_2(X1)),inference(pm,[status(thm)],[80,169,theory(equality)])).
% cnf(213,negated_conjecture,(r2_hidden(k4_tarski(X1,esk11_0),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~r1_orders_2(k1_latsum_1(esk8_0,esk9_0),X1,esk11_0)|~m1_subset_1(X1,u1_struct_0(k1_latsum_1(esk8_0,esk9_0)))|~l1_orders_2(k1_latsum_1(esk8_0,esk9_0))),inference(pm,[status(thm)],[73,166,theory(equality)])).
% cnf(219,negated_conjecture,(r2_hidden(X1,u1_struct_0(esk8_0))|~v12_waybel_0(k3_xboole_0(u1_struct_0(esk8_0),u1_struct_0(esk9_0)),esk9_0)|~l1_orders_2(esk9_0)|~l1_orders_2(esk8_0)|~r2_hidden(k4_tarski(X1,X2),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~r2_hidden(X2,u1_struct_0(esk8_0))),inference(pm,[status(thm)],[64,164,theory(equality)])).
% cnf(221,negated_conjecture,(r2_hidden(X1,u1_struct_0(esk8_0))|$false|~l1_orders_2(esk9_0)|~l1_orders_2(esk8_0)|~r2_hidden(k4_tarski(X1,X2),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~r2_hidden(X2,u1_struct_0(esk8_0))),inference(rw,[status(thm)],[219,165,theory(equality)])).
% cnf(222,negated_conjecture,(r2_hidden(X1,u1_struct_0(esk8_0))|$false|$false|~l1_orders_2(esk8_0)|~r2_hidden(k4_tarski(X1,X2),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~r2_hidden(X2,u1_struct_0(esk8_0))),inference(rw,[status(thm)],[221,168,theory(equality)])).
% cnf(223,negated_conjecture,(r2_hidden(X1,u1_struct_0(esk8_0))|$false|$false|$false|~r2_hidden(k4_tarski(X1,X2),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~r2_hidden(X2,u1_struct_0(esk8_0))),inference(rw,[status(thm)],[222,169,theory(equality)])).
% cnf(224,negated_conjecture,(r2_hidden(X1,u1_struct_0(esk8_0))|~r2_hidden(k4_tarski(X1,X2),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~r2_hidden(X2,u1_struct_0(esk8_0))),inference(cn,[status(thm)],[223,theory(equality)])).
% cnf(242,negated_conjecture,(l1_orders_2(k1_latsum_1(esk8_0,esk9_0))),inference(pm,[status(thm)],[184,168,theory(equality)])).
% cnf(1220,negated_conjecture,(r2_hidden(k4_tarski(X1,esk11_0),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~r1_orders_2(k1_latsum_1(esk8_0,esk9_0),X1,esk11_0)|~m1_subset_1(X1,u1_struct_0(k1_latsum_1(esk8_0,esk9_0)))|$false),inference(rw,[status(thm)],[213,242,theory(equality)])).
% cnf(1221,negated_conjecture,(r2_hidden(k4_tarski(X1,esk11_0),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~r1_orders_2(k1_latsum_1(esk8_0,esk9_0),X1,esk11_0)|~m1_subset_1(X1,u1_struct_0(k1_latsum_1(esk8_0,esk9_0)))),inference(cn,[status(thm)],[1220,theory(equality)])).
% cnf(1222,negated_conjecture,(r2_hidden(k4_tarski(esk10_0,esk11_0),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|~m1_subset_1(esk10_0,u1_struct_0(k1_latsum_1(esk8_0,esk9_0)))),inference(pm,[status(thm)],[1221,163,theory(equality)])).
% cnf(1223,negated_conjecture,(r2_hidden(k4_tarski(esk10_0,esk11_0),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))|$false),inference(rw,[status(thm)],[1222,167,theory(equality)])).
% cnf(1224,negated_conjecture,(r2_hidden(k4_tarski(esk10_0,esk11_0),u1_orders_2(k1_latsum_1(esk8_0,esk9_0)))),inference(cn,[status(thm)],[1223,theory(equality)])).
% cnf(35854,negated_conjecture,(r2_hidden(esk10_0,u1_struct_0(esk8_0))|~r2_hidden(esk11_0,u1_struct_0(esk8_0))),inference(pm,[status(thm)],[224,1224,theory(equality)])).
% cnf(35860,negated_conjecture,(r2_hidden(esk10_0,u1_struct_0(esk8_0))|$false),inference(rw,[status(thm)],[35854,162,theory(equality)])).
% cnf(35861,negated_conjecture,(r2_hidden(esk10_0,u1_struct_0(esk8_0))),inference(cn,[status(thm)],[35860,theory(equality)])).
% cnf(35862,negated_conjecture,($false),inference(sr,[status(thm)],[35861,161,theory(equality)])).
% cnf(35863,negated_conjecture,($false),35862,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 1277
% # ...of these trivial : 1
% # ...subsumed : 320
% # ...remaining for further processing: 956
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 22
% # Backward-rewritten : 2
% # Generated clauses : 34995
% # ...of the previous two non-trivial : 34772
% # Contextual simplify-reflections : 0
% # Paramodulations : 34989
% # Factorizations : 2
% # Equation resolutions : 4
% # Current number of processed clauses: 932
% # Positive orientable unit clauses: 585
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 5
% # Non-unit-clauses : 341
% # Current number of unprocessed clauses: 33472
% # ...number of literals in the above : 35016
% # Clause-clause subsumption calls (NU) : 5113
% # Rec. Clause-clause subsumption calls : 4468
% # Unit Clause-clause subsumption calls : 2635
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 12373
% # Indexed BW rewrite successes : 6
% # Backwards rewriting index: 492 leaves, 2.63+/-8.020 terms/leaf
% # Paramod-from index: 145 leaves, 4.46+/-12.510 terms/leaf
% # Paramod-into index: 433 leaves, 2.34+/-7.427 terms/leaf
% # -------------------------------------------------
% # User time : 0.495 s
% # System time : 0.030 s
% # Total time : 0.525 s
% # Maximum resident set size: 0 pages
% PrfWatch: 1.03 CPU 1.11 WC
% FINAL PrfWatch: 1.03 CPU 1.11 WC
% SZS output end Solution for /tmp/SystemOnTPTP916/SEU413+1.tptp
%
%------------------------------------------------------------------------------