YES
Time: 0.354

Problem:
 Equations:
  +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
  +AC(x3,x4) -> +AC(x4,x3)
  +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
  +AC(x4,x3) -> +AC(x3,x4)
 TRS:
  +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
  k(a(),g(g(a()))) -> k(g(a()),f(a()))
  +AC(g(x),y) -> g(+AC(x,y))
  f(+AC(x,y)) -> +AC(f(x),y)
  k(a(),b()) -> k(b(),a())
  k(g(a()),a()) -> k(a(),g(b()))
  k(g(a()),b()) -> k(a(),g(a()))

Proof:
 DP Processor:
  Equations#:
   +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5))
   +{AC,#}(x3,x4) -> +{AC,#}(x4,x3)
   +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5)
   +{AC,#}(x4,x3) -> +{AC,#}(x3,x4)
  DPs:
   +{AC,#}(f(b()),g(a())) -> f#(a())
   +{AC,#}(f(b()),g(a())) -> +{AC,#}(f(a()),g(b()))
   k#(a(),g(g(a()))) -> f#(a())
   k#(a(),g(g(a()))) -> k#(g(a()),f(a()))
   +{AC,#}(g(x),y) -> +{AC,#}(x,y)
   f#(+AC(x,y)) -> f#(x)
   f#(+AC(x,y)) -> +{AC,#}(f(x),y)
   k#(a(),b()) -> k#(b(),a())
   k#(g(a()),a()) -> k#(a(),g(b()))
   k#(g(a()),b()) -> k#(a(),g(a()))
   +{AC,#}(x6,+AC(f(b()),g(a()))) -> f#(a())
   +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(f(a()),g(b()))
   +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(x6,+AC(f(a()),g(b())))
   +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x,y)
   +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x7,g(+AC(x,y)))
  Equations:
   +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
   +AC(x3,x4) -> +AC(x4,x3)
   +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
   +AC(x4,x3) -> +AC(x3,x4)
  TRS:
   +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
   k(a(),g(g(a()))) -> k(g(a()),f(a()))
   +AC(g(x),y) -> g(+AC(x,y))
   f(+AC(x,y)) -> +AC(f(x),y)
   k(a(),b()) -> k(b(),a())
   k(g(a()),a()) -> k(a(),g(b()))
   k(g(a()),b()) -> k(a(),g(a()))
  S:
   +{AC,#}(+AC(x8,x9),x10) -> +{AC,#}(x8,x9)
   +{AC,#}(x8,+AC(x9,x10)) -> +{AC,#}(x9,x10)
  AC-EDG Processor:
   Equations#:
    +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5))
    +{AC,#}(x3,x4) -> +{AC,#}(x4,x3)
    +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5)
    +{AC,#}(x4,x3) -> +{AC,#}(x3,x4)
   DPs:
    +{AC,#}(f(b()),g(a())) -> f#(a())
    +{AC,#}(f(b()),g(a())) -> +{AC,#}(f(a()),g(b()))
    k#(a(),g(g(a()))) -> f#(a())
    k#(a(),g(g(a()))) -> k#(g(a()),f(a()))
    +{AC,#}(g(x),y) -> +{AC,#}(x,y)
    f#(+AC(x,y)) -> f#(x)
    f#(+AC(x,y)) -> +{AC,#}(f(x),y)
    k#(a(),b()) -> k#(b(),a())
    k#(g(a()),a()) -> k#(a(),g(b()))
    k#(g(a()),b()) -> k#(a(),g(a()))
    +{AC,#}(x6,+AC(f(b()),g(a()))) -> f#(a())
    +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(f(a()),g(b()))
    +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(x6,+AC(f(a()),g(b())))
    +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x,y)
    +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x7,g(+AC(x,y)))
   Equations:
    +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
    +AC(x3,x4) -> +AC(x4,x3)
    +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
    +AC(x4,x3) -> +AC(x3,x4)
   TRS:
    +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
    k(a(),g(g(a()))) -> k(g(a()),f(a()))
    +AC(g(x),y) -> g(+AC(x,y))
    f(+AC(x,y)) -> +AC(f(x),y)
    k(a(),b()) -> k(b(),a())
    k(g(a()),a()) -> k(a(),g(b()))
    k(g(a()),b()) -> k(a(),g(a()))
   S:
    +{AC,#}(+AC(x8,x9),x10) -> +{AC,#}(x8,x9)
    +{AC,#}(x8,+AC(x9,x10)) -> +{AC,#}(x9,x10)
   SCC Processor:
    #sccs: 2
    #rules: 7
    #arcs: 56/225
    Equations#:
     +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5))
     +{AC,#}(x3,x4) -> +{AC,#}(x4,x3)
     +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5)
     +{AC,#}(x4,x3) -> +{AC,#}(x3,x4)
    DPs:
     f#(+AC(x,y)) -> f#(x)
    Equations:
     +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
     +AC(x3,x4) -> +AC(x4,x3)
     +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
     +AC(x4,x3) -> +AC(x3,x4)
    TRS:
     +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
     k(a(),g(g(a()))) -> k(g(a()),f(a()))
     +AC(g(x),y) -> g(+AC(x,y))
     f(+AC(x,y)) -> +AC(f(x),y)
     k(a(),b()) -> k(b(),a())
     k(g(a()),a()) -> k(a(),g(b()))
     k(g(a()),b()) -> k(a(),g(a()))
    S:
     +{AC,#}(+AC(x8,x9),x10) -> +{AC,#}(x8,x9)
     +{AC,#}(x8,+AC(x9,x10)) -> +{AC,#}(x9,x10)
    AC-DP unlabeling:
     Equations#:
      +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
      +AC(x3,x4) -> +AC(x4,x3)
      +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
      +AC(x4,x3) -> +AC(x3,x4)
     DPs:
      f#(+AC(x,y)) -> f#(x)
     Equations:
      +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
      +AC(x3,x4) -> +AC(x4,x3)
      +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
      +AC(x4,x3) -> +AC(x3,x4)
     TRS:
      +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
      k(a(),g(g(a()))) -> k(g(a()),f(a()))
      +AC(g(x),y) -> g(+AC(x,y))
      f(+AC(x,y)) -> +AC(f(x),y)
      k(a(),b()) -> k(b(),a())
      k(g(a()),a()) -> k(a(),g(b()))
      k(g(a()),b()) -> k(a(),g(a()))
     S:
      +AC(+AC(x8,x9),x10) -> +AC(x8,x9)
      +AC(x8,+AC(x9,x10)) -> +AC(x9,x10)
     Usable Rule Processor:
      Equations#:
       +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
       +AC(x3,x4) -> +AC(x4,x3)
       +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
       +AC(x4,x3) -> +AC(x3,x4)
      DPs:
       f#(+AC(x,y)) -> f#(x)
      Equations:
       +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
       +AC(x3,x4) -> +AC(x4,x3)
       +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
       +AC(x4,x3) -> +AC(x3,x4)
      TRS:
       
      S:
       +AC(+AC(x8,x9),x10) -> +AC(x8,x9)
       +AC(x8,+AC(x9,x10)) -> +AC(x9,x10)
      AC-KBO Processor:
       argument filtering:
        pi(+AC) = [0,1]
        pi(f#) = 0
       precedence:
        f# ~ +AC
        weight function:
         w0 = 7
         w(f#) = 7
         w(+AC) = 5
         usable rules:
          
         problem:
          Equations#:
           +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
           +AC(x3,x4) -> +AC(x4,x3)
           +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
           +AC(x4,x3) -> +AC(x3,x4)
          DPs:
           
          Equations:
           +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
           +AC(x3,x4) -> +AC(x4,x3)
           +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
           +AC(x4,x3) -> +AC(x3,x4)
          TRS:
           
          S:
           +AC(+AC(x8,x9),x10) -> +AC(x8,x9)
           +AC(x8,+AC(x9,x10)) -> +AC(x9,x10)
         Qed
     
     Equations#:
      +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5))
      +{AC,#}(x3,x4) -> +{AC,#}(x4,x3)
      +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5)
      +{AC,#}(x4,x3) -> +{AC,#}(x3,x4)
     DPs:
      +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x7,g(+AC(x,y)))
      +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x,y)
      +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(x6,+AC(f(a()),g(b())))
      +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(f(a()),g(b()))
      +{AC,#}(g(x),y) -> +{AC,#}(x,y)
      +{AC,#}(f(b()),g(a())) -> +{AC,#}(f(a()),g(b()))
     Equations:
      +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
      +AC(x3,x4) -> +AC(x4,x3)
      +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
      +AC(x4,x3) -> +AC(x3,x4)
     TRS:
      +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
      k(a(),g(g(a()))) -> k(g(a()),f(a()))
      +AC(g(x),y) -> g(+AC(x,y))
      f(+AC(x,y)) -> +AC(f(x),y)
      k(a(),b()) -> k(b(),a())
      k(g(a()),a()) -> k(a(),g(b()))
      k(g(a()),b()) -> k(a(),g(a()))
     S:
      +{AC,#}(+AC(x8,x9),x10) -> +{AC,#}(x8,x9)
      +{AC,#}(x8,+AC(x9,x10)) -> +{AC,#}(x9,x10)
     AC-DP unlabeling:
      Equations#:
       +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
       +AC(x3,x4) -> +AC(x4,x3)
       +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
       +AC(x4,x3) -> +AC(x3,x4)
      DPs:
       +AC(x7,+AC(g(x),y)) -> +AC(x7,g(+AC(x,y)))
       +AC(x7,+AC(g(x),y)) -> +AC(x,y)
       +AC(x6,+AC(f(b()),g(a()))) -> +AC(x6,+AC(f(a()),g(b())))
       +AC(x6,+AC(f(b()),g(a()))) -> +AC(f(a()),g(b()))
       +AC(g(x),y) -> +AC(x,y)
       +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
      Equations:
       +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
       +AC(x3,x4) -> +AC(x4,x3)
       +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
       +AC(x4,x3) -> +AC(x3,x4)
      TRS:
       +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
       k(a(),g(g(a()))) -> k(g(a()),f(a()))
       +AC(g(x),y) -> g(+AC(x,y))
       f(+AC(x,y)) -> +AC(f(x),y)
       k(a(),b()) -> k(b(),a())
       k(g(a()),a()) -> k(a(),g(b()))
       k(g(a()),b()) -> k(a(),g(a()))
      S:
       +AC(+AC(x8,x9),x10) -> +AC(x8,x9)
       +AC(x8,+AC(x9,x10)) -> +AC(x9,x10)
      Usable Rule Processor:
       Equations#:
        +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
        +AC(x3,x4) -> +AC(x4,x3)
        +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
        +AC(x4,x3) -> +AC(x3,x4)
       DPs:
        +AC(x7,+AC(g(x),y)) -> +AC(x7,g(+AC(x,y)))
        +AC(x7,+AC(g(x),y)) -> +AC(x,y)
        +AC(x6,+AC(f(b()),g(a()))) -> +AC(x6,+AC(f(a()),g(b())))
        +AC(x6,+AC(f(b()),g(a()))) -> +AC(f(a()),g(b()))
        +AC(g(x),y) -> +AC(x,y)
        +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
       Equations:
        +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
        +AC(x3,x4) -> +AC(x4,x3)
        +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
        +AC(x4,x3) -> +AC(x3,x4)
       TRS:
        +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
        +AC(g(x),y) -> g(+AC(x,y))
       S:
        +AC(+AC(x8,x9),x10) -> +AC(x8,x9)
        +AC(x8,+AC(x9,x10)) -> +AC(x9,x10)
       AC-KBO Processor:
        argument filtering:
         pi(+AC) = [0,1]
         pi(b) = []
         pi(f) = []
         pi(a) = []
         pi(g) = [0]
        precedence:
         a ~ b > +AC > g > f
         weight function:
          w0 = 2
          w(f) = 7
          w(+AC) = 6
          w(a) = 4
          w(b) = 2
          w(g) = 1
          usable rules:
           +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
           +AC(g(x),y) -> g(+AC(x,y))
          problem:
           Equations#:
            +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
            +AC(x3,x4) -> +AC(x4,x3)
            +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
            +AC(x4,x3) -> +AC(x3,x4)
           DPs:
            
           Equations:
            +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
            +AC(x3,x4) -> +AC(x4,x3)
            +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
            +AC(x4,x3) -> +AC(x3,x4)
           TRS:
            +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
            +AC(g(x),y) -> g(+AC(x,y))
           S:
            +AC(+AC(x8,x9),x10) -> +AC(x8,x9)
            +AC(x8,+AC(x9,x10)) -> +AC(x9,x10)
          Qed