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) +(1(x),1(y)) -> 0(+(+(x,y),1(#)))
(8) +(x,+(y,z)) -> +(+(x,y),z)
(9) -(x,#) -> x
(10) -(#,x) -> #
(11) -(0(x),0(y)) -> 0(-(x,y))
(12) -(0(x),1(y)) -> 1(-(-(x,y),1(#)))
(13) -(1(x),0(y)) -> 1(-(x,y))
(14) -(1(x),1(y)) -> 0(-(x,y))
(15) not(false) -> true
(16) not(true) -> false
(17) and(x,true) -> x
(18) and(x,false) -> false
(19) if`1(true,if`2(x,y)) -> x
(20) if`1(false,if`2(x,y)) -> y
(21) ge(0(x),0(y)) -> ge(x,y)
(22) ge(0(x),1(y)) -> not(ge(y,x))
(23) ge(1(x),0(y)) -> ge(x,y)
(24) ge(1(x),1(y)) -> ge(x,y)
(25) ge(x,#) -> true
(26) ge(#,1(x)) -> false
(27) ge(#,0(x)) -> ge(#,x)
(28) val(l(x)) -> x
(29) val(n`1(x,n`2(y,z))) -> x
(30) min(l(x)) -> x
(31) min(n`1(x,n`2(y,z))) -> min(y)
(32) max(l(x)) -> x
(33) max(n`1(x,n`2(y,z))) -> max(z)
(34) bs(l(x)) -> true
(35) bs(n`1(x,n`2(y,z))) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
(36) size(l(x)) -> 1(#)
(37) size(n`1(x,n`2(y,z))) -> +(+(size(x),size(y)),1(#))
(38) wb(l(x)) -> true
(39) wb(n`1(x,n`2(y,z))) -> and(if`1(ge(size(y),size(z)),if`2(ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y))))),and(wb(y),wb(z)))

[2]  Use following polynomial interpretation:
[n`1(x,y)] = 7xy
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(29), (31), (33), (35), (37), (39)

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

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

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

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

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

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

[6]  Use following polynomial interpretation:
[max(x)] = x + 1
rest default

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

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

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

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

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

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

  Remove rules with left hand side strictly bigger than right hand side:
(25)-(26)

[10]  Use following polynomial interpretation:
[if`1(x,y)] = x + y + 1
rest default

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

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

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

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

  Remove rules with left hand side strictly bigger than right hand side:
(1), (4)-(6), (11), (13)-(14), (21)-(24), (27)

[13]  Use following polynomial interpretation:
[not(x)] = x + 1
rest default

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

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

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

[15]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: +: Lex-RL, 
Precedence:
+{i,j} > 0{k} for all i, j, k
+{i,j} > # for all i, j
-{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} > 1{k} for all i, j, k
-{i,j} > -{k,l} for i > k


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