YES

TRS:

  f(x,nil()) -> g(nil(),x)
  f(x,g(y,z)) -> g(f(x,y),z)
  ++(x,nil()) -> x
  ++(x,g(y,z)) -> g(++(x,y),z)
  null(nil()) -> true()
  null(g(x,y)) -> false()
  mem(nil(),y) -> false()
  mem(g(x,y),z) -> or(=(y,z),mem(x,z))
  mem(x,max(x)) -> not(null(x))
  max(g(g(nil(),x),y)) -> max'(x,y)
  max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())

max/plus interpretations on N:

  f_A(x1,x2) = max{6, 5 + x1, 1 + x2}
  f#_A(x1,x2) = max{6, 5 + x1, 1 + x2}
  nil_A = 4
  nil#_A = 4
  g_A(x1,x2) = max{6, x1, 2 + x2}
  g#_A(x1,x2) = max{6, x1, 2 + x2}
  ++_A(x1,x2) = max{0, x1, x2}
  ++#_A(x1,x2) = max{0, x1, x2}
  null_A(x1) = max{17, 8 + x1}
  null#_A(x1) = max{17, 8 + x1}
  true_A = 0
  true#_A = 0
  false_A = 3
  false#_A = 3
  mem_A(x1,x2) = max{28, 20 + x1, 9 + x2}
  mem#_A(x1,x2) = max{28, 20 + x1, 9 + x2}
  or_A(x1,x2) = max{27, x1, x2}
  or#_A(x1,x2) = max{27, x1, x2}
  =_A(x1,x2) = max{27, x1, x2}
  =#_A(x1,x2) = max{27, x1, x2}
  max_A(x1) = max{7, x1}
  max#_A(x1) = max{7, x1}
  not_A(x1) = max{8, 2 + x1}
  not#_A(x1) = max{8, 2 + x1}
  max'_A(x1,x2) = max{7, x1, 2 + x2}
  max'#_A(x1,x2) = max{7, x1, 2 + x2}
  u_A = 5
  u#_A = 5

precedence:

  nil > f = ++ = true > g > false = max > mem = max' = u > null = or = = = not