YES
Time: 0.390

Problem:
 Equations:
  pAC(pAC(x2,x3),x4) -> pAC(x2,pAC(x3,x4))
  pAC(x2,x3) -> pAC(x3,x2)
  pAC(x2,pAC(x3,x4)) -> pAC(pAC(x2,x3),x4)
  pAC(x3,x2) -> pAC(x2,x3)
 TRS:
  pAC(x,one()) -> x
  pAC(x,x) -> x
  pAC(T(x),x) -> T(x)
  T(pAC(x,T(y))) -> pAC(T(pAC(x,y)),T(y))
  L(pAC(x,T(y))) -> pAC(L(pAC(x,y)),L(y))

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