YES
Time: 0.061

Problem:
 Equations:
  fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
  fAC(x2,x3) -> fAC(x3,x2)
  fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
  fAC(x3,x2) -> fAC(x2,x3)
 TRS:
  fAC(x,one()) -> x
  fAC(i(x),x) -> one()
  g(one()) -> one()
  g(fAC(x,y)) -> fAC(g(x),g(y))

Proof:
 DP Processor:
  Equations#:
   f{AC,#}(fAC(x2,x3),x4) -> f{AC,#}(x2,fAC(x3,x4))
   f{AC,#}(x2,x3) -> f{AC,#}(x3,x2)
   f{AC,#}(x2,fAC(x3,x4)) -> f{AC,#}(fAC(x2,x3),x4)
   f{AC,#}(x3,x2) -> f{AC,#}(x2,x3)
  DPs:
   g#(fAC(x,y)) -> g#(y)
   g#(fAC(x,y)) -> g#(x)
   g#(fAC(x,y)) -> f{AC,#}(g(x),g(y))
   f{AC,#}(x5,fAC(x,one())) -> f{AC,#}(x5,x)
   f{AC,#}(x6,fAC(i(x),x)) -> f{AC,#}(x6,one())
  Equations:
   fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
   fAC(x2,x3) -> fAC(x3,x2)
   fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
   fAC(x3,x2) -> fAC(x2,x3)
  TRS:
   fAC(x,one()) -> x
   fAC(i(x),x) -> one()
   g(one()) -> one()
   g(fAC(x,y)) -> fAC(g(x),g(y))
  S:
   f{AC,#}(fAC(x7,x8),x9) -> f{AC,#}(x7,x8)
   f{AC,#}(x7,fAC(x8,x9)) -> f{AC,#}(x8,x9)
  AC-EDG Processor:
   Equations#:
    f{AC,#}(fAC(x2,x3),x4) -> f{AC,#}(x2,fAC(x3,x4))
    f{AC,#}(x2,x3) -> f{AC,#}(x3,x2)
    f{AC,#}(x2,fAC(x3,x4)) -> f{AC,#}(fAC(x2,x3),x4)
    f{AC,#}(x3,x2) -> f{AC,#}(x2,x3)
   DPs:
    g#(fAC(x,y)) -> g#(y)
    g#(fAC(x,y)) -> g#(x)
    g#(fAC(x,y)) -> f{AC,#}(g(x),g(y))
    f{AC,#}(x5,fAC(x,one())) -> f{AC,#}(x5,x)
    f{AC,#}(x6,fAC(i(x),x)) -> f{AC,#}(x6,one())
   Equations:
    fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
    fAC(x2,x3) -> fAC(x3,x2)
    fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
    fAC(x3,x2) -> fAC(x2,x3)
   TRS:
    fAC(x,one()) -> x
    fAC(i(x),x) -> one()
    g(one()) -> one()
    g(fAC(x,y)) -> fAC(g(x),g(y))
   S:
    f{AC,#}(fAC(x7,x8),x9) -> f{AC,#}(x7,x8)
    f{AC,#}(x7,fAC(x8,x9)) -> f{AC,#}(x8,x9)
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 12/25
    Equations#:
     f{AC,#}(fAC(x2,x3),x4) -> f{AC,#}(x2,fAC(x3,x4))
     f{AC,#}(x2,x3) -> f{AC,#}(x3,x2)
     f{AC,#}(x2,fAC(x3,x4)) -> f{AC,#}(fAC(x2,x3),x4)
     f{AC,#}(x3,x2) -> f{AC,#}(x2,x3)
    DPs:
     g#(fAC(x,y)) -> g#(y)
     g#(fAC(x,y)) -> g#(x)
    Equations:
     fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
     fAC(x2,x3) -> fAC(x3,x2)
     fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
     fAC(x3,x2) -> fAC(x2,x3)
    TRS:
     fAC(x,one()) -> x
     fAC(i(x),x) -> one()
     g(one()) -> one()
     g(fAC(x,y)) -> fAC(g(x),g(y))
    S:
     f{AC,#}(fAC(x7,x8),x9) -> f{AC,#}(x7,x8)
     f{AC,#}(x7,fAC(x8,x9)) -> f{AC,#}(x8,x9)
    AC-DP unlabeling:
     Equations#:
      fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
      fAC(x2,x3) -> fAC(x3,x2)
      fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
      fAC(x3,x2) -> fAC(x2,x3)
     DPs:
      g#(fAC(x,y)) -> g#(y)
      g#(fAC(x,y)) -> g#(x)
     Equations:
      fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
      fAC(x2,x3) -> fAC(x3,x2)
      fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
      fAC(x3,x2) -> fAC(x2,x3)
     TRS:
      fAC(x,one()) -> x
      fAC(i(x),x) -> one()
      g(one()) -> one()
      g(fAC(x,y)) -> fAC(g(x),g(y))
     S:
      fAC(fAC(x7,x8),x9) -> fAC(x7,x8)
      fAC(x7,fAC(x8,x9)) -> fAC(x8,x9)
     Usable Rule Processor:
      Equations#:
       fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
       fAC(x2,x3) -> fAC(x3,x2)
       fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
       fAC(x3,x2) -> fAC(x2,x3)
      DPs:
       g#(fAC(x,y)) -> g#(y)
       g#(fAC(x,y)) -> g#(x)
      Equations:
       fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
       fAC(x2,x3) -> fAC(x3,x2)
       fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
       fAC(x3,x2) -> fAC(x2,x3)
      TRS:
       
      S:
       fAC(fAC(x7,x8),x9) -> fAC(x7,x8)
       fAC(x7,fAC(x8,x9)) -> fAC(x8,x9)
      AC-KBO Processor:
       argument filtering:
        pi(fAC) = [0,1]
        pi(g#) = 0
       precedence:
        g# > fAC
        weight function:
         [g#](x0) = x0,
         
         [fAC](x0, x1) = x0 + x1
         usable rules:
          
         problem:
          Equations#:
           fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
           fAC(x2,x3) -> fAC(x3,x2)
           fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
           fAC(x3,x2) -> fAC(x2,x3)
          DPs:
           
          Equations:
           fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
           fAC(x2,x3) -> fAC(x3,x2)
           fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
           fAC(x3,x2) -> fAC(x2,x3)
          TRS:
           
          S:
           fAC(fAC(x7,x8),x9) -> fAC(x7,x8)
           fAC(x7,fAC(x8,x9)) -> fAC(x8,x9)
         Qed
     
     Equations#:
      f{AC,#}(fAC(x2,x3),x4) -> f{AC,#}(x2,fAC(x3,x4))
      f{AC,#}(x2,x3) -> f{AC,#}(x3,x2)
      f{AC,#}(x2,fAC(x3,x4)) -> f{AC,#}(fAC(x2,x3),x4)
      f{AC,#}(x3,x2) -> f{AC,#}(x2,x3)
     DPs:
      f{AC,#}(x6,fAC(i(x),x)) -> f{AC,#}(x6,one())
      f{AC,#}(x5,fAC(x,one())) -> f{AC,#}(x5,x)
     Equations:
      fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
      fAC(x2,x3) -> fAC(x3,x2)
      fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
      fAC(x3,x2) -> fAC(x2,x3)
     TRS:
      fAC(x,one()) -> x
      fAC(i(x),x) -> one()
      g(one()) -> one()
      g(fAC(x,y)) -> fAC(g(x),g(y))
     S:
      f{AC,#}(fAC(x7,x8),x9) -> f{AC,#}(x7,x8)
      f{AC,#}(x7,fAC(x8,x9)) -> f{AC,#}(x8,x9)
     AC-DP unlabeling:
      Equations#:
       fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
       fAC(x2,x3) -> fAC(x3,x2)
       fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
       fAC(x3,x2) -> fAC(x2,x3)
      DPs:
       fAC(x6,fAC(i(x),x)) -> fAC(x6,one())
       fAC(x5,fAC(x,one())) -> fAC(x5,x)
      Equations:
       fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
       fAC(x2,x3) -> fAC(x3,x2)
       fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
       fAC(x3,x2) -> fAC(x2,x3)
      TRS:
       fAC(x,one()) -> x
       fAC(i(x),x) -> one()
       g(one()) -> one()
       g(fAC(x,y)) -> fAC(g(x),g(y))
      S:
       fAC(fAC(x7,x8),x9) -> fAC(x7,x8)
       fAC(x7,fAC(x8,x9)) -> fAC(x8,x9)
      Usable Rule Processor:
       Equations#:
        fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
        fAC(x2,x3) -> fAC(x3,x2)
        fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
        fAC(x3,x2) -> fAC(x2,x3)
       DPs:
        fAC(x6,fAC(i(x),x)) -> fAC(x6,one())
        fAC(x5,fAC(x,one())) -> fAC(x5,x)
       Equations:
        fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
        fAC(x2,x3) -> fAC(x3,x2)
        fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
        fAC(x3,x2) -> fAC(x2,x3)
       TRS:
        fAC(x,one()) -> x
        fAC(i(x),x) -> one()
       S:
        fAC(fAC(x7,x8),x9) -> fAC(x7,x8)
        fAC(x7,fAC(x8,x9)) -> fAC(x8,x9)
       AC-KBO Processor:
        argument filtering:
         pi(fAC) = [0,1]
         pi(one) = []
         pi(i) = 0
        precedence:
         i ~ fAC > one
         weight function:
          [i](x0) = x0,
          
          [one] = 3,
          
          [fAC](x0, x1) = x0 + x1 + 3
          usable rules:
           fAC(x,one()) -> x
           fAC(i(x),x) -> one()
          problem:
           Equations#:
            fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
            fAC(x2,x3) -> fAC(x3,x2)
            fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
            fAC(x3,x2) -> fAC(x2,x3)
           DPs:
            
           Equations:
            fAC(fAC(x2,x3),x4) -> fAC(x2,fAC(x3,x4))
            fAC(x2,x3) -> fAC(x3,x2)
            fAC(x2,fAC(x3,x4)) -> fAC(fAC(x2,x3),x4)
            fAC(x3,x2) -> fAC(x2,x3)
           TRS:
            fAC(x,one()) -> x
            fAC(i(x),x) -> one()
           S:
            fAC(fAC(x7,x8),x9) -> fAC(x7,x8)
            fAC(x7,fAC(x8,x9)) -> fAC(x8,x9)
          Qed