YES
Time: 0.167

Problem:
 Equations:
  fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
  fAC(x1,x2) -> fAC(x2,x1)
  fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
  fAC(x2,x1) -> fAC(x1,x2)
 TRS:
  fAC(g(g(x)),x) -> fAC(g(x),g(x))
  fAC(fAC(x,x),g(x)) -> fAC(x,h(x))

Proof:
 DP Processor:
  Equations#:
   f{AC,#}(fAC(x1,x2),x3) -> f{AC,#}(x1,fAC(x2,x3))
   f{AC,#}(x1,x2) -> f{AC,#}(x2,x1)
   f{AC,#}(x1,fAC(x2,x3)) -> f{AC,#}(fAC(x1,x2),x3)
   f{AC,#}(x2,x1) -> f{AC,#}(x1,x2)
  DPs:
   f{AC,#}(g(g(x)),x) -> f{AC,#}(g(x),g(x))
   f{AC,#}(fAC(x,x),g(x)) -> f{AC,#}(x,h(x))
   f{AC,#}(x4,fAC(g(g(x)),x)) -> f{AC,#}(g(x),g(x))
   f{AC,#}(x4,fAC(g(g(x)),x)) -> f{AC,#}(x4,fAC(g(x),g(x)))
   f{AC,#}(x5,fAC(fAC(x,x),g(x))) -> f{AC,#}(x,h(x))
   f{AC,#}(x5,fAC(fAC(x,x),g(x))) -> f{AC,#}(x5,fAC(x,h(x)))
  Equations:
   fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
   fAC(x1,x2) -> fAC(x2,x1)
   fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
   fAC(x2,x1) -> fAC(x1,x2)
  TRS:
   fAC(g(g(x)),x) -> fAC(g(x),g(x))
   fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
  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(x1,x2),x3) -> f{AC,#}(x1,fAC(x2,x3))
    f{AC,#}(x1,x2) -> f{AC,#}(x2,x1)
    f{AC,#}(x1,fAC(x2,x3)) -> f{AC,#}(fAC(x1,x2),x3)
    f{AC,#}(x2,x1) -> f{AC,#}(x1,x2)
   DPs:
    f{AC,#}(g(g(x)),x) -> f{AC,#}(g(x),g(x))
    f{AC,#}(fAC(x,x),g(x)) -> f{AC,#}(x,h(x))
    f{AC,#}(x4,fAC(g(g(x)),x)) -> f{AC,#}(g(x),g(x))
    f{AC,#}(x4,fAC(g(g(x)),x)) -> f{AC,#}(x4,fAC(g(x),g(x)))
    f{AC,#}(x5,fAC(fAC(x,x),g(x))) -> f{AC,#}(x,h(x))
    f{AC,#}(x5,fAC(fAC(x,x),g(x))) -> f{AC,#}(x5,fAC(x,h(x)))
   Equations:
    fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
    fAC(x1,x2) -> fAC(x2,x1)
    fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
    fAC(x2,x1) -> fAC(x1,x2)
   TRS:
    fAC(g(g(x)),x) -> fAC(g(x),g(x))
    fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
   S:
    f{AC,#}(fAC(x6,x7),x8) -> f{AC,#}(x6,x7)
    f{AC,#}(x6,fAC(x7,x8)) -> f{AC,#}(x7,x8)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 26/36
    Equations#:
     f{AC,#}(fAC(x1,x2),x3) -> f{AC,#}(x1,fAC(x2,x3))
     f{AC,#}(x1,x2) -> f{AC,#}(x2,x1)
     f{AC,#}(x1,fAC(x2,x3)) -> f{AC,#}(fAC(x1,x2),x3)
     f{AC,#}(x2,x1) -> f{AC,#}(x1,x2)
    DPs:
     f{AC,#}(fAC(x,x),g(x)) -> f{AC,#}(x,h(x))
     f{AC,#}(x5,fAC(fAC(x,x),g(x))) -> f{AC,#}(x5,fAC(x,h(x)))
     f{AC,#}(x5,fAC(fAC(x,x),g(x))) -> f{AC,#}(x,h(x))
     f{AC,#}(x4,fAC(g(g(x)),x)) -> f{AC,#}(x4,fAC(g(x),g(x)))
    Equations:
     fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
     fAC(x1,x2) -> fAC(x2,x1)
     fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
     fAC(x2,x1) -> fAC(x1,x2)
    TRS:
     fAC(g(g(x)),x) -> fAC(g(x),g(x))
     fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
    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(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
      fAC(x1,x2) -> fAC(x2,x1)
      fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
      fAC(x2,x1) -> fAC(x1,x2)
     DPs:
      fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
      fAC(x5,fAC(fAC(x,x),g(x))) -> fAC(x5,fAC(x,h(x)))
      fAC(x5,fAC(fAC(x,x),g(x))) -> fAC(x,h(x))
      fAC(x4,fAC(g(g(x)),x)) -> fAC(x4,fAC(g(x),g(x)))
     Equations:
      fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
      fAC(x1,x2) -> fAC(x2,x1)
      fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
      fAC(x2,x1) -> fAC(x1,x2)
     TRS:
      fAC(g(g(x)),x) -> fAC(g(x),g(x))
      fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
     S:
      fAC(fAC(x6,x7),x8) -> fAC(x6,x7)
      fAC(x6,fAC(x7,x8)) -> fAC(x7,x8)
     AC-KBO Processor:
      argument filtering:
       pi(fAC) = [0,1]
       pi(g) = [0]
       pi(h) = 0
      precedence:
       h ~ fAC > g
       weight function:
        w0 = 2
        w(h) = 5
        w(g) = 4
        w(fAC) = 3
        usable rules:
         fAC(g(g(x)),x) -> fAC(g(x),g(x))
         fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
        problem:
         Equations#:
          fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
          fAC(x1,x2) -> fAC(x2,x1)
          fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
          fAC(x2,x1) -> fAC(x1,x2)
         DPs:
          
         Equations:
          fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
          fAC(x1,x2) -> fAC(x2,x1)
          fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
          fAC(x2,x1) -> fAC(x1,x2)
         TRS:
          fAC(g(g(x)),x) -> fAC(g(x),g(x))
          fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
         S:
          fAC(fAC(x6,x7),x8) -> fAC(x6,x7)
          fAC(x6,fAC(x7,x8)) -> fAC(x7,x8)
        Qed
     
     Equations#:
      f{AC,#}(fAC(x1,x2),x3) -> f{AC,#}(x1,fAC(x2,x3))
      f{AC,#}(x1,x2) -> f{AC,#}(x2,x1)
      f{AC,#}(x1,fAC(x2,x3)) -> f{AC,#}(fAC(x1,x2),x3)
      f{AC,#}(x2,x1) -> f{AC,#}(x1,x2)
     DPs:
      f{AC,#}(g(g(x)),x) -> f{AC,#}(g(x),g(x))
     Equations:
      fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
      fAC(x1,x2) -> fAC(x2,x1)
      fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
      fAC(x2,x1) -> fAC(x1,x2)
     TRS:
      fAC(g(g(x)),x) -> fAC(g(x),g(x))
      fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
     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(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
       fAC(x1,x2) -> fAC(x2,x1)
       fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
       fAC(x2,x1) -> fAC(x1,x2)
      DPs:
       fAC(g(g(x)),x) -> fAC(g(x),g(x))
      Equations:
       fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
       fAC(x1,x2) -> fAC(x2,x1)
       fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
       fAC(x2,x1) -> fAC(x1,x2)
      TRS:
       fAC(g(g(x)),x) -> fAC(g(x),g(x))
       fAC(fAC(x,x),g(x)) -> fAC(x,h(x))
      S:
       fAC(fAC(x6,x7),x8) -> fAC(x6,x7)
       fAC(x6,fAC(x7,x8)) -> fAC(x7,x8)
      Usable Rule Processor:
       Equations#:
        fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
        fAC(x1,x2) -> fAC(x2,x1)
        fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
        fAC(x2,x1) -> fAC(x1,x2)
       DPs:
        fAC(g(g(x)),x) -> fAC(g(x),g(x))
       Equations:
        fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
        fAC(x1,x2) -> fAC(x2,x1)
        fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
        fAC(x2,x1) -> fAC(x1,x2)
       TRS:
        fAC(g(g(x)),x) -> fAC(g(x),g(x))
       S:
        fAC(fAC(x6,x7),x8) -> fAC(x6,x7)
        fAC(x6,fAC(x7,x8)) -> fAC(x7,x8)
       AC-KBO Processor:
        argument filtering:
         pi(fAC) = [0,1]
         pi(g) = [0]
        precedence:
         fAC > g
         weight function:
          w0 = 2
          w(g) = w(fAC) = 6
          usable rules:
           fAC(g(g(x)),x) -> fAC(g(x),g(x))
          problem:
           Equations#:
            fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
            fAC(x1,x2) -> fAC(x2,x1)
            fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
            fAC(x2,x1) -> fAC(x1,x2)
           DPs:
            
           Equations:
            fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3))
            fAC(x1,x2) -> fAC(x2,x1)
            fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3)
            fAC(x2,x1) -> fAC(x1,x2)
           TRS:
            fAC(g(g(x)),x) -> fAC(g(x),g(x))
           S:
            fAC(fAC(x6,x7),x8) -> fAC(x6,x7)
            fAC(x6,fAC(x7,x8)) -> fAC(x7,x8)
          Qed