YES
Time: 0.158

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:
 DP Processor:
  Equations#:
   app{AC,#}(appAC(x5,x6),x7) -> app{AC,#}(x5,appAC(x6,x7))
   app{AC,#}(x5,x6) -> app{AC,#}(x6,x5)
   app{AC,#}(x5,appAC(x6,x7)) -> app{AC,#}(appAC(x5,x6),x7)
   app{AC,#}(x6,x5) -> app{AC,#}(x5,x6)
  DPs:
   2#() -> 1#()
   3#() -> 2#()
   4#() -> 3#()
   5#() -> 4#()
   6#() -> 5#()
   7#() -> 6#()
   8#() -> 7#()
   9#() -> 8#()
   max'{C,#}(s(x),s(y)) -> max'{C,#}(x,y)
   max#(appAC(singl(x),Y)) -> max2#(x,Y)
   max2#(x,singl(y)) -> max'{C,#}(x,y)
   max2#(x,appAC(singl(y),Z)) -> max'{C,#}(x,y)
   max2#(x,appAC(singl(y),Z)) -> max2#(max'C(x,y),Z)
   app{AC,#}(x8,appAC(empty(),X)) -> app{AC,#}(x8,X)
  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)
  S:
   app{AC,#}(appAC(x9,x10),x11) -> app{AC,#}(x9,x10)
   app{AC,#}(x9,appAC(x10,x11)) -> app{AC,#}(x10,x11)
  AC-EDG Processor:
   Equations#:
    app{AC,#}(appAC(x5,x6),x7) -> app{AC,#}(x5,appAC(x6,x7))
    app{AC,#}(x5,x6) -> app{AC,#}(x6,x5)
    app{AC,#}(x5,appAC(x6,x7)) -> app{AC,#}(appAC(x5,x6),x7)
    app{AC,#}(x6,x5) -> app{AC,#}(x5,x6)
   DPs:
    2#() -> 1#()
    3#() -> 2#()
    4#() -> 3#()
    5#() -> 4#()
    6#() -> 5#()
    7#() -> 6#()
    8#() -> 7#()
    9#() -> 8#()
    max'{C,#}(s(x),s(y)) -> max'{C,#}(x,y)
    max#(appAC(singl(x),Y)) -> max2#(x,Y)
    max2#(x,singl(y)) -> max'{C,#}(x,y)
    max2#(x,appAC(singl(y),Z)) -> max'{C,#}(x,y)
    max2#(x,appAC(singl(y),Z)) -> max2#(max'C(x,y),Z)
    app{AC,#}(x8,appAC(empty(),X)) -> app{AC,#}(x8,X)
   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)
   S:
    app{AC,#}(appAC(x9,x10),x11) -> app{AC,#}(x9,x10)
    app{AC,#}(x9,appAC(x10,x11)) -> app{AC,#}(x10,x11)
   SCC Processor:
    #sccs: 3
    #rules: 3
    #arcs: 17/196
    Equations#:
     app{AC,#}(appAC(x5,x6),x7) -> app{AC,#}(x5,appAC(x6,x7))
     app{AC,#}(x5,x6) -> app{AC,#}(x6,x5)
     app{AC,#}(x5,appAC(x6,x7)) -> app{AC,#}(appAC(x5,x6),x7)
     app{AC,#}(x6,x5) -> app{AC,#}(x5,x6)
    DPs:
     app{AC,#}(x8,appAC(empty(),X)) -> app{AC,#}(x8,X)
    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)
    S:
     app{AC,#}(appAC(x9,x10),x11) -> app{AC,#}(x9,x10)
     app{AC,#}(x9,appAC(x10,x11)) -> app{AC,#}(x10,x11)
    AC-DP unlabeling:
     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)
     DPs:
      appAC(x8,appAC(empty(),X)) -> appAC(x8,X)
     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)
     S:
      appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
      appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
     Usable Rule Processor:
      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)
      DPs:
       appAC(x8,appAC(empty(),X)) -> appAC(x8,X)
      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:
       appAC(empty(),X) -> X
      S:
       appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
       appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
      AC-KBO Processor:
       argument filtering:
        pi(appAC) = [0,1]
        pi(empty) = []
       precedence:
        empty ~ appAC
        weight function:
         w0 = 1
         w(empty) = 7
         w(appAC) = 1
         usable rules:
          appAC(empty(),X) -> X
         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)
          DPs:
           
          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:
           appAC(empty(),X) -> X
          S:
           appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
           appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
         Qed
     
     Equations#:
      app{AC,#}(appAC(x5,x6),x7) -> app{AC,#}(x5,appAC(x6,x7))
      app{AC,#}(x5,x6) -> app{AC,#}(x6,x5)
      app{AC,#}(x5,appAC(x6,x7)) -> app{AC,#}(appAC(x5,x6),x7)
      app{AC,#}(x6,x5) -> app{AC,#}(x5,x6)
     DPs:
      max2#(x,appAC(singl(y),Z)) -> max2#(max'C(x,y),Z)
     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)
     S:
      app{AC,#}(appAC(x9,x10),x11) -> app{AC,#}(x9,x10)
      app{AC,#}(x9,appAC(x10,x11)) -> app{AC,#}(x10,x11)
     AC-DP unlabeling:
      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)
      DPs:
       max2#(x,appAC(singl(y),Z)) -> max2#(max'C(x,y),Z)
      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)
      S:
       appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
       appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
      Usable Rule Processor:
       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)
       DPs:
        max2#(x,appAC(singl(y),Z)) -> max2#(max'C(x,y),Z)
       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:
        max'C(0(),x) -> x
        max'C(s(x),s(y)) -> s(max'C(x,y))
       S:
        appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
        appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
       AC-KBO Processor:
        argument filtering:
         pi(appAC) = [0,1]
         pi(max'C) = []
         pi(0) = []
         pi(s) = 0
         pi(singl) = []
         pi(max2#) = 1
        precedence:
         max2# ~ singl ~ s ~ 0 ~ max'C ~ appAC
         weight function:
          w0 = 4
          w(singl) = 5
          w(max2#) = w(s) = w(0) = w(max'C) = w(appAC) = 4
          usable rules:
           
          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)
           DPs:
            
           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:
            max'C(0(),x) -> x
            max'C(s(x),s(y)) -> s(max'C(x,y))
           S:
            appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
            appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
          Qed
      
      Equations#:
       app{AC,#}(appAC(x5,x6),x7) -> app{AC,#}(x5,appAC(x6,x7))
       app{AC,#}(x5,x6) -> app{AC,#}(x6,x5)
       app{AC,#}(x5,appAC(x6,x7)) -> app{AC,#}(appAC(x5,x6),x7)
       app{AC,#}(x6,x5) -> app{AC,#}(x5,x6)
      DPs:
       max'{C,#}(s(x),s(y)) -> max'{C,#}(x,y)
      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)
      S:
       app{AC,#}(appAC(x9,x10),x11) -> app{AC,#}(x9,x10)
       app{AC,#}(x9,appAC(x10,x11)) -> app{AC,#}(x10,x11)
      AC-DP unlabeling:
       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)
       DPs:
        max'{C,#}(s(x),s(y)) -> max'{C,#}(x,y)
       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)
       S:
        appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
        appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
       Usable Rule Processor:
        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)
        DPs:
         max'{C,#}(s(x),s(y)) -> max'{C,#}(x,y)
        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:
         
        S:
         appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
         appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
        AC-KBO Processor:
         argument filtering:
          pi(s) = [0]
          pi(max'{C,#}) = [0,1]
         precedence:
          max'{C,#} ~ s
          weight function:
           w0 = 1
           w(max'{C,#}) = 7
           w(s) = 1
           usable rules:
            
           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)
            DPs:
             
            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:
             
            S:
             appAC(appAC(x9,x10),x11) -> appAC(x9,x10)
             appAC(x9,appAC(x10,x11)) -> appAC(x10,x11)
           Qed