YES
Time: 0.036

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(x,one()) -> x
  fAC(i(x),x) -> one()
  phi(one(),y1) -> y1
  phi(y1,phi(y2,x)) -> phi(fAC(y1,y2),x)

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:
   phi#(y1,phi(y2,x)) -> f{AC,#}(y1,y2)
   phi#(y1,phi(y2,x)) -> phi#(fAC(y1,y2),x)
   f{AC,#}(x6,fAC(x,one())) -> f{AC,#}(x6,x)
   f{AC,#}(x7,fAC(i(x),x)) -> f{AC,#}(x7,one())
  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(x,one()) -> x
   fAC(i(x),x) -> one()
   phi(one(),y1) -> y1
   phi(y1,phi(y2,x)) -> phi(fAC(y1,y2),x)
  S:
   f{AC,#}(fAC(x8,x9),x10) -> f{AC,#}(x8,x9)
   f{AC,#}(x8,fAC(x9,x10)) -> f{AC,#}(x9,x10)
  AC-EDG 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:
    phi#(y1,phi(y2,x)) -> f{AC,#}(y1,y2)
    phi#(y1,phi(y2,x)) -> phi#(fAC(y1,y2),x)
    f{AC,#}(x6,fAC(x,one())) -> f{AC,#}(x6,x)
    f{AC,#}(x7,fAC(i(x),x)) -> f{AC,#}(x7,one())
   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(x,one()) -> x
    fAC(i(x),x) -> one()
    phi(one(),y1) -> y1
    phi(y1,phi(y2,x)) -> phi(fAC(y1,y2),x)
   S:
    f{AC,#}(fAC(x8,x9),x10) -> f{AC,#}(x8,x9)
    f{AC,#}(x8,fAC(x9,x10)) -> f{AC,#}(x9,x10)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 8/16
    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:
     phi#(y1,phi(y2,x)) -> phi#(fAC(y1,y2),x)
    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(x,one()) -> x
     fAC(i(x),x) -> one()
     phi(one(),y1) -> y1
     phi(y1,phi(y2,x)) -> phi(fAC(y1,y2),x)
    S:
     f{AC,#}(fAC(x8,x9),x10) -> f{AC,#}(x8,x9)
     f{AC,#}(x8,fAC(x9,x10)) -> f{AC,#}(x9,x10)
    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:
      phi#(y1,phi(y2,x)) -> phi#(fAC(y1,y2),x)
     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(x,one()) -> x
      fAC(i(x),x) -> one()
      phi(one(),y1) -> y1
      phi(y1,phi(y2,x)) -> phi(fAC(y1,y2),x)
     S:
      fAC(fAC(x8,x9),x10) -> fAC(x8,x9)
      fAC(x8,fAC(x9,x10)) -> fAC(x9,x10)
     Usable Rule Processor:
      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:
       phi#(y1,phi(y2,x)) -> phi#(fAC(y1,y2),x)
      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(x,one()) -> x
       fAC(i(x),x) -> one()
      S:
       fAC(fAC(x8,x9),x10) -> fAC(x8,x9)
       fAC(x8,fAC(x9,x10)) -> fAC(x9,x10)
      AC-RPO Processor:
       argument filtering:
        pi(fAC) = [0,1]
        pi(one) = []
        pi(i) = 0
        pi(phi) = [1]
        pi(phi#) = [1]
       precedence:
        phi > phi# > one > i > fAC
       status:
        phi#:lex  phi:mul  
       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(x,one()) -> x
         fAC(i(x),x) -> one()
        S:
         fAC(fAC(x8,x9),x10) -> fAC(x8,x9)
         fAC(x8,fAC(x9,x10)) -> fAC(x9,x10)
       Qed
    
    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,#}(x7,fAC(i(x),x)) -> f{AC,#}(x7,one())
     f{AC,#}(x6,fAC(x,one())) -> f{AC,#}(x6,x)
    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(x,one()) -> x
     fAC(i(x),x) -> one()
     phi(one(),y1) -> y1
     phi(y1,phi(y2,x)) -> phi(fAC(y1,y2),x)
    S:
     f{AC,#}(fAC(x8,x9),x10) -> f{AC,#}(x8,x9)
     f{AC,#}(x8,fAC(x9,x10)) -> f{AC,#}(x9,x10)
    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(x7,fAC(i(x),x)) -> fAC(x7,one())
      fAC(x6,fAC(x,one())) -> fAC(x6,x)
     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(x,one()) -> x
      fAC(i(x),x) -> one()
      phi(one(),y1) -> y1
      phi(y1,phi(y2,x)) -> phi(fAC(y1,y2),x)
     S:
      fAC(fAC(x8,x9),x10) -> fAC(x8,x9)
      fAC(x8,fAC(x9,x10)) -> fAC(x9,x10)
     Usable Rule Processor:
      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(x7,fAC(i(x),x)) -> fAC(x7,one())
       fAC(x6,fAC(x,one())) -> fAC(x6,x)
      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(x,one()) -> x
       fAC(i(x),x) -> one()
      S:
       fAC(fAC(x8,x9),x10) -> fAC(x8,x9)
       fAC(x8,fAC(x9,x10)) -> fAC(x9,x10)
      AC-RPO Processor:
       argument filtering:
        pi(fAC) = [0,1]
        pi(one) = []
        pi(i) = []
       precedence:
        i > one > fAC
       status:
        
       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(x,one()) -> x
         fAC(i(x),x) -> one()
        S:
         fAC(fAC(x8,x9),x10) -> fAC(x8,x9)
         fAC(x8,fAC(x9,x10)) -> fAC(x9,x10)
       Qed