YES
Time: 0.174

Problem:
 Equations:
  
 TRS:
  1() -> s(0())
  2() -> s(1())
  3() -> s(2())
  4() -> s(3())
  5() -> s(4())
  6() -> s(5())
  7() -> s(6())
  8() -> s(7())
  9() -> s(8())
  max'C(0(),x) -> x
  max'C(s(x),s(y)) -> s(max'C(x,y))
  app(empty(),X) -> X
  max(singl(x)) -> x
  max(app(singl(x),Y)) -> max2(x,Y)
  max2(x,empty()) -> x
  max2(x,singl(y)) -> max'C(x,y)
  max2(x,app(singl(y),Z)) -> max2(max'C(x,y),Z)

Proof:
 AC-KBO Processor:
  precedence:
   max2 > empty > 2 > max > 9 > 4 > 6 > 0 > app > 1 > 5 > 7 > 8 > 3 > singl > s > max'C
   weight function:
    w0 = 4
    w(9) = 14
    w(8) = 13
    w(singl) = w(7) = 12
    w(6) = 11
    w(5) = 10
    w(4) = 8
    w(3) = 7
    w(2) = w(app) = 6
    w(1) = 5
    w(empty) = w(0) = 4
    w(max) = 2
    w(s) = 1
    w(max2) = w(max'C) = 0
   problem:
    Equations:
     
    TRS:
     
   Qed