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) l(m(x)) -> m(l(x))
(2) m(r(x)) -> r(m(x))
(3) f(m(x),y) -> f(x,m(y))
(4) b ->= l(b)
(5) f(x,y) ->= f(x,r(y))

[2]  Label this TRS using following interpretation that is a quasi-model:
[l(x)] = 0
[m(x)] = 0
[r(x)] = 0
[f(x,y)] = 0
[b] = 1
rest default

  thus obtaining new TRS:
(1a) l$0(m$1(x)) -> m$0(l$1(x))
(1b) l$0(m$0(x)) -> m$0(l$0(x))
(2a) m$0(r$1(x)) -> r$0(m$1(x))
(2b) m$0(r$0(x)) -> r$0(m$0(x))
(3a) f$01(m$1(x),y) -> f$10(x,m$1(y))
(3b) f$00(m$1(x),y) -> f$10(x,m$0(y))
(3c) f$01(m$0(x),y) -> f$00(x,m$1(y))
(3d) f$00(m$0(x),y) -> f$00(x,m$0(y))
(4a) b ->= l$1(b)
(5a) f$11(x,y) ->= f$10(x,r$1(y))
(5b) f$10(x,y) ->= f$10(x,r$0(y))
(5c) f$01(x,y) ->= f$00(x,r$1(y))
(5d) f$00(x,y) ->= f$00(x,r$0(y))
(D1) m$1(x) ->= m$0(x)
(D2) l$1(x) ->= l$0(x)
(D3) r$1(x) ->= r$0(x)
(D4) f$10(x,y) ->= f$00(x,y)
(D5) f$11(x,y) ->= f$01(x,y)
(D6) f$11(x,y) ->= f$10(x,y)
(D7) f$01(x,y) ->= f$00(x,y)

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

  Remove rules with left hand side strictly bigger than right hand side:
(5a), (D5)-(D6)

[4]  Use following polynomial interpretation:
[f$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(3a), (3c), (5c), (D7)

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

  Remove rules with left hand side strictly bigger than right hand side:
(2a), (D3)

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

  Remove rules with left hand side strictly bigger than right hand side:
(1a), (3b), (D1)

[7]  Use following polynomial interpretation:
[f$10(x,y)] = x + y + 1
rest default

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

[8]  Use following polynomial interpretation:
[m$0(x)] = x + 1
[f$00(x,y)] = x^2 + y
rest default

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

[9]  Unlabel this TRS to obtain the one consisting of the rules:
(1)-(2), (4)-(5)

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

  This interpretation is a model and yields following TRS:
(1) l{i}(m{i}(x)) -> m{i}(l{i}(x))
(2) m{i + 1}(r{i}(x)) -> r{i}(m{i}(x))
(4) b ->= l{2}(b)
(5) f{i,j}(x,y) ->= f{i,j + 1}(x,r{j}(y))

[11]  Use following polynomial interpretation:
[l_{i}(x)] = x
[m_{i}(x)] = x + i
[r_{i}(x)] = x
[f_{i,j}(x,y)] = x + y - 2
rest default

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

[12]  Unlabel this TRS to obtain the one consisting of the rules:
(1), (4)-(5)

[13]  Label this TRS using following interpretation that is a model:
[m(x)] = 1
[f(x,y)] = 0
rest default

  thus obtaining new TRS:
(1a) l$1(m$1(x)) -> m$1(l$1(x))
(1b) l$1(m$0(x)) -> m$0(l$0(x))
(4a) b ->= l$0(b)
(5a) f$11(x,y) ->= f$11(x,r$1(y))
(5b) f$10(x,y) ->= f$10(x,r$0(y))
(5c) f$01(x,y) ->= f$01(x,r$1(y))
(5d) f$00(x,y) ->= f$00(x,r$0(y))

[14]  Use following polynomial interpretation:
[l$1(x)] = x + 1
rest default

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

[15]  Use following polynomial interpretation:
[m$1(x)] = x + 1
[l$1(x)] = 7x
rest default

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

[16]  Since there are no remaining strict rules, relative termination is proved!

../tpdb/TRS/relative/rt3-9.trs, 0., Y
Couldn't open file <60>: 60: No such file or directory