YES
Time: 0.027

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(x,one()) -> 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,#}(x4,fAC(x,one())) -> f{AC,#}(x4,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(x,one()) -> x
  S:
   f{AC,#}(fAC(x5,x6),x7) -> f{AC,#}(x5,x6)
   f{AC,#}(x5,fAC(x6,x7)) -> f{AC,#}(x6,x7)
  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(x4,fAC(x,one())) -> fAC(x4,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(x,one()) -> x
   S:
    fAC(fAC(x5,x6),x7) -> fAC(x5,x6)
    fAC(x5,fAC(x6,x7)) -> fAC(x6,x7)
   AC-KBO Processor:
    argument filtering:
     pi(fAC) = [0,1]
     pi(one) = []
    precedence:
     one ~ fAC
     weight function:
      w0 = 1
      w(one) = 1
      w(fAC) = 0
      usable rules:
       fAC(x,one()) -> 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(x,one()) -> x
       S:
        fAC(fAC(x5,x6),x7) -> fAC(x5,x6)
        fAC(x5,fAC(x6,x7)) -> fAC(x6,x7)
      Qed