YES
Time: 0.106

Problem:
 Equations:
  plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
  plusAC(x2,x3) -> plusAC(x3,x2)
  plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
  plusAC(x3,x2) -> plusAC(x2,x3)
 TRS:
  minus(plusAC(x,y),y) -> x
  dix(zero(),s(y)) -> 0()
  div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
  plusAC(0(),x) -> x
  plusAC(s(x),y) -> s(plusAC(x,y))

Proof:
 DP Processor:
  Equations#:
   plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4))
   plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2)
   plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4)
   plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3)
  DPs:
   div#(s(x),s(y)) -> minus#(x,y)
   div#(s(x),s(y)) -> div#(minus(x,y),s(y))
   plus{AC,#}(s(x),y) -> plus{AC,#}(x,y)
   plus{AC,#}(x5,plusAC(0(),x)) -> plus{AC,#}(x5,x)
   plus{AC,#}(x6,plusAC(s(x),y)) -> plus{AC,#}(x,y)
   plus{AC,#}(x6,plusAC(s(x),y)) -> plus{AC,#}(x6,s(plusAC(x,y)))
  Equations:
   plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
   plusAC(x2,x3) -> plusAC(x3,x2)
   plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
   plusAC(x3,x2) -> plusAC(x2,x3)
  TRS:
   minus(plusAC(x,y),y) -> x
   dix(zero(),s(y)) -> 0()
   div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
   plusAC(0(),x) -> x
   plusAC(s(x),y) -> s(plusAC(x,y))
  S:
   plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,x8)
   plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(x8,x9)
  AC-EDG Processor:
   Equations#:
    plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4))
    plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2)
    plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4)
    plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3)
   DPs:
    div#(s(x),s(y)) -> minus#(x,y)
    div#(s(x),s(y)) -> div#(minus(x,y),s(y))
    plus{AC,#}(s(x),y) -> plus{AC,#}(x,y)
    plus{AC,#}(x5,plusAC(0(),x)) -> plus{AC,#}(x5,x)
    plus{AC,#}(x6,plusAC(s(x),y)) -> plus{AC,#}(x,y)
    plus{AC,#}(x6,plusAC(s(x),y)) -> plus{AC,#}(x6,s(plusAC(x,y)))
   Equations:
    plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
    plusAC(x2,x3) -> plusAC(x3,x2)
    plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
    plusAC(x3,x2) -> plusAC(x2,x3)
   TRS:
    minus(plusAC(x,y),y) -> x
    dix(zero(),s(y)) -> 0()
    div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
    plusAC(0(),x) -> x
    plusAC(s(x),y) -> s(plusAC(x,y))
   S:
    plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,x8)
    plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(x8,x9)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 18/36
    Equations#:
     plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4))
     plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2)
     plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4)
     plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3)
    DPs:
     div#(s(x),s(y)) -> div#(minus(x,y),s(y))
    Equations:
     plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
     plusAC(x2,x3) -> plusAC(x3,x2)
     plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
     plusAC(x3,x2) -> plusAC(x2,x3)
    TRS:
     minus(plusAC(x,y),y) -> x
     dix(zero(),s(y)) -> 0()
     div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
     plusAC(0(),x) -> x
     plusAC(s(x),y) -> s(plusAC(x,y))
    S:
     plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,x8)
     plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(x8,x9)
    AC-DP unlabeling:
     Equations#:
      plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
      plusAC(x2,x3) -> plusAC(x3,x2)
      plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
      plusAC(x3,x2) -> plusAC(x2,x3)
     DPs:
      div#(s(x),s(y)) -> div#(minus(x,y),s(y))
     Equations:
      plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
      plusAC(x2,x3) -> plusAC(x3,x2)
      plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
      plusAC(x3,x2) -> plusAC(x2,x3)
     TRS:
      minus(plusAC(x,y),y) -> x
      dix(zero(),s(y)) -> 0()
      div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
      plusAC(0(),x) -> x
      plusAC(s(x),y) -> s(plusAC(x,y))
     S:
      plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8)
      plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9)
     Usable Rule Processor:
      Equations#:
       plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
       plusAC(x2,x3) -> plusAC(x3,x2)
       plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
       plusAC(x3,x2) -> plusAC(x2,x3)
      DPs:
       div#(s(x),s(y)) -> div#(minus(x,y),s(y))
      Equations:
       plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
       plusAC(x2,x3) -> plusAC(x3,x2)
       plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
       plusAC(x3,x2) -> plusAC(x2,x3)
      TRS:
       minus(plusAC(x,y),y) -> x
      S:
       plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8)
       plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9)
      AC-KBO Processor:
       argument filtering:
        pi(plusAC) = [0,1]
        pi(minus) = 0
        pi(s) = [0]
        pi(div#) = 0
       precedence:
        div# ~ s ~ minus ~ plusAC
        weight function:
         w0 = 4
         w(minus) = w(plusAC) = 4
         w(div#) = 2
         w(s) = 1
         usable rules:
          minus(plusAC(x,y),y) -> x
         problem:
          Equations#:
           plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
           plusAC(x2,x3) -> plusAC(x3,x2)
           plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
           plusAC(x3,x2) -> plusAC(x2,x3)
          DPs:
           
          Equations:
           plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
           plusAC(x2,x3) -> plusAC(x3,x2)
           plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
           plusAC(x3,x2) -> plusAC(x2,x3)
          TRS:
           minus(plusAC(x,y),y) -> x
          S:
           plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8)
           plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9)
         Qed
     
     Equations#:
      plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4))
      plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2)
      plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4)
      plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3)
     DPs:
      plus{AC,#}(s(x),y) -> plus{AC,#}(x,y)
      plus{AC,#}(x6,plusAC(s(x),y)) -> plus{AC,#}(x6,s(plusAC(x,y)))
      plus{AC,#}(x6,plusAC(s(x),y)) -> plus{AC,#}(x,y)
      plus{AC,#}(x5,plusAC(0(),x)) -> plus{AC,#}(x5,x)
     Equations:
      plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
      plusAC(x2,x3) -> plusAC(x3,x2)
      plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
      plusAC(x3,x2) -> plusAC(x2,x3)
     TRS:
      minus(plusAC(x,y),y) -> x
      dix(zero(),s(y)) -> 0()
      div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
      plusAC(0(),x) -> x
      plusAC(s(x),y) -> s(plusAC(x,y))
     S:
      plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,x8)
      plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(x8,x9)
     AC-DP unlabeling:
      Equations#:
       plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
       plusAC(x2,x3) -> plusAC(x3,x2)
       plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
       plusAC(x3,x2) -> plusAC(x2,x3)
      DPs:
       plusAC(s(x),y) -> plusAC(x,y)
       plusAC(x6,plusAC(s(x),y)) -> plusAC(x6,s(plusAC(x,y)))
       plusAC(x6,plusAC(s(x),y)) -> plusAC(x,y)
       plusAC(x5,plusAC(0(),x)) -> plusAC(x5,x)
      Equations:
       plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
       plusAC(x2,x3) -> plusAC(x3,x2)
       plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
       plusAC(x3,x2) -> plusAC(x2,x3)
      TRS:
       minus(plusAC(x,y),y) -> x
       dix(zero(),s(y)) -> 0()
       div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
       plusAC(0(),x) -> x
       plusAC(s(x),y) -> s(plusAC(x,y))
      S:
       plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8)
       plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9)
      Usable Rule Processor:
       Equations#:
        plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
        plusAC(x2,x3) -> plusAC(x3,x2)
        plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
        plusAC(x3,x2) -> plusAC(x2,x3)
       DPs:
        plusAC(s(x),y) -> plusAC(x,y)
        plusAC(x6,plusAC(s(x),y)) -> plusAC(x6,s(plusAC(x,y)))
        plusAC(x6,plusAC(s(x),y)) -> plusAC(x,y)
        plusAC(x5,plusAC(0(),x)) -> plusAC(x5,x)
       Equations:
        plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
        plusAC(x2,x3) -> plusAC(x3,x2)
        plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
        plusAC(x3,x2) -> plusAC(x2,x3)
       TRS:
        plusAC(0(),x) -> x
        plusAC(s(x),y) -> s(plusAC(x,y))
       S:
        plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8)
        plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9)
       AC-KBO Processor:
        argument filtering:
         pi(plusAC) = [0,1]
         pi(s) = [0]
         pi(0) = []
        precedence:
         0 ~ plusAC > s
         weight function:
          w0 = 4
          w(0) = 5
          w(s) = 4
          w(plusAC) = 0
          usable rules:
           plusAC(0(),x) -> x
           plusAC(s(x),y) -> s(plusAC(x,y))
          problem:
           Equations#:
            plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
            plusAC(x2,x3) -> plusAC(x3,x2)
            plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
            plusAC(x3,x2) -> plusAC(x2,x3)
           DPs:
            
           Equations:
            plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
            plusAC(x2,x3) -> plusAC(x3,x2)
            plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
            plusAC(x3,x2) -> plusAC(x2,x3)
           TRS:
            plusAC(0(),x) -> x
            plusAC(s(x),y) -> s(plusAC(x,y))
           S:
            plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8)
            plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9)
          Qed