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) 0(#) -> #
(2) +(#,x) -> x
(3) +(x,#) -> x
(4) +(0(x),0(y)) -> 0(+(x,y))
(5) +(0(x),1(y)) -> 1(+(x,y))
(6) +(1(x),0(y)) -> 1(+(x,y))
(7) +(0(x),j(y)) -> j(+(x,y))
(8) +(j(x),0(y)) -> j(+(x,y))
(9) +(1(x),1(y)) -> j(+(+(x,y),1(#)))
(10) +(j(x),j(y)) -> 1(+(+(x,y),j(#)))
(11) +(1(x),j(y)) -> 0(+(x,y))
(12) +(j(x),1(y)) -> 0(+(x,y))
(13) +(+(x,y),z) -> +(x,+(y,z))
(14) opp(#) -> #
(15) opp(0(x)) -> 0(opp(x))
(16) opp(1(x)) -> j(opp(x))
(17) opp(j(x)) -> 1(opp(x))
(18) -(x,y) -> +(x,opp(y))
(19) *(#,x) -> #
(20) *(0(x),y) -> 0(*(x,y))
(21) *(1(x),y) -> +(0(*(x,y)),y)
(22) *(j(x),y) -> -(0(*(x,y)),y)
(23) *(*(x,y),z) -> *(x,*(y,z))

[2]  Use following polynomial interpretation:
[1(x)] = x + 1
[j(x)] = x + 1
[*(x,y)] = xy
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(11)-(12), (19), (21)-(22)

[3]  Use following polynomial interpretation:
[-(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(18)

[4]  Use following polynomial interpretation:
[opp(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(14)

[5]  Use following polynomial interpretation:
[0(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1), (4)-(8)

[6]  Use following polynomial interpretation:
[*(x,y)] = x^2 + y
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(23)

[7]  Use following polynomial interpretation:
[0(x)] = x + 1
[*(x,y)] = xy
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(20)

[8]  Use following polynomial interpretation:
[0(x)] = x + 1
[opp(x)] = 7x
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(15)

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

  This interpretation is a model and yields following TRS:
(2) +{2,k}(#,x) -> x
(3) +{k,2}(x,#) -> x
(9) +{k + 1,j + 1}(1{k}(x),1{j}(y)) -> j{-1 + j + k}(+{j + k - 2,3}(+{k,j}(x,y),1{2}(#)))
(10) +{k + 1,j + 1}(j{k}(x),j{j}(y)) -> 1{-1 + j + k}(+{j + k - 2,3}(+{k,j}(x,y),j{2}(#)))
(13) +{j + k - 2,i}(+{k,j}(x,y),z) -> +{k,i + j - 2}(x,+{j,i}(y,z))
(16) opp{k + 1}(1{k}(x)) -> j{k}(opp{k}(x))
(17) opp{k + 1}(j{k}(x)) -> 1{k}(opp{k}(x))

[10]  Use following polynomial interpretation:
[+_{i,j}(x,y)] = x + y - 2
[1_{i}(x)] = x
[j_{i}(x)] = x
[opp_{i}(x)] = x + i
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(16)-(17)

[11]  Unlabel this TRS to obtain the one consisting of the rules:
(2)-(3), (9)-(10), (13)

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

  This interpretation is a model and yields following TRS:
(2) +{2,k}(#,x) -> x
(3) +{k,2}(x,#) -> x
(9) +{k + 1,j + 1}(1{k}(x),1{j}(y)) -> j{-1 + j + k}(+{j + k - 2,3}(+{k,j}(x,y),1{2}(#)))
(10) +{k + 1,j + 1}(j{k}(x),j{j}(y)) -> 1{-1 + j + k}(+{j + k - 2,3}(+{k,j}(x,y),j{2}(#)))
(13) +{j + k - 2,i}(+{k,j}(x,y),z) -> +{k,i + j - 2}(x,+{j,i}(y,z))

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


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