YES
Time: 0.031

Problem:
 Equations:
  fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
  fAC(x3,x4) -> fAC(x4,x3)
  fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
  fAC(x4,x3) -> fAC(x3,x4)
 TRS:
  g(0(),fAC(x,x)) -> x
  g(x,s(y)) -> g(fAC(x,y),0())
  g(s(x),y) -> g(fAC(x,y),0())
  g(fAC(x,y),0()) -> fAC(g(x,0()),g(y,0()))

Proof:
 DP Processor:
  Equations#:
   f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5))
   f{AC,#}(x3,x4) -> f{AC,#}(x4,x3)
   f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5)
   f{AC,#}(x4,x3) -> f{AC,#}(x3,x4)
  DPs:
   g#(x,s(y)) -> g#(fAC(x,y),0())
   g#(s(x),y) -> g#(fAC(x,y),0())
   g#(fAC(x,y),0()) -> g#(y,0())
   g#(fAC(x,y),0()) -> g#(x,0())
  Equations:
   fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
   fAC(x3,x4) -> fAC(x4,x3)
   fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
   fAC(x4,x3) -> fAC(x3,x4)
  TRS:
   g(0(),fAC(x,x)) -> x
   g(x,s(y)) -> g(fAC(x,y),0())
   g(s(x),y) -> g(fAC(x,y),0())
   g(fAC(x,y),0()) -> fAC(g(x,0()),g(y,0()))
  S:
   f{AC,#}(fAC(x6,x7),x8) -> f{AC,#}(x6,x7)
   f{AC,#}(x6,fAC(x7,x8)) -> f{AC,#}(x7,x8)
  AC-EDG Processor:
   Equations#:
    f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5))
    f{AC,#}(x3,x4) -> f{AC,#}(x4,x3)
    f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5)
    f{AC,#}(x4,x3) -> f{AC,#}(x3,x4)
   DPs:
    g#(x,s(y)) -> g#(fAC(x,y),0())
    g#(s(x),y) -> g#(fAC(x,y),0())
    g#(fAC(x,y),0()) -> g#(y,0())
    g#(fAC(x,y),0()) -> g#(x,0())
   Equations:
    fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
    fAC(x3,x4) -> fAC(x4,x3)
    fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
    fAC(x4,x3) -> fAC(x3,x4)
   TRS:
    g(0(),fAC(x,x)) -> x
    g(x,s(y)) -> g(fAC(x,y),0())
    g(s(x),y) -> g(fAC(x,y),0())
    g(fAC(x,y),0()) -> fAC(g(x,0()),g(y,0()))
   S:
    f{AC,#}(fAC(x6,x7),x8) -> f{AC,#}(x6,x7)
    f{AC,#}(x6,fAC(x7,x8)) -> f{AC,#}(x7,x8)
   SCC Processor:
    #sccs: 1
    #rules: 3
    #arcs: 10/16
    Equations#:
     f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5))
     f{AC,#}(x3,x4) -> f{AC,#}(x4,x3)
     f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5)
     f{AC,#}(x4,x3) -> f{AC,#}(x3,x4)
    DPs:
     g#(s(x),y) -> g#(fAC(x,y),0())
     g#(fAC(x,y),0()) -> g#(x,0())
     g#(fAC(x,y),0()) -> g#(y,0())
    Equations:
     fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
     fAC(x3,x4) -> fAC(x4,x3)
     fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
     fAC(x4,x3) -> fAC(x3,x4)
    TRS:
     g(0(),fAC(x,x)) -> x
     g(x,s(y)) -> g(fAC(x,y),0())
     g(s(x),y) -> g(fAC(x,y),0())
     g(fAC(x,y),0()) -> fAC(g(x,0()),g(y,0()))
    S:
     f{AC,#}(fAC(x6,x7),x8) -> f{AC,#}(x6,x7)
     f{AC,#}(x6,fAC(x7,x8)) -> f{AC,#}(x7,x8)
    AC-DP unlabeling:
     Equations#:
      fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
      fAC(x3,x4) -> fAC(x4,x3)
      fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
      fAC(x4,x3) -> fAC(x3,x4)
     DPs:
      g#(s(x),y) -> g#(fAC(x,y),0())
      g#(fAC(x,y),0()) -> g#(x,0())
      g#(fAC(x,y),0()) -> g#(y,0())
     Equations:
      fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
      fAC(x3,x4) -> fAC(x4,x3)
      fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
      fAC(x4,x3) -> fAC(x3,x4)
     TRS:
      g(0(),fAC(x,x)) -> x
      g(x,s(y)) -> g(fAC(x,y),0())
      g(s(x),y) -> g(fAC(x,y),0())
      g(fAC(x,y),0()) -> fAC(g(x,0()),g(y,0()))
     S:
      fAC(fAC(x6,x7),x8) -> fAC(x6,x7)
      fAC(x6,fAC(x7,x8)) -> fAC(x7,x8)
     Usable Rule Processor:
      Equations#:
       fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
       fAC(x3,x4) -> fAC(x4,x3)
       fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
       fAC(x4,x3) -> fAC(x3,x4)
      DPs:
       g#(s(x),y) -> g#(fAC(x,y),0())
       g#(fAC(x,y),0()) -> g#(x,0())
       g#(fAC(x,y),0()) -> g#(y,0())
      Equations:
       fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
       fAC(x3,x4) -> fAC(x4,x3)
       fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
       fAC(x4,x3) -> fAC(x3,x4)
      TRS:
       
      S:
       fAC(fAC(x6,x7),x8) -> fAC(x6,x7)
       fAC(x6,fAC(x7,x8)) -> fAC(x7,x8)
      AC-RPO Processor:
       argument filtering:
        pi(fAC) = [0,1]
        pi(0) = []
        pi(s) = [0]
        pi(g#) = [0,1]
       precedence:
        s > g# > 0 > fAC
       status:
        g#:lex  
       problem:
        Equations#:
         fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
         fAC(x3,x4) -> fAC(x4,x3)
         fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
         fAC(x4,x3) -> fAC(x3,x4)
        DPs:
         
        Equations:
         fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
         fAC(x3,x4) -> fAC(x4,x3)
         fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
         fAC(x4,x3) -> fAC(x3,x4)
        TRS:
         
        S:
         fAC(fAC(x6,x7),x8) -> fAC(x6,x7)
         fAC(x6,fAC(x7,x8)) -> fAC(x7,x8)
       Qed