YES
Time: 0.039

Problem:
 Equations:
  fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
  fAC(x3,x4) -> fAC(x4,x3)
  fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
  fAC(x4,x3) -> fAC(x3,x4)
 TRS:
  fAC(i(x),fAC(x,y)) -> y

Proof:
 DP Processor:
  Equations#:
   f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5))
   f{AC,#}(x3,x4) -> f{AC,#}(x4,x3)
   f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5)
   f{AC,#}(x4,x3) -> f{AC,#}(x3,x4)
  DPs:
   f{AC,#}(x6,fAC(i(x),fAC(x,y))) -> f{AC,#}(x6,y)
  Equations:
   fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
   fAC(x3,x4) -> fAC(x4,x3)
   fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
   fAC(x4,x3) -> fAC(x3,x4)
  TRS:
   fAC(i(x),fAC(x,y)) -> 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(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
    fAC(x3,x4) -> fAC(x4,x3)
    fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
    fAC(x4,x3) -> fAC(x3,x4)
   DPs:
    fAC(x6,fAC(i(x),fAC(x,y))) -> fAC(x6,y)
   Equations:
    fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
    fAC(x3,x4) -> fAC(x4,x3)
    fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
    fAC(x4,x3) -> fAC(x3,x4)
   TRS:
    fAC(i(x),fAC(x,y)) -> y
   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(i) = [0]
    precedence:
     i ~ fAC
     weight function:
      w0 = 2
      w(i) = 7
      w(fAC) = 3
      usable rules:
       fAC(i(x),fAC(x,y)) -> y
      problem:
       Equations#:
        fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
        fAC(x3,x4) -> fAC(x4,x3)
        fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
        fAC(x4,x3) -> fAC(x3,x4)
       DPs:
        
       Equations:
        fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
        fAC(x3,x4) -> fAC(x4,x3)
        fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
        fAC(x4,x3) -> fAC(x3,x4)
       TRS:
        fAC(i(x),fAC(x,y)) -> y
       S:
        fAC(fAC(x7,x8),x9) -> fAC(x7,x8)
        fAC(x7,fAC(x8,x9)) -> fAC(x8,x9)
      Qed