%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL454+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 : art02.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 : Wed Dec 29 13:24:50 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/SystemOnTPTP309/LCL454+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP309/LCL454+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP309/LCL454+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 406
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.018 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,(r1<=>![X1]:is_a_theorem(implies(or(X1,X1),X1))),file('/tmp/SRASS.s.p', r1)).
% fof(2, axiom,modus_ponens,file('/tmp/SRASS.s.p', hilbert_modus_ponens)).
% fof(4, axiom,implies_1,file('/tmp/SRASS.s.p', hilbert_implies_1)).
% fof(5, axiom,implies_2,file('/tmp/SRASS.s.p', hilbert_implies_2)).
% fof(12, axiom,or_3,file('/tmp/SRASS.s.p', hilbert_or_3)).
% fof(16, axiom,op_implies_or,file('/tmp/SRASS.s.p', principia_op_implies_or)).
% fof(19, axiom,(or_3<=>![X2]:![X3]:![X4]:is_a_theorem(implies(implies(X2,X4),implies(implies(X3,X4),implies(or(X2,X3),X4))))),file('/tmp/SRASS.s.p', or_3)).
% fof(24, axiom,(modus_ponens<=>![X2]:![X3]:((is_a_theorem(X2)&is_a_theorem(implies(X2,X3)))=>is_a_theorem(X3))),file('/tmp/SRASS.s.p', modus_ponens)).
% fof(25, axiom,(implies_1<=>![X2]:![X3]:is_a_theorem(implies(X2,implies(X3,X2)))),file('/tmp/SRASS.s.p', implies_1)).
% fof(26, axiom,(implies_2<=>![X2]:![X3]:is_a_theorem(implies(implies(X2,implies(X2,X3)),implies(X2,X3)))),file('/tmp/SRASS.s.p', implies_2)).
% fof(29, axiom,op_or,file('/tmp/SRASS.s.p', hilbert_op_or)).
% fof(30, axiom,op_implies_and,file('/tmp/SRASS.s.p', hilbert_op_implies_and)).
% fof(33, axiom,op_and,file('/tmp/SRASS.s.p', principia_op_and)).
% fof(35, axiom,(op_or=>![X2]:![X3]:or(X2,X3)=not(and(not(X2),not(X3)))),file('/tmp/SRASS.s.p', op_or)).
% fof(36, axiom,(op_and=>![X2]:![X3]:and(X2,X3)=not(or(not(X2),not(X3)))),file('/tmp/SRASS.s.p', op_and)).
% fof(48, axiom,(op_implies_or=>![X2]:![X3]:implies(X2,X3)=or(not(X2),X3)),file('/tmp/SRASS.s.p', op_implies_or)).
% fof(51, axiom,(op_implies_and=>![X2]:![X3]:implies(X2,X3)=not(and(X2,not(X3)))),file('/tmp/SRASS.s.p', op_implies_and)).
% fof(53, conjecture,r1,file('/tmp/SRASS.s.p', principia_r1)).
% fof(54, negated_conjecture,~(r1),inference(assume_negation,[status(cth)],[53])).
% fof(55, negated_conjecture,~(r1),inference(fof_simplification,[status(thm)],[54,theory(equality)])).
% fof(56, plain,((~(r1)|![X1]:is_a_theorem(implies(or(X1,X1),X1)))&(?[X1]:~(is_a_theorem(implies(or(X1,X1),X1)))|r1)),inference(fof_nnf,[status(thm)],[1])).
% fof(57, plain,((~(r1)|![X2]:is_a_theorem(implies(or(X2,X2),X2)))&(?[X3]:~(is_a_theorem(implies(or(X3,X3),X3)))|r1)),inference(variable_rename,[status(thm)],[56])).
% fof(58, plain,((~(r1)|![X2]:is_a_theorem(implies(or(X2,X2),X2)))&(~(is_a_theorem(implies(or(esk1_0,esk1_0),esk1_0)))|r1)),inference(skolemize,[status(esa)],[57])).
% fof(59, plain,![X2]:((is_a_theorem(implies(or(X2,X2),X2))|~(r1))&(~(is_a_theorem(implies(or(esk1_0,esk1_0),esk1_0)))|r1)),inference(shift_quantors,[status(thm)],[58])).
% cnf(60,plain,(r1|~is_a_theorem(implies(or(esk1_0,esk1_0),esk1_0))),inference(split_conjunct,[status(thm)],[59])).
% cnf(62,plain,(modus_ponens),inference(split_conjunct,[status(thm)],[2])).
% cnf(64,plain,(implies_1),inference(split_conjunct,[status(thm)],[4])).
% cnf(65,plain,(implies_2),inference(split_conjunct,[status(thm)],[5])).
% cnf(72,plain,(or_3),inference(split_conjunct,[status(thm)],[12])).
% cnf(76,plain,(op_implies_or),inference(split_conjunct,[status(thm)],[16])).
% fof(89, plain,((~(or_3)|![X2]:![X3]:![X4]:is_a_theorem(implies(implies(X2,X4),implies(implies(X3,X4),implies(or(X2,X3),X4)))))&(?[X2]:?[X3]:?[X4]:~(is_a_theorem(implies(implies(X2,X4),implies(implies(X3,X4),implies(or(X2,X3),X4)))))|or_3)),inference(fof_nnf,[status(thm)],[19])).
% fof(90, plain,((~(or_3)|![X5]:![X6]:![X7]:is_a_theorem(implies(implies(X5,X7),implies(implies(X6,X7),implies(or(X5,X6),X7)))))&(?[X8]:?[X9]:?[X10]:~(is_a_theorem(implies(implies(X8,X10),implies(implies(X9,X10),implies(or(X8,X9),X10)))))|or_3)),inference(variable_rename,[status(thm)],[89])).
% fof(91, plain,((~(or_3)|![X5]:![X6]:![X7]:is_a_theorem(implies(implies(X5,X7),implies(implies(X6,X7),implies(or(X5,X6),X7)))))&(~(is_a_theorem(implies(implies(esk6_0,esk8_0),implies(implies(esk7_0,esk8_0),implies(or(esk6_0,esk7_0),esk8_0)))))|or_3)),inference(skolemize,[status(esa)],[90])).
% fof(92, plain,![X5]:![X6]:![X7]:((is_a_theorem(implies(implies(X5,X7),implies(implies(X6,X7),implies(or(X5,X6),X7))))|~(or_3))&(~(is_a_theorem(implies(implies(esk6_0,esk8_0),implies(implies(esk7_0,esk8_0),implies(or(esk6_0,esk7_0),esk8_0)))))|or_3)),inference(shift_quantors,[status(thm)],[91])).
% cnf(94,plain,(is_a_theorem(implies(implies(X1,X2),implies(implies(X3,X2),implies(or(X1,X3),X2))))|~or_3),inference(split_conjunct,[status(thm)],[92])).
% fof(119, plain,((~(modus_ponens)|![X2]:![X3]:((~(is_a_theorem(X2))|~(is_a_theorem(implies(X2,X3))))|is_a_theorem(X3)))&(?[X2]:?[X3]:((is_a_theorem(X2)&is_a_theorem(implies(X2,X3)))&~(is_a_theorem(X3)))|modus_ponens)),inference(fof_nnf,[status(thm)],[24])).
% fof(120, plain,((~(modus_ponens)|![X4]:![X5]:((~(is_a_theorem(X4))|~(is_a_theorem(implies(X4,X5))))|is_a_theorem(X5)))&(?[X6]:?[X7]:((is_a_theorem(X6)&is_a_theorem(implies(X6,X7)))&~(is_a_theorem(X7)))|modus_ponens)),inference(variable_rename,[status(thm)],[119])).
% fof(121, plain,((~(modus_ponens)|![X4]:![X5]:((~(is_a_theorem(X4))|~(is_a_theorem(implies(X4,X5))))|is_a_theorem(X5)))&(((is_a_theorem(esk19_0)&is_a_theorem(implies(esk19_0,esk20_0)))&~(is_a_theorem(esk20_0)))|modus_ponens)),inference(skolemize,[status(esa)],[120])).
% fof(122, plain,![X4]:![X5]:((((~(is_a_theorem(X4))|~(is_a_theorem(implies(X4,X5))))|is_a_theorem(X5))|~(modus_ponens))&(((is_a_theorem(esk19_0)&is_a_theorem(implies(esk19_0,esk20_0)))&~(is_a_theorem(esk20_0)))|modus_ponens)),inference(shift_quantors,[status(thm)],[121])).
% fof(123, plain,![X4]:![X5]:((((~(is_a_theorem(X4))|~(is_a_theorem(implies(X4,X5))))|is_a_theorem(X5))|~(modus_ponens))&(((is_a_theorem(esk19_0)|modus_ponens)&(is_a_theorem(implies(esk19_0,esk20_0))|modus_ponens))&(~(is_a_theorem(esk20_0))|modus_ponens))),inference(distribute,[status(thm)],[122])).
% cnf(127,plain,(is_a_theorem(X1)|~modus_ponens|~is_a_theorem(implies(X2,X1))|~is_a_theorem(X2)),inference(split_conjunct,[status(thm)],[123])).
% fof(128, plain,((~(implies_1)|![X2]:![X3]:is_a_theorem(implies(X2,implies(X3,X2))))&(?[X2]:?[X3]:~(is_a_theorem(implies(X2,implies(X3,X2))))|implies_1)),inference(fof_nnf,[status(thm)],[25])).
% fof(129, plain,((~(implies_1)|![X4]:![X5]:is_a_theorem(implies(X4,implies(X5,X4))))&(?[X6]:?[X7]:~(is_a_theorem(implies(X6,implies(X7,X6))))|implies_1)),inference(variable_rename,[status(thm)],[128])).
% fof(130, plain,((~(implies_1)|![X4]:![X5]:is_a_theorem(implies(X4,implies(X5,X4))))&(~(is_a_theorem(implies(esk21_0,implies(esk22_0,esk21_0))))|implies_1)),inference(skolemize,[status(esa)],[129])).
% fof(131, plain,![X4]:![X5]:((is_a_theorem(implies(X4,implies(X5,X4)))|~(implies_1))&(~(is_a_theorem(implies(esk21_0,implies(esk22_0,esk21_0))))|implies_1)),inference(shift_quantors,[status(thm)],[130])).
% cnf(133,plain,(is_a_theorem(implies(X1,implies(X2,X1)))|~implies_1),inference(split_conjunct,[status(thm)],[131])).
% fof(134, plain,((~(implies_2)|![X2]:![X3]:is_a_theorem(implies(implies(X2,implies(X2,X3)),implies(X2,X3))))&(?[X2]:?[X3]:~(is_a_theorem(implies(implies(X2,implies(X2,X3)),implies(X2,X3))))|implies_2)),inference(fof_nnf,[status(thm)],[26])).
% fof(135, plain,((~(implies_2)|![X4]:![X5]:is_a_theorem(implies(implies(X4,implies(X4,X5)),implies(X4,X5))))&(?[X6]:?[X7]:~(is_a_theorem(implies(implies(X6,implies(X6,X7)),implies(X6,X7))))|implies_2)),inference(variable_rename,[status(thm)],[134])).
% fof(136, plain,((~(implies_2)|![X4]:![X5]:is_a_theorem(implies(implies(X4,implies(X4,X5)),implies(X4,X5))))&(~(is_a_theorem(implies(implies(esk23_0,implies(esk23_0,esk24_0)),implies(esk23_0,esk24_0))))|implies_2)),inference(skolemize,[status(esa)],[135])).
% fof(137, plain,![X4]:![X5]:((is_a_theorem(implies(implies(X4,implies(X4,X5)),implies(X4,X5)))|~(implies_2))&(~(is_a_theorem(implies(implies(esk23_0,implies(esk23_0,esk24_0)),implies(esk23_0,esk24_0))))|implies_2)),inference(shift_quantors,[status(thm)],[136])).
% cnf(139,plain,(is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2)))|~implies_2),inference(split_conjunct,[status(thm)],[137])).
% cnf(152,plain,(op_or),inference(split_conjunct,[status(thm)],[29])).
% cnf(153,plain,(op_implies_and),inference(split_conjunct,[status(thm)],[30])).
% cnf(156,plain,(op_and),inference(split_conjunct,[status(thm)],[33])).
% fof(158, plain,(~(op_or)|![X2]:![X3]:or(X2,X3)=not(and(not(X2),not(X3)))),inference(fof_nnf,[status(thm)],[35])).
% fof(159, plain,(~(op_or)|![X4]:![X5]:or(X4,X5)=not(and(not(X4),not(X5)))),inference(variable_rename,[status(thm)],[158])).
% fof(160, plain,![X4]:![X5]:(or(X4,X5)=not(and(not(X4),not(X5)))|~(op_or)),inference(shift_quantors,[status(thm)],[159])).
% cnf(161,plain,(or(X1,X2)=not(and(not(X1),not(X2)))|~op_or),inference(split_conjunct,[status(thm)],[160])).
% fof(162, plain,(~(op_and)|![X2]:![X3]:and(X2,X3)=not(or(not(X2),not(X3)))),inference(fof_nnf,[status(thm)],[36])).
% fof(163, plain,(~(op_and)|![X4]:![X5]:and(X4,X5)=not(or(not(X4),not(X5)))),inference(variable_rename,[status(thm)],[162])).
% fof(164, plain,![X4]:![X5]:(and(X4,X5)=not(or(not(X4),not(X5)))|~(op_and)),inference(shift_quantors,[status(thm)],[163])).
% cnf(165,plain,(and(X1,X2)=not(or(not(X1),not(X2)))|~op_and),inference(split_conjunct,[status(thm)],[164])).
% fof(232, plain,(~(op_implies_or)|![X2]:![X3]:implies(X2,X3)=or(not(X2),X3)),inference(fof_nnf,[status(thm)],[48])).
% fof(233, plain,(~(op_implies_or)|![X4]:![X5]:implies(X4,X5)=or(not(X4),X5)),inference(variable_rename,[status(thm)],[232])).
% fof(234, plain,![X4]:![X5]:(implies(X4,X5)=or(not(X4),X5)|~(op_implies_or)),inference(shift_quantors,[status(thm)],[233])).
% cnf(235,plain,(implies(X1,X2)=or(not(X1),X2)|~op_implies_or),inference(split_conjunct,[status(thm)],[234])).
% fof(250, plain,(~(op_implies_and)|![X2]:![X3]:implies(X2,X3)=not(and(X2,not(X3)))),inference(fof_nnf,[status(thm)],[51])).
% fof(251, plain,(~(op_implies_and)|![X4]:![X5]:implies(X4,X5)=not(and(X4,not(X5)))),inference(variable_rename,[status(thm)],[250])).
% fof(252, plain,![X4]:![X5]:(implies(X4,X5)=not(and(X4,not(X5)))|~(op_implies_and)),inference(shift_quantors,[status(thm)],[251])).
% cnf(253,plain,(implies(X1,X2)=not(and(X1,not(X2)))|~op_implies_and),inference(split_conjunct,[status(thm)],[252])).
% cnf(258,negated_conjecture,(~r1),inference(split_conjunct,[status(thm)],[55])).
% cnf(263,plain,(~is_a_theorem(implies(or(esk1_0,esk1_0),esk1_0))),inference(sr,[status(thm)],[60,258,theory(equality)])).
% cnf(275,plain,(or(not(X1),X2)=implies(X1,X2)|$false),inference(rw,[status(thm)],[235,76,theory(equality)])).
% cnf(276,plain,(or(not(X1),X2)=implies(X1,X2)),inference(cn,[status(thm)],[275,theory(equality)])).
% cnf(287,plain,(is_a_theorem(implies(X1,implies(X2,X1)))|$false),inference(rw,[status(thm)],[133,64,theory(equality)])).
% cnf(288,plain,(is_a_theorem(implies(X1,implies(X2,X1)))),inference(cn,[status(thm)],[287,theory(equality)])).
% cnf(296,plain,(is_a_theorem(X1)|$false|~is_a_theorem(X2)|~is_a_theorem(implies(X2,X1))),inference(rw,[status(thm)],[127,62,theory(equality)])).
% cnf(297,plain,(is_a_theorem(X1)|~is_a_theorem(X2)|~is_a_theorem(implies(X2,X1))),inference(cn,[status(thm)],[296,theory(equality)])).
% cnf(303,plain,(not(and(X1,not(X2)))=implies(X1,X2)|$false),inference(rw,[status(thm)],[253,153,theory(equality)])).
% cnf(304,plain,(not(and(X1,not(X2)))=implies(X1,X2)),inference(cn,[status(thm)],[303,theory(equality)])).
% cnf(320,plain,(not(implies(X1,not(X2)))=and(X1,X2)|~op_and),inference(rw,[status(thm)],[165,276,theory(equality)])).
% cnf(321,plain,(not(implies(X1,not(X2)))=and(X1,X2)|$false),inference(rw,[status(thm)],[320,156,theory(equality)])).
% cnf(322,plain,(not(implies(X1,not(X2)))=and(X1,X2)),inference(cn,[status(thm)],[321,theory(equality)])).
% cnf(323,plain,(or(and(X1,X2),X3)=implies(implies(X1,not(X2)),X3)),inference(spm,[status(thm)],[276,322,theory(equality)])).
% cnf(327,plain,(implies(not(X1),X2)=or(X1,X2)|~op_or),inference(rw,[status(thm)],[161,304,theory(equality)])).
% cnf(328,plain,(implies(not(X1),X2)=or(X1,X2)|$false),inference(rw,[status(thm)],[327,152,theory(equality)])).
% cnf(329,plain,(implies(not(X1),X2)=or(X1,X2)),inference(cn,[status(thm)],[328,theory(equality)])).
% cnf(337,plain,(is_a_theorem(X1)|~is_a_theorem(or(X2,X1))|~is_a_theorem(not(X2))),inference(spm,[status(thm)],[297,329,theory(equality)])).
% cnf(368,plain,(is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2)))|$false),inference(rw,[status(thm)],[139,65,theory(equality)])).
% cnf(369,plain,(is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2)))),inference(cn,[status(thm)],[368,theory(equality)])).
% cnf(370,plain,(is_a_theorem(implies(X1,X2))|~is_a_theorem(implies(X1,implies(X1,X2)))),inference(spm,[status(thm)],[297,369,theory(equality)])).
% cnf(393,plain,(is_a_theorem(implies(implies(X1,X2),implies(implies(X3,X2),implies(or(X1,X3),X2))))|$false),inference(rw,[status(thm)],[94,72,theory(equality)])).
% cnf(394,plain,(is_a_theorem(implies(implies(X1,X2),implies(implies(X3,X2),implies(or(X1,X3),X2))))),inference(cn,[status(thm)],[393,theory(equality)])).
% cnf(499,plain,(is_a_theorem(implies(implies(X1,X2),implies(or(X1,X1),X2)))),inference(spm,[status(thm)],[370,394,theory(equality)])).
% cnf(501,plain,(is_a_theorem(implies(X1,X1))),inference(spm,[status(thm)],[370,288,theory(equality)])).
% cnf(511,plain,(is_a_theorem(or(X1,not(X1)))),inference(spm,[status(thm)],[501,329,theory(equality)])).
% cnf(537,plain,(is_a_theorem(implies(X1,not(not(X1))))),inference(spm,[status(thm)],[511,276,theory(equality)])).
% cnf(549,plain,(is_a_theorem(not(not(X1)))|~is_a_theorem(X1)),inference(spm,[status(thm)],[297,537,theory(equality)])).
% cnf(561,plain,(is_a_theorem(not(and(X1,X2)))|~is_a_theorem(implies(X1,not(X2)))),inference(spm,[status(thm)],[549,322,theory(equality)])).
% cnf(708,plain,(is_a_theorem(not(and(not(X1),X1)))),inference(spm,[status(thm)],[561,501,theory(equality)])).
% cnf(715,plain,(is_a_theorem(X1)|~is_a_theorem(or(and(not(X2),X2),X1))),inference(spm,[status(thm)],[337,708,theory(equality)])).
% cnf(725,plain,(is_a_theorem(X1)|~is_a_theorem(implies(or(X2,not(X2)),X1))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[715,323,theory(equality)]),329,theory(equality)])).
% cnf(968,plain,(is_a_theorem(X1)|~is_a_theorem(implies(implies(X2,not(not(X2))),X1))),inference(spm,[status(thm)],[725,276,theory(equality)])).
% cnf(1455,plain,(is_a_theorem(implies(or(X1,X1),not(not(X1))))),inference(spm,[status(thm)],[968,499,theory(equality)])).
% cnf(1516,plain,(is_a_theorem(not(and(or(X1,X1),not(X1))))),inference(spm,[status(thm)],[561,1455,theory(equality)])).
% cnf(1524,plain,(is_a_theorem(implies(or(X1,X1),X1))),inference(rw,[status(thm)],[1516,304,theory(equality)])).
% cnf(1533,plain,($false),inference(rw,[status(thm)],[263,1524,theory(equality)])).
% cnf(1534,plain,($false),inference(cn,[status(thm)],[1533,theory(equality)])).
% cnf(1535,plain,($false),1534,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 215
% # ...of these trivial : 27
% # ...subsumed : 22
% # ...remaining for further processing: 166
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 19
% # Generated clauses : 831
% # ...of the previous two non-trivial : 719
% # Contextual simplify-reflections : 0
% # Paramodulations : 831
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 147
% # Positive orientable unit clauses: 95
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 50
% # Current number of unprocessed clauses: 560
% # ...number of literals in the above : 706
% # Clause-clause subsumption calls (NU) : 288
% # Rec. Clause-clause subsumption calls : 288
% # Unit Clause-clause subsumption calls : 114
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 245
% # Indexed BW rewrite successes : 18
% # Backwards rewriting index: 187 leaves, 1.71+/-1.381 terms/leaf
% # Paramod-from index: 63 leaves, 1.60+/-1.409 terms/leaf
% # Paramod-into index: 176 leaves, 1.67+/-1.299 terms/leaf
% # -------------------------------------------------
% # User time : 0.039 s
% # System time : 0.007 s
% # Total time : 0.046 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.15 CPU 0.24 WC
% FINAL PrfWatch: 0.15 CPU 0.24 WC
% SZS output end Solution for /tmp/SystemOnTPTP309/LCL454+1.tptp
%
%------------------------------------------------------------------------------