MAYBE
Time: 0.025

Problem:
 Equations:
  appAC(appAC(x5,x6),x7) -> appAC(x5,appAC(x6,x7))
  appAC(x5,x6) -> appAC(x6,x5)
  appAC(x5,appAC(x6,x7)) -> appAC(appAC(x5,x6),x7)
  appAC(x6,x5) -> appAC(x5,x6)
 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))
  appAC(empty(),X) -> X
  max(singl(x)) -> x
  max(appAC(singl(x),Y)) -> max2(x,Y)
  max2(x,empty()) -> x
  max2(x,singl(y)) -> max'C(x,y)
  max2(x,appAC(singl(y),Z)) -> max2(max'C(x,y),Z)

Proof:
 Open