YES
Time: 0.338

Problem:
 Equations:
  plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
  plusAC(x3,x4) -> plusAC(x4,x3)
  plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
  plusAC(x4,x3) -> plusAC(x3,x4)
 TRS:
  minus(x,0()) -> x
  minus(s(x),s(y)) -> minus(x,y)
  minus(minus(x,y),z) -> minus(x,plusAC(y,z))
  quot(0(),s(y)) -> 0()
  quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
  plusAC(0(),y) -> y
  plusAC(s(x),y) -> s(plusAC(x,y))

Proof:
 DP Processor:
  Equations#:
   plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5))
   plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3)
   plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5)
   plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4)
  DPs:
   minus#(s(x),s(y)) -> minus#(x,y)
   minus#(minus(x,y),z) -> plus{AC,#}(y,z)
   minus#(minus(x,y),z) -> minus#(x,plusAC(y,z))
   quot#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
   plus{AC,#}(s(x),y) -> plus{AC,#}(x,y)
   plus{AC,#}(x6,plusAC(0(),y)) -> plus{AC,#}(x6,y)
   plus{AC,#}(x7,plusAC(s(x),y)) -> plus{AC,#}(x,y)
   plus{AC,#}(x7,plusAC(s(x),y)) -> plus{AC,#}(x7,s(plusAC(x,y)))
  Equations:
   plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
   plusAC(x3,x4) -> plusAC(x4,x3)
   plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
   plusAC(x4,x3) -> plusAC(x3,x4)
  TRS:
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   minus(minus(x,y),z) -> minus(x,plusAC(y,z))
   quot(0(),s(y)) -> 0()
   quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
   plusAC(0(),y) -> y
   plusAC(s(x),y) -> s(plusAC(x,y))
  S:
   plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9)
   plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10)
  AC-EDG Processor:
   Equations#:
    plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5))
    plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3)
    plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5)
    plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4)
   DPs:
    minus#(s(x),s(y)) -> minus#(x,y)
    minus#(minus(x,y),z) -> plus{AC,#}(y,z)
    minus#(minus(x,y),z) -> minus#(x,plusAC(y,z))
    quot#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    plus{AC,#}(s(x),y) -> plus{AC,#}(x,y)
    plus{AC,#}(x6,plusAC(0(),y)) -> plus{AC,#}(x6,y)
    plus{AC,#}(x7,plusAC(s(x),y)) -> plus{AC,#}(x,y)
    plus{AC,#}(x7,plusAC(s(x),y)) -> plus{AC,#}(x7,s(plusAC(x,y)))
   Equations:
    plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
    plusAC(x3,x4) -> plusAC(x4,x3)
    plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
    plusAC(x4,x3) -> plusAC(x3,x4)
   TRS:
    minus(x,0()) -> x
    minus(s(x),s(y)) -> minus(x,y)
    minus(minus(x,y),z) -> minus(x,plusAC(y,z))
    quot(0(),s(y)) -> 0()
    quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
    plusAC(0(),y) -> y
    plusAC(s(x),y) -> s(plusAC(x,y))
   S:
    plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9)
    plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10)
   SCC Processor:
    #sccs: 3
    #rules: 7
    #arcs: 31/81
    Equations#:
     plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5))
     plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3)
     plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5)
     plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4)
    DPs:
     quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    Equations:
     plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
     plusAC(x3,x4) -> plusAC(x4,x3)
     plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
     plusAC(x4,x3) -> plusAC(x3,x4)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     minus(minus(x,y),z) -> minus(x,plusAC(y,z))
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     plusAC(0(),y) -> y
     plusAC(s(x),y) -> s(plusAC(x,y))
    S:
     plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9)
     plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10)
    AC-DP unlabeling:
     Equations#:
      plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
      plusAC(x3,x4) -> plusAC(x4,x3)
      plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
      plusAC(x4,x3) -> plusAC(x3,x4)
     DPs:
      quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
     Equations:
      plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
      plusAC(x3,x4) -> plusAC(x4,x3)
      plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
      plusAC(x4,x3) -> plusAC(x3,x4)
     TRS:
      minus(x,0()) -> x
      minus(s(x),s(y)) -> minus(x,y)
      minus(minus(x,y),z) -> minus(x,plusAC(y,z))
      quot(0(),s(y)) -> 0()
      quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
      plusAC(0(),y) -> y
      plusAC(s(x),y) -> s(plusAC(x,y))
     S:
      plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
      plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
     Usable Rule Processor:
      Equations#:
       plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
       plusAC(x3,x4) -> plusAC(x4,x3)
       plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
       plusAC(x4,x3) -> plusAC(x3,x4)
      DPs:
       quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
      Equations:
       plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
       plusAC(x3,x4) -> plusAC(x4,x3)
       plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
       plusAC(x4,x3) -> plusAC(x3,x4)
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       minus(minus(x,y),z) -> minus(x,plusAC(y,z))
       plusAC(0(),y) -> y
       plusAC(s(x),y) -> s(plusAC(x,y))
      S:
       plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
       plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
      AC-KBO Processor:
       argument filtering:
        pi(plusAC) = [0,1]
        pi(0) = []
        pi(minus) = 0
        pi(s) = [0]
        pi(quot#) = 0
       precedence:
        s > quot# ~ minus ~ 0 ~ plusAC
        weight function:
         [quot#](x0, x1) = x0,
         
         [s](x0) = x0 + 1,
         
         [minus](x0, x1) = x0,
         
         [0] = 2,
         
         [plusAC](x0, x1) = x0 + x1
         usable rules:
          minus(x,0()) -> x
          minus(s(x),s(y)) -> minus(x,y)
          minus(minus(x,y),z) -> minus(x,plusAC(y,z))
         problem:
          Equations#:
           plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
           plusAC(x3,x4) -> plusAC(x4,x3)
           plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
           plusAC(x4,x3) -> plusAC(x3,x4)
          DPs:
           
          Equations:
           plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
           plusAC(x3,x4) -> plusAC(x4,x3)
           plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
           plusAC(x4,x3) -> plusAC(x3,x4)
          TRS:
           minus(x,0()) -> x
           minus(s(x),s(y)) -> minus(x,y)
           minus(minus(x,y),z) -> minus(x,plusAC(y,z))
           plusAC(0(),y) -> y
           plusAC(s(x),y) -> s(plusAC(x,y))
          S:
           plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
           plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
         Qed
     
     Equations#:
      plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5))
      plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3)
      plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5)
      plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4)
     DPs:
      minus#(minus(x,y),z) -> minus#(x,plusAC(y,z))
      minus#(s(x),s(y)) -> minus#(x,y)
     Equations:
      plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
      plusAC(x3,x4) -> plusAC(x4,x3)
      plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
      plusAC(x4,x3) -> plusAC(x3,x4)
     TRS:
      minus(x,0()) -> x
      minus(s(x),s(y)) -> minus(x,y)
      minus(minus(x,y),z) -> minus(x,plusAC(y,z))
      quot(0(),s(y)) -> 0()
      quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
      plusAC(0(),y) -> y
      plusAC(s(x),y) -> s(plusAC(x,y))
     S:
      plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9)
      plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10)
     AC-DP unlabeling:
      Equations#:
       plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
       plusAC(x3,x4) -> plusAC(x4,x3)
       plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
       plusAC(x4,x3) -> plusAC(x3,x4)
      DPs:
       minus#(minus(x,y),z) -> minus#(x,plusAC(y,z))
       minus#(s(x),s(y)) -> minus#(x,y)
      Equations:
       plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
       plusAC(x3,x4) -> plusAC(x4,x3)
       plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
       plusAC(x4,x3) -> plusAC(x3,x4)
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       minus(minus(x,y),z) -> minus(x,plusAC(y,z))
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       plusAC(0(),y) -> y
       plusAC(s(x),y) -> s(plusAC(x,y))
      S:
       plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
       plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
      Usable Rule Processor:
       Equations#:
        plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
        plusAC(x3,x4) -> plusAC(x4,x3)
        plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
        plusAC(x4,x3) -> plusAC(x3,x4)
       DPs:
        minus#(minus(x,y),z) -> minus#(x,plusAC(y,z))
        minus#(s(x),s(y)) -> minus#(x,y)
       Equations:
        plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
        plusAC(x3,x4) -> plusAC(x4,x3)
        plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
        plusAC(x4,x3) -> plusAC(x3,x4)
       TRS:
        plusAC(0(),y) -> y
        plusAC(s(x),y) -> s(plusAC(x,y))
       S:
        plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
        plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
       AC-KBO Processor:
        argument filtering:
         pi(plusAC) = [0,1]
         pi(0) = []
         pi(minus) = 0
         pi(s) = [0]
         pi(minus#) = 0
        precedence:
         minus > minus# ~ s ~ 0 ~ plusAC
         weight function:
          [minus#](x0, x1) = x0,
          
          [s](x0) = 3x0 + 5,
          
          [minus](x0, x1) = x0,
          
          [0] = 1,
          
          [plusAC](x0, x1) = x0 + x1 + 1
          usable rules:
           
          problem:
           Equations#:
            plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
            plusAC(x3,x4) -> plusAC(x4,x3)
            plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
            plusAC(x4,x3) -> plusAC(x3,x4)
           DPs:
            minus#(minus(x,y),z) -> minus#(x,plusAC(y,z))
           Equations:
            plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
            plusAC(x3,x4) -> plusAC(x4,x3)
            plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
            plusAC(x4,x3) -> plusAC(x3,x4)
           TRS:
            plusAC(0(),y) -> y
            plusAC(s(x),y) -> s(plusAC(x,y))
           S:
            plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
            plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
          Restore Modifier:
           Equations#:
            plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
            plusAC(x3,x4) -> plusAC(x4,x3)
            plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
            plusAC(x4,x3) -> plusAC(x3,x4)
           DPs:
            minus#(minus(x,y),z) -> minus#(x,plusAC(y,z))
           Equations:
            plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
            plusAC(x3,x4) -> plusAC(x4,x3)
            plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
            plusAC(x4,x3) -> plusAC(x3,x4)
           TRS:
            plusAC(0(),y) -> y
            plusAC(s(x),y) -> s(plusAC(x,y))
           S:
            plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
            plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
           AC-DP unlabeling:
            Equations#:
             plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
             plusAC(x3,x4) -> plusAC(x4,x3)
             plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
             plusAC(x4,x3) -> plusAC(x3,x4)
            DPs:
             minus#(minus(x,y),z) -> minus#(x,plusAC(y,z))
            Equations:
             plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
             plusAC(x3,x4) -> plusAC(x4,x3)
             plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
             plusAC(x4,x3) -> plusAC(x3,x4)
            TRS:
             plusAC(0(),y) -> y
             plusAC(s(x),y) -> s(plusAC(x,y))
            S:
             plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
             plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
            AC-KBO Processor:
             argument filtering:
              pi(plusAC) = [0,1]
              pi(0) = []
              pi(minus) = [0]
              pi(s) = []
              pi(minus#) = 0
             precedence:
              minus# > s > minus ~ 0 ~ plusAC
              weight function:
               [minus#](x0, x1) = x0,
               
               [s](x0) = 4,
               
               [minus](x0, x1) = 4x0 + 4,
               
               [0] = 2,
               
               [plusAC](x0, x1) = x0 + x1 + 5
               usable rules:
                
               problem:
                Equations#:
                 plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
                 plusAC(x3,x4) -> plusAC(x4,x3)
                 plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
                 plusAC(x4,x3) -> plusAC(x3,x4)
                DPs:
                 
                Equations:
                 plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
                 plusAC(x3,x4) -> plusAC(x4,x3)
                 plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
                 plusAC(x4,x3) -> plusAC(x3,x4)
                TRS:
                 plusAC(0(),y) -> y
                 plusAC(s(x),y) -> s(plusAC(x,y))
                S:
                 plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
                 plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
               Qed
      
      Equations#:
       plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5))
       plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3)
       plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5)
       plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4)
      DPs:
       plus{AC,#}(x7,plusAC(s(x),y)) -> plus{AC,#}(x7,s(plusAC(x,y)))
       plus{AC,#}(x7,plusAC(s(x),y)) -> plus{AC,#}(x,y)
       plus{AC,#}(x6,plusAC(0(),y)) -> plus{AC,#}(x6,y)
       plus{AC,#}(s(x),y) -> plus{AC,#}(x,y)
      Equations:
       plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
       plusAC(x3,x4) -> plusAC(x4,x3)
       plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
       plusAC(x4,x3) -> plusAC(x3,x4)
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       minus(minus(x,y),z) -> minus(x,plusAC(y,z))
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       plusAC(0(),y) -> y
       plusAC(s(x),y) -> s(plusAC(x,y))
      S:
       plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9)
       plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10)
      AC-DP unlabeling:
       Equations#:
        plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
        plusAC(x3,x4) -> plusAC(x4,x3)
        plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
        plusAC(x4,x3) -> plusAC(x3,x4)
       DPs:
        plusAC(x7,plusAC(s(x),y)) -> plusAC(x7,s(plusAC(x,y)))
        plusAC(x7,plusAC(s(x),y)) -> plusAC(x,y)
        plusAC(x6,plusAC(0(),y)) -> plusAC(x6,y)
        plusAC(s(x),y) -> plusAC(x,y)
       Equations:
        plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
        plusAC(x3,x4) -> plusAC(x4,x3)
        plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
        plusAC(x4,x3) -> plusAC(x3,x4)
       TRS:
        minus(x,0()) -> x
        minus(s(x),s(y)) -> minus(x,y)
        minus(minus(x,y),z) -> minus(x,plusAC(y,z))
        quot(0(),s(y)) -> 0()
        quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
        plusAC(0(),y) -> y
        plusAC(s(x),y) -> s(plusAC(x,y))
       S:
        plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
        plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
       Usable Rule Processor:
        Equations#:
         plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
         plusAC(x3,x4) -> plusAC(x4,x3)
         plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
         plusAC(x4,x3) -> plusAC(x3,x4)
        DPs:
         plusAC(x7,plusAC(s(x),y)) -> plusAC(x7,s(plusAC(x,y)))
         plusAC(x7,plusAC(s(x),y)) -> plusAC(x,y)
         plusAC(x6,plusAC(0(),y)) -> plusAC(x6,y)
         plusAC(s(x),y) -> plusAC(x,y)
        Equations:
         plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
         plusAC(x3,x4) -> plusAC(x4,x3)
         plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
         plusAC(x4,x3) -> plusAC(x3,x4)
        TRS:
         plusAC(0(),y) -> y
         plusAC(s(x),y) -> s(plusAC(x,y))
        S:
         plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
         plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
        AC-KBO Processor:
         argument filtering:
          pi(plusAC) = [0,1]
          pi(0) = []
          pi(s) = [0]
         precedence:
          plusAC > s ~ 0
          weight function:
           [s](x0) = x0 + 7,
           
           [0] = 3,
           
           [plusAC](x0, x1) = x0 + x1 + 1
           usable rules:
            plusAC(0(),y) -> y
            plusAC(s(x),y) -> s(plusAC(x,y))
           problem:
            Equations#:
             plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
             plusAC(x3,x4) -> plusAC(x4,x3)
             plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
             plusAC(x4,x3) -> plusAC(x3,x4)
            DPs:
             
            Equations:
             plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
             plusAC(x3,x4) -> plusAC(x4,x3)
             plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
             plusAC(x4,x3) -> plusAC(x3,x4)
            TRS:
             plusAC(0(),y) -> y
             plusAC(s(x),y) -> s(plusAC(x,y))
            S:
             plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9)
             plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10)
           Qed