YES
Time: 0.044

Problem:
 Equations:
  pAC(pAC(x1,x2),x3) -> pAC(x1,pAC(x2,x3))
  pAC(x1,x2) -> pAC(x2,x1)
  pAC(x1,pAC(x2,x3)) -> pAC(pAC(x1,x2),x3)
  pAC(x2,x1) -> pAC(x1,x2)
 TRS:
  pAC(a(),x) -> pAC(b(),g(a()))

Proof:
 DP Processor:
  Equations#:
   p{AC,#}(pAC(x1,x2),x3) -> p{AC,#}(x1,pAC(x2,x3))
   p{AC,#}(x1,x2) -> p{AC,#}(x2,x1)
   p{AC,#}(x1,pAC(x2,x3)) -> p{AC,#}(pAC(x1,x2),x3)
   p{AC,#}(x2,x1) -> p{AC,#}(x1,x2)
  DPs:
   p{AC,#}(a(),x) -> p{AC,#}(b(),g(a()))
   p{AC,#}(x4,pAC(a(),x)) -> p{AC,#}(b(),g(a()))
   p{AC,#}(x4,pAC(a(),x)) -> p{AC,#}(x4,pAC(b(),g(a())))
  Equations:
   pAC(pAC(x1,x2),x3) -> pAC(x1,pAC(x2,x3))
   pAC(x1,x2) -> pAC(x2,x1)
   pAC(x1,pAC(x2,x3)) -> pAC(pAC(x1,x2),x3)
   pAC(x2,x1) -> pAC(x1,x2)
  TRS:
   pAC(a(),x) -> pAC(b(),g(a()))
  S:
   p{AC,#}(pAC(x5,x6),x7) -> p{AC,#}(x5,x6)
   p{AC,#}(x5,pAC(x6,x7)) -> p{AC,#}(x6,x7)
  AC-EDG Processor:
   Equations#:
    p{AC,#}(pAC(x1,x2),x3) -> p{AC,#}(x1,pAC(x2,x3))
    p{AC,#}(x1,x2) -> p{AC,#}(x2,x1)
    p{AC,#}(x1,pAC(x2,x3)) -> p{AC,#}(pAC(x1,x2),x3)
    p{AC,#}(x2,x1) -> p{AC,#}(x1,x2)
   DPs:
    p{AC,#}(a(),x) -> p{AC,#}(b(),g(a()))
    p{AC,#}(x4,pAC(a(),x)) -> p{AC,#}(b(),g(a()))
    p{AC,#}(x4,pAC(a(),x)) -> p{AC,#}(x4,pAC(b(),g(a())))
   Equations:
    pAC(pAC(x1,x2),x3) -> pAC(x1,pAC(x2,x3))
    pAC(x1,x2) -> pAC(x2,x1)
    pAC(x1,pAC(x2,x3)) -> pAC(pAC(x1,x2),x3)
    pAC(x2,x1) -> pAC(x1,x2)
   TRS:
    pAC(a(),x) -> pAC(b(),g(a()))
   S:
    p{AC,#}(pAC(x5,x6),x7) -> p{AC,#}(x5,x6)
    p{AC,#}(x5,pAC(x6,x7)) -> p{AC,#}(x6,x7)
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 3/9
    Equations#:
     p{AC,#}(pAC(x1,x2),x3) -> p{AC,#}(x1,pAC(x2,x3))
     p{AC,#}(x1,x2) -> p{AC,#}(x2,x1)
     p{AC,#}(x1,pAC(x2,x3)) -> p{AC,#}(pAC(x1,x2),x3)
     p{AC,#}(x2,x1) -> p{AC,#}(x1,x2)
    DPs:
     p{AC,#}(x4,pAC(a(),x)) -> p{AC,#}(x4,pAC(b(),g(a())))
    Equations:
     pAC(pAC(x1,x2),x3) -> pAC(x1,pAC(x2,x3))
     pAC(x1,x2) -> pAC(x2,x1)
     pAC(x1,pAC(x2,x3)) -> pAC(pAC(x1,x2),x3)
     pAC(x2,x1) -> pAC(x1,x2)
    TRS:
     pAC(a(),x) -> pAC(b(),g(a()))
    S:
     p{AC,#}(pAC(x5,x6),x7) -> p{AC,#}(x5,x6)
     p{AC,#}(x5,pAC(x6,x7)) -> p{AC,#}(x6,x7)
    AC-DP unlabeling:
     Equations#:
      pAC(pAC(x1,x2),x3) -> pAC(x1,pAC(x2,x3))
      pAC(x1,x2) -> pAC(x2,x1)
      pAC(x1,pAC(x2,x3)) -> pAC(pAC(x1,x2),x3)
      pAC(x2,x1) -> pAC(x1,x2)
     DPs:
      pAC(x4,pAC(a(),x)) -> pAC(x4,pAC(b(),g(a())))
     Equations:
      pAC(pAC(x1,x2),x3) -> pAC(x1,pAC(x2,x3))
      pAC(x1,x2) -> pAC(x2,x1)
      pAC(x1,pAC(x2,x3)) -> pAC(pAC(x1,x2),x3)
      pAC(x2,x1) -> pAC(x1,x2)
     TRS:
      pAC(a(),x) -> pAC(b(),g(a()))
     S:
      pAC(pAC(x5,x6),x7) -> pAC(x5,x6)
      pAC(x5,pAC(x6,x7)) -> pAC(x6,x7)
     AC-KBO Processor:
      argument filtering:
       pi(pAC) = [0,1]
       pi(a) = []
       pi(b) = []
       pi(g) = []
      precedence:
       pAC > g ~ b ~ a
       weight function:
        w0 = 2
        w(a) = 5
        w(g) = w(b) = 3
        w(pAC) = 2
        usable rules:
         pAC(a(),x) -> pAC(b(),g(a()))
        problem:
         Equations#:
          pAC(pAC(x1,x2),x3) -> pAC(x1,pAC(x2,x3))
          pAC(x1,x2) -> pAC(x2,x1)
          pAC(x1,pAC(x2,x3)) -> pAC(pAC(x1,x2),x3)
          pAC(x2,x1) -> pAC(x1,x2)
         DPs:
          
         Equations:
          pAC(pAC(x1,x2),x3) -> pAC(x1,pAC(x2,x3))
          pAC(x1,x2) -> pAC(x2,x1)
          pAC(x1,pAC(x2,x3)) -> pAC(pAC(x1,x2),x3)
          pAC(x2,x1) -> pAC(x1,x2)
         TRS:
          pAC(a(),x) -> pAC(b(),g(a()))
         S:
          pAC(pAC(x5,x6),x7) -> pAC(x5,x6)
          pAC(x5,pAC(x6,x7)) -> pAC(x6,x7)
        Qed