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, 3, 3}
  f#_A(x1,x2) = max{0, 6, 6}
  nil_A = 1
  nil#_A = 7
  g_A(x1,x2) = max{6, 4, 3}
  g#_A(x1,x2) = max{6, 1, 3}
  ++_A(x1,x2) = max{4, 3 + x1, 1 + x2}
  ++#_A(x1,x2) = max{1, 5, 7}
  null_A(x1) = max{2, -5 + x1}
  null#_A(x1) = max{5, 3}
  true_A = 0
  true#_A = 6
  false_A = 2
  false#_A = 2
  mem_A(x1,x2) = max{1, -1, 4 + x2}
  mem#_A(x1,x2) = max{10, 14, 11 + x2}
  or_A(x1,x2) = max{2, 3 + x1, x2}
  or#_A(x1,x2) = max{13, 9, 9}
  =_A(x1,x2) = max{1, -4, 1 + x2}
  =#_A(x1,x2) = max{0, 0, 0}
  max_A(x1) = max{5, -2 + x1}
  max#_A(x1) = max{4, 7}
  not_A(x1) = max{3, 7 + x1}
  not#_A(x1) = max{8, 13 + x1}
  max'_A(x1,x2) = max{5, 1, 5}
  max'#_A(x1,x2) = max{2, 2, 0}
  u_A = 1
  u#_A = 5

precedence:

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