YES
Time: 2.364

Problem:
 Equations:
  plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
  plusAC(x4,x5) -> plusAC(x5,x4)
  appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
  appAC(x4,x5) -> appAC(x5,x4)
  plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
  plusAC(x5,x4) -> plusAC(x4,x5)
  appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
  appAC(x5,x4) -> appAC(x4,x5)
 TRS:
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eq(0(),0()) -> true()
  eq(0(),s(x)) -> false()
  eq(s(x),s(y)) -> eq(x,y)
  plusAC(empty(),x) -> x
  appAC(x,empty()) -> empty()
  appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
  appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
  appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
  appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())

Proof:
 DP Processor:
  Equations#:
   plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
   plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
   app{AC,#}(appAC(x4,x5),x6) -> app{AC,#}(x4,appAC(x5,x6))
   app{AC,#}(x4,x5) -> app{AC,#}(x5,x4)
   plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
   plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
   app{AC,#}(x4,appAC(x5,x6)) -> app{AC,#}(appAC(x4,x5),x6)
   app{AC,#}(x5,x4) -> app{AC,#}(x4,x5)
  DPs:
   eq#(s(x),s(y)) -> eq#(x,y)
   app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,z)
   app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,y)
   app{AC,#}(x,plusAC(y,z)) -> plus{AC,#}(appAC(x,y),appAC(x,z))
   app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,z)
   app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,y)
   app{AC,#}(x,appAC(plusAC(y,z),t)) -> plus{AC,#}(appAC(x,y),appAC(x,z))
   app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
   app{AC,#}(singl(x),singl(y)) -> eq#(x,y)
   app{AC,#}(singl(x),singl(y)) -> if#(eq(x,y),singl(x),empty())
   plus{AC,#}(x7,plusAC(empty(),x)) -> plus{AC,#}(x7,x)
   app{AC,#}(x8,appAC(x,empty())) -> app{AC,#}(x8,empty())
   app{AC,#}(x9,appAC(x,appAC(empty(),z))) -> app{AC,#}(x9,appAC(empty(),z))
   app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,z)
   app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,y)
   app{AC,#}(x10,appAC(x,plusAC(y,z))) -> plus{AC,#}(appAC(x,y),appAC(x,z))
   app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x10,plusAC(appAC(x,y),appAC(x,z)))
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,z)
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,y)
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> plus{AC,#}(appAC(x,y),appAC(x,z))
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) ->
   app{AC,#}(x11,appAC(plusAC(appAC(x,y),appAC(x,z)),t))
   app{AC,#}(x12,appAC(singl(x),singl(y))) -> eq#(x,y)
   app{AC,#}(x12,appAC(singl(x),singl(y))) -> if#(eq(x,y),singl(x),empty())
   app{AC,#}(x12,appAC(singl(x),singl(y))) -> app{AC,#}(x12,if(eq(x,y),singl(x),empty()))
  Equations:
   plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
   plusAC(x4,x5) -> plusAC(x5,x4)
   appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
   appAC(x4,x5) -> appAC(x5,x4)
   plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
   plusAC(x5,x4) -> plusAC(x4,x5)
   appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
   appAC(x5,x4) -> appAC(x4,x5)
  TRS:
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   eq(0(),0()) -> true()
   eq(0(),s(x)) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   plusAC(empty(),x) -> x
   appAC(x,empty()) -> empty()
   appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
   appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
   appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
   appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
  S:
   plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
   plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
   app{AC,#}(appAC(x13,x14),x15) -> app{AC,#}(x13,x14)
   app{AC,#}(x13,appAC(x14,x15)) -> app{AC,#}(x14,x15)
  AC-EDG Processor:
   Equations#:
    plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
    plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
    app{AC,#}(appAC(x4,x5),x6) -> app{AC,#}(x4,appAC(x5,x6))
    app{AC,#}(x4,x5) -> app{AC,#}(x5,x4)
    plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
    plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
    app{AC,#}(x4,appAC(x5,x6)) -> app{AC,#}(appAC(x4,x5),x6)
    app{AC,#}(x5,x4) -> app{AC,#}(x4,x5)
   DPs:
    eq#(s(x),s(y)) -> eq#(x,y)
    app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,z)
    app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,y)
    app{AC,#}(x,plusAC(y,z)) -> plus{AC,#}(appAC(x,y),appAC(x,z))
    app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,z)
    app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,y)
    app{AC,#}(x,appAC(plusAC(y,z),t)) -> plus{AC,#}(appAC(x,y),appAC(x,z))
    app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
    app{AC,#}(singl(x),singl(y)) -> eq#(x,y)
    app{AC,#}(singl(x),singl(y)) -> if#(eq(x,y),singl(x),empty())
    plus{AC,#}(x7,plusAC(empty(),x)) -> plus{AC,#}(x7,x)
    app{AC,#}(x8,appAC(x,empty())) -> app{AC,#}(x8,empty())
    app{AC,#}(x9,appAC(x,appAC(empty(),z))) -> app{AC,#}(x9,appAC(empty(),z))
    app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,z)
    app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,y)
    app{AC,#}(x10,appAC(x,plusAC(y,z))) -> plus{AC,#}(appAC(x,y),appAC(x,z))
    app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x10,plusAC(appAC(x,y),appAC(x,z)))
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,z)
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,y)
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> plus{AC,#}(appAC(x,y),appAC(x,z))
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) ->
    app{AC,#}(x11,appAC(plusAC(appAC(x,y),appAC(x,z)),t))
    app{AC,#}(x12,appAC(singl(x),singl(y))) -> eq#(x,y)
    app{AC,#}(x12,appAC(singl(x),singl(y))) -> if#(eq(x,y),singl(x),empty())
    app{AC,#}(x12,appAC(singl(x),singl(y))) -> app{AC,#}(x12,if(eq(x,y),singl(x),empty()))
   Equations:
    plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
    plusAC(x4,x5) -> plusAC(x5,x4)
    appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
    appAC(x4,x5) -> appAC(x5,x4)
    plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
    plusAC(x5,x4) -> plusAC(x4,x5)
    appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
    appAC(x5,x4) -> appAC(x4,x5)
   TRS:
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    plusAC(empty(),x) -> x
    appAC(x,empty()) -> empty()
    appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
    appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
    appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
    appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
   S:
    plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
    plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
    app{AC,#}(appAC(x13,x14),x15) -> app{AC,#}(x13,x14)
    app{AC,#}(x13,appAC(x14,x15)) -> app{AC,#}(x14,x15)
   SCC Processor:
    #sccs: 3
    #rules: 17
    #arcs: 353/625
    Equations#:
     plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
     plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
     app{AC,#}(appAC(x4,x5),x6) -> app{AC,#}(x4,appAC(x5,x6))
     app{AC,#}(x4,x5) -> app{AC,#}(x5,x4)
     plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
     plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
     app{AC,#}(x4,appAC(x5,x6)) -> app{AC,#}(appAC(x4,x5),x6)
     app{AC,#}(x5,x4) -> app{AC,#}(x4,x5)
    DPs:
     app{AC,#}(x12,appAC(singl(x),singl(y))) -> app{AC,#}(x12,if(eq(x,y),singl(x),empty()))
     app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) ->
     app{AC,#}(x11,appAC(plusAC(appAC(x,y),appAC(x,z)),t))
     app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
     app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,y)
     app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,z)
     app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x10,plusAC(appAC(x,y),appAC(x,z)))
     app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,y)
     app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,z)
     app{AC,#}(x9,appAC(x,appAC(empty(),z))) -> app{AC,#}(x9,appAC(empty(),z))
     app{AC,#}(x8,appAC(x,empty())) -> app{AC,#}(x8,empty())
     app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
     app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,y)
     app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,z)
     app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,y)
     app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,z)
    Equations:
     plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
     plusAC(x4,x5) -> plusAC(x5,x4)
     appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
     appAC(x4,x5) -> appAC(x5,x4)
     plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
     plusAC(x5,x4) -> plusAC(x4,x5)
     appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
     appAC(x5,x4) -> appAC(x4,x5)
    TRS:
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     plusAC(empty(),x) -> x
     appAC(x,empty()) -> empty()
     appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
     appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
     appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
     appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
    S:
     plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
     plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
     app{AC,#}(appAC(x13,x14),x15) -> app{AC,#}(x13,x14)
     app{AC,#}(x13,appAC(x14,x15)) -> app{AC,#}(x14,x15)
    AC-DP unlabeling:
     Equations#:
      plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
      plusAC(x4,x5) -> plusAC(x5,x4)
      appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
      appAC(x4,x5) -> appAC(x5,x4)
      plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
      plusAC(x5,x4) -> plusAC(x4,x5)
      appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
      appAC(x5,x4) -> appAC(x4,x5)
     DPs:
      appAC(x12,appAC(singl(x),singl(y))) -> appAC(x12,if(eq(x,y),singl(x),empty()))
      appAC(x11,appAC(x,appAC(plusAC(y,z),t))) -> appAC(x11,appAC(plusAC(appAC(x,y),appAC(x,z)),t))
      appAC(x11,appAC(x,appAC(plusAC(y,z),t))) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
      appAC(x11,appAC(x,appAC(plusAC(y,z),t))) -> appAC(x,y)
      appAC(x11,appAC(x,appAC(plusAC(y,z),t))) -> appAC(x,z)
      appAC(x10,appAC(x,plusAC(y,z))) -> appAC(x10,plusAC(appAC(x,y),appAC(x,z)))
      appAC(x10,appAC(x,plusAC(y,z))) -> appAC(x,y)
      appAC(x10,appAC(x,plusAC(y,z))) -> appAC(x,z)
      appAC(x9,appAC(x,appAC(empty(),z))) -> appAC(x9,appAC(empty(),z))
      appAC(x8,appAC(x,empty())) -> appAC(x8,empty())
      appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
      appAC(x,appAC(plusAC(y,z),t)) -> appAC(x,y)
      appAC(x,appAC(plusAC(y,z),t)) -> appAC(x,z)
      appAC(x,plusAC(y,z)) -> appAC(x,y)
      appAC(x,plusAC(y,z)) -> appAC(x,z)
     Equations:
      plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
      plusAC(x4,x5) -> plusAC(x5,x4)
      appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
      appAC(x4,x5) -> appAC(x5,x4)
      plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
      plusAC(x5,x4) -> plusAC(x4,x5)
      appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
      appAC(x5,x4) -> appAC(x4,x5)
     TRS:
      if(true(),x,y) -> x
      if(false(),x,y) -> y
      eq(0(),0()) -> true()
      eq(0(),s(x)) -> false()
      eq(s(x),s(y)) -> eq(x,y)
      plusAC(empty(),x) -> x
      appAC(x,empty()) -> empty()
      appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
      appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
      appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
      appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
     S:
      plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14)
      plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15)
      appAC(appAC(x13,x14),x15) -> appAC(x13,x14)
      appAC(x13,appAC(x14,x15)) -> appAC(x14,x15)
     AC-RPO Processor:
      argument filtering:
       pi(appAC) = [0,1]
       pi(plusAC) = [0,1]
       pi(true) = []
       pi(if) = [1,2]
       pi(false) = []
       pi(0) = []
       pi(eq) = 1
       pi(s) = 0
       pi(empty) = []
       pi(singl) = [0]
      precedence:
       appAC > plusAC > empty > false > 0 > eq > if > true > singl > s
      status:
       eq:mul  if:mul  
      problem:
       Equations#:
        plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
        plusAC(x4,x5) -> plusAC(x5,x4)
        appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
        appAC(x4,x5) -> appAC(x5,x4)
        plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
        plusAC(x5,x4) -> plusAC(x4,x5)
        appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
        appAC(x5,x4) -> appAC(x4,x5)
       DPs:
        
       Equations:
        plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
        plusAC(x4,x5) -> plusAC(x5,x4)
        appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
        appAC(x4,x5) -> appAC(x5,x4)
        plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
        plusAC(x5,x4) -> plusAC(x4,x5)
        appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
        appAC(x5,x4) -> appAC(x4,x5)
       TRS:
        if(true(),x,y) -> x
        if(false(),x,y) -> y
        eq(0(),0()) -> true()
        eq(0(),s(x)) -> false()
        eq(s(x),s(y)) -> eq(x,y)
        plusAC(empty(),x) -> x
        appAC(x,empty()) -> empty()
        appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
        appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
        appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
        appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
       S:
        plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14)
        plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15)
        appAC(appAC(x13,x14),x15) -> appAC(x13,x14)
        appAC(x13,appAC(x14,x15)) -> appAC(x14,x15)
      Qed
    
    Equations#:
     plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
     plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
     app{AC,#}(appAC(x4,x5),x6) -> app{AC,#}(x4,appAC(x5,x6))
     app{AC,#}(x4,x5) -> app{AC,#}(x5,x4)
     plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
     plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
     app{AC,#}(x4,appAC(x5,x6)) -> app{AC,#}(appAC(x4,x5),x6)
     app{AC,#}(x5,x4) -> app{AC,#}(x4,x5)
    DPs:
     plus{AC,#}(x7,plusAC(empty(),x)) -> plus{AC,#}(x7,x)
    Equations:
     plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
     plusAC(x4,x5) -> plusAC(x5,x4)
     appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
     appAC(x4,x5) -> appAC(x5,x4)
     plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
     plusAC(x5,x4) -> plusAC(x4,x5)
     appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
     appAC(x5,x4) -> appAC(x4,x5)
    TRS:
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     plusAC(empty(),x) -> x
     appAC(x,empty()) -> empty()
     appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
     appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
     appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
     appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
    S:
     plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
     plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
     app{AC,#}(appAC(x13,x14),x15) -> app{AC,#}(x13,x14)
     app{AC,#}(x13,appAC(x14,x15)) -> app{AC,#}(x14,x15)
    AC-DP unlabeling:
     Equations#:
      plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
      plusAC(x4,x5) -> plusAC(x5,x4)
      appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
      appAC(x4,x5) -> appAC(x5,x4)
      plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
      plusAC(x5,x4) -> plusAC(x4,x5)
      appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
      appAC(x5,x4) -> appAC(x4,x5)
     DPs:
      plusAC(x7,plusAC(empty(),x)) -> plusAC(x7,x)
     Equations:
      plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
      plusAC(x4,x5) -> plusAC(x5,x4)
      appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
      appAC(x4,x5) -> appAC(x5,x4)
      plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
      plusAC(x5,x4) -> plusAC(x4,x5)
      appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
      appAC(x5,x4) -> appAC(x4,x5)
     TRS:
      if(true(),x,y) -> x
      if(false(),x,y) -> y
      eq(0(),0()) -> true()
      eq(0(),s(x)) -> false()
      eq(s(x),s(y)) -> eq(x,y)
      plusAC(empty(),x) -> x
      appAC(x,empty()) -> empty()
      appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
      appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
      appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
      appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
     S:
      plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14)
      plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15)
      appAC(appAC(x13,x14),x15) -> appAC(x13,x14)
      appAC(x13,appAC(x14,x15)) -> appAC(x14,x15)
     Usable Rule Processor:
      Equations#:
       plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
       plusAC(x4,x5) -> plusAC(x5,x4)
       appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
       appAC(x4,x5) -> appAC(x5,x4)
       plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
       plusAC(x5,x4) -> plusAC(x4,x5)
       appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
       appAC(x5,x4) -> appAC(x4,x5)
      DPs:
       plusAC(x7,plusAC(empty(),x)) -> plusAC(x7,x)
      Equations:
       plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
       plusAC(x4,x5) -> plusAC(x5,x4)
       appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
       appAC(x4,x5) -> appAC(x5,x4)
       plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
       plusAC(x5,x4) -> plusAC(x4,x5)
       appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
       appAC(x5,x4) -> appAC(x4,x5)
      TRS:
       plusAC(empty(),x) -> x
      S:
       plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14)
       plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15)
       appAC(appAC(x13,x14),x15) -> appAC(x13,x14)
       appAC(x13,appAC(x14,x15)) -> appAC(x14,x15)
      AC-RPO Processor:
       argument filtering:
        pi(appAC) = []
        pi(plusAC) = [0,1]
        pi(empty) = []
       precedence:
        plusAC > empty > appAC
       status:
        
       problem:
        Equations#:
         plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
         plusAC(x4,x5) -> plusAC(x5,x4)
         appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
         appAC(x4,x5) -> appAC(x5,x4)
         plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
         plusAC(x5,x4) -> plusAC(x4,x5)
         appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
         appAC(x5,x4) -> appAC(x4,x5)
        DPs:
         
        Equations:
         plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
         plusAC(x4,x5) -> plusAC(x5,x4)
         appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
         appAC(x4,x5) -> appAC(x5,x4)
         plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
         plusAC(x5,x4) -> plusAC(x4,x5)
         appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
         appAC(x5,x4) -> appAC(x4,x5)
        TRS:
         plusAC(empty(),x) -> x
        S:
         plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14)
         plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15)
         appAC(appAC(x13,x14),x15) -> appAC(x13,x14)
         appAC(x13,appAC(x14,x15)) -> appAC(x14,x15)
       Qed
    
    Equations#:
     plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
     plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
     app{AC,#}(appAC(x4,x5),x6) -> app{AC,#}(x4,appAC(x5,x6))
     app{AC,#}(x4,x5) -> app{AC,#}(x5,x4)
     plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
     plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
     app{AC,#}(x4,appAC(x5,x6)) -> app{AC,#}(appAC(x4,x5),x6)
     app{AC,#}(x5,x4) -> app{AC,#}(x4,x5)
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
    Equations:
     plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
     plusAC(x4,x5) -> plusAC(x5,x4)
     appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
     appAC(x4,x5) -> appAC(x5,x4)
     plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
     plusAC(x5,x4) -> plusAC(x4,x5)
     appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
     appAC(x5,x4) -> appAC(x4,x5)
    TRS:
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     plusAC(empty(),x) -> x
     appAC(x,empty()) -> empty()
     appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
     appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
     appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
     appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
    S:
     plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
     plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
     app{AC,#}(appAC(x13,x14),x15) -> app{AC,#}(x13,x14)
     app{AC,#}(x13,appAC(x14,x15)) -> app{AC,#}(x14,x15)
    AC-DP unlabeling:
     Equations#:
      plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
      plusAC(x4,x5) -> plusAC(x5,x4)
      appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
      appAC(x4,x5) -> appAC(x5,x4)
      plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
      plusAC(x5,x4) -> plusAC(x4,x5)
      appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
      appAC(x5,x4) -> appAC(x4,x5)
     DPs:
      eq#(s(x),s(y)) -> eq#(x,y)
     Equations:
      plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
      plusAC(x4,x5) -> plusAC(x5,x4)
      appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
      appAC(x4,x5) -> appAC(x5,x4)
      plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
      plusAC(x5,x4) -> plusAC(x4,x5)
      appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
      appAC(x5,x4) -> appAC(x4,x5)
     TRS:
      if(true(),x,y) -> x
      if(false(),x,y) -> y
      eq(0(),0()) -> true()
      eq(0(),s(x)) -> false()
      eq(s(x),s(y)) -> eq(x,y)
      plusAC(empty(),x) -> x
      appAC(x,empty()) -> empty()
      appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
      appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
      appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
      appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
     S:
      plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14)
      plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15)
      appAC(appAC(x13,x14),x15) -> appAC(x13,x14)
      appAC(x13,appAC(x14,x15)) -> appAC(x14,x15)
     Usable Rule Processor:
      Equations#:
       plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
       plusAC(x4,x5) -> plusAC(x5,x4)
       appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
       appAC(x4,x5) -> appAC(x5,x4)
       plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
       plusAC(x5,x4) -> plusAC(x4,x5)
       appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
       appAC(x5,x4) -> appAC(x4,x5)
      DPs:
       eq#(s(x),s(y)) -> eq#(x,y)
      Equations:
       plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
       plusAC(x4,x5) -> plusAC(x5,x4)
       appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
       appAC(x4,x5) -> appAC(x5,x4)
       plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
       plusAC(x5,x4) -> plusAC(x4,x5)
       appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
       appAC(x5,x4) -> appAC(x4,x5)
      TRS:
       
      S:
       plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14)
       plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15)
       appAC(appAC(x13,x14),x15) -> appAC(x13,x14)
       appAC(x13,appAC(x14,x15)) -> appAC(x14,x15)
      AC-RPO Processor:
       argument filtering:
        pi(appAC) = []
        pi(plusAC) = []
        pi(s) = [0]
        pi(eq#) = 1
       precedence:
        eq# > s > plusAC > appAC
       status:
        eq#:mul  
       problem:
        Equations#:
         plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
         plusAC(x4,x5) -> plusAC(x5,x4)
         appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
         appAC(x4,x5) -> appAC(x5,x4)
         plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
         plusAC(x5,x4) -> plusAC(x4,x5)
         appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
         appAC(x5,x4) -> appAC(x4,x5)
        DPs:
         
        Equations:
         plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
         plusAC(x4,x5) -> plusAC(x5,x4)
         appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
         appAC(x4,x5) -> appAC(x5,x4)
         plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
         plusAC(x5,x4) -> plusAC(x4,x5)
         appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
         appAC(x5,x4) -> appAC(x4,x5)
        TRS:
         
        S:
         plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14)
         plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15)
         appAC(appAC(x13,x14),x15) -> appAC(x13,x14)
         appAC(x13,appAC(x14,x15)) -> appAC(x14,x15)
       Qed