YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
(2) plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))

[2]  Label this TRS using following interpretation over N\{0,1}:
[plus(x,y)] = x + y + 1
rest default

  This interpretation is a model and yields following TRS:
(1) plus{i,k + j + 1}(s{i}(X),plus{j,k}(Y,Z)) -> plus{i,k + j + 1}(X,plus{j,k}(s{j}(s{j}(Y)),Z))
(2) plus{l0,l2 + l1 + l3 + 2}(s{l0}(X1),plus{l1,l3 + l2 + 1}(X2,plus{l2,l3}(X3,X4))) -> plus{l0,l1 + l2 + l3 + 2}(X1,plus{l2,l3 + l1 + 1}(X3,plus{l1,l3}(X2,X4)))

[3]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: plus: Lex-LR, 
Precedence:
plus{i,j} > plus{k,l} for j > l
plus{i,j} > s{k} for all i, j, k


../tpdb/TRS/Rubio/bn129.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory