YES
Time: 0.489

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:
   7 > 2 > app > 1 > max'C > 9 > max2 > singl > 8 > 0 > max > 3 > empty > 6 > 5 > s > 4
   weight function:
    [max2](x0, x1) = x0 + x1 + 8,
    
    [max](x0) = 3x0 + 15,
    
    [singl](x0) = 11x0 + 8,
    
    [empty] = 1,
    
    [9] = 14,
    
    [8] = 13,
    
    [7] = 12,
    
    [6] = 9,
    
    [5] = 8,
    
    [4] = 6,
    
    [3] = 4,
    
    [2] = 3,
    
    [s](x0) = x0 + 1,
    
    [0] = 1,
    
    [1] = 2,
    
    [max'C](x0, x1) = x0 + 11x1 + 3,
    
    [app](x0, x1) = x0 + 2x1 + 3
   problem:
    Equations:
     
    TRS:
     
   Qed