YES
Time: 0.704

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

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,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(x,y1)
   f{AC,#}(fAC(i(x),i(y1)),y2) -> i#(fAC(x,y1))
   f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(i(fAC(x,y1)),y2)
   phi#(x,phi(y1,y2)) -> f{AC,#}(x,y1)
   phi#(x,phi(y1,y2)) -> phi#(fAC(x,y1),y2)
   f{AC,#}(i(fAC(x,y1)),y1) -> i#(x)
   i#(fAC(i(y1),x)) -> i#(x)
   i#(fAC(i(y1),x)) -> f{AC,#}(i(x),y1)
   f{AC,#}(i(x),i(y1)) -> f{AC,#}(x,y1)
   f{AC,#}(i(x),i(y1)) -> i#(fAC(x,y1))
   f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x,y1)
   f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> i#(fAC(x,y1))
   f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(i(fAC(x,y1)),y2)
   f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x6,fAC(i(fAC(x,y1)),y2))
   f{AC,#}(x7,fAC(one(),x)) -> f{AC,#}(x7,x)
   f{AC,#}(x8,fAC(i(x),x)) -> f{AC,#}(x8,one())
   f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> i#(x)
   f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> f{AC,#}(x9,i(x))
   f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x,y1)
   f{AC,#}(x10,fAC(i(x),i(y1))) -> i#(fAC(x,y1))
   f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x10,i(fAC(x,y1)))
  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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
   fAC(one(),x) -> x
   phi(one(),x) -> x
   fAC(i(x),x) -> one()
   i(one()) -> one()
   i(i(x)) -> x
   phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
   fAC(i(fAC(x,y1)),y1) -> i(x)
   i(fAC(i(y1),x)) -> fAC(i(x),y1)
   fAC(i(x),i(y1)) -> i(fAC(x,y1))
  S:
   f{AC,#}(fAC(x11,x12),x13) -> f{AC,#}(x11,x12)
   f{AC,#}(x11,fAC(x12,x13)) -> f{AC,#}(x12,x13)
  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:
    f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(x,y1)
    f{AC,#}(fAC(i(x),i(y1)),y2) -> i#(fAC(x,y1))
    f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(i(fAC(x,y1)),y2)
    phi#(x,phi(y1,y2)) -> f{AC,#}(x,y1)
    phi#(x,phi(y1,y2)) -> phi#(fAC(x,y1),y2)
    f{AC,#}(i(fAC(x,y1)),y1) -> i#(x)
    i#(fAC(i(y1),x)) -> i#(x)
    i#(fAC(i(y1),x)) -> f{AC,#}(i(x),y1)
    f{AC,#}(i(x),i(y1)) -> f{AC,#}(x,y1)
    f{AC,#}(i(x),i(y1)) -> i#(fAC(x,y1))
    f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x,y1)
    f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> i#(fAC(x,y1))
    f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(i(fAC(x,y1)),y2)
    f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x6,fAC(i(fAC(x,y1)),y2))
    f{AC,#}(x7,fAC(one(),x)) -> f{AC,#}(x7,x)
    f{AC,#}(x8,fAC(i(x),x)) -> f{AC,#}(x8,one())
    f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> i#(x)
    f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> f{AC,#}(x9,i(x))
    f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x,y1)
    f{AC,#}(x10,fAC(i(x),i(y1))) -> i#(fAC(x,y1))
    f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x10,i(fAC(x,y1)))
   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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
    fAC(one(),x) -> x
    phi(one(),x) -> x
    fAC(i(x),x) -> one()
    i(one()) -> one()
    i(i(x)) -> x
    phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
    fAC(i(fAC(x,y1)),y1) -> i(x)
    i(fAC(i(y1),x)) -> fAC(i(x),y1)
    fAC(i(x),i(y1)) -> i(fAC(x,y1))
   S:
    f{AC,#}(fAC(x11,x12),x13) -> f{AC,#}(x11,x12)
    f{AC,#}(x11,fAC(x12,x13)) -> f{AC,#}(x12,x13)
   SCC Processor:
    #sccs: 2
    #rules: 20
    #arcs: 237/441
    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#(x,phi(y1,y2)) -> phi#(fAC(x,y1),y2)
    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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
     fAC(one(),x) -> x
     phi(one(),x) -> x
     fAC(i(x),x) -> one()
     i(one()) -> one()
     i(i(x)) -> x
     phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
     fAC(i(fAC(x,y1)),y1) -> i(x)
     i(fAC(i(y1),x)) -> fAC(i(x),y1)
     fAC(i(x),i(y1)) -> i(fAC(x,y1))
    S:
     f{AC,#}(fAC(x11,x12),x13) -> f{AC,#}(x11,x12)
     f{AC,#}(x11,fAC(x12,x13)) -> f{AC,#}(x12,x13)
    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#(x,phi(y1,y2)) -> phi#(fAC(x,y1),y2)
     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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
      fAC(one(),x) -> x
      phi(one(),x) -> x
      fAC(i(x),x) -> one()
      i(one()) -> one()
      i(i(x)) -> x
      phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
      fAC(i(fAC(x,y1)),y1) -> i(x)
      i(fAC(i(y1),x)) -> fAC(i(x),y1)
      fAC(i(x),i(y1)) -> i(fAC(x,y1))
     S:
      fAC(fAC(x11,x12),x13) -> fAC(x11,x12)
      fAC(x11,fAC(x12,x13)) -> fAC(x12,x13)
     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#(x,phi(y1,y2)) -> phi#(fAC(x,y1),y2)
      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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
       fAC(one(),x) -> x
       fAC(i(x),x) -> one()
       fAC(i(fAC(x,y1)),y1) -> i(x)
       fAC(i(x),i(y1)) -> i(fAC(x,y1))
       i(one()) -> one()
       i(i(x)) -> x
       i(fAC(i(y1),x)) -> fAC(i(x),y1)
      S:
       fAC(fAC(x11,x12),x13) -> fAC(x11,x12)
       fAC(x11,fAC(x12,x13)) -> fAC(x12,x13)
      AC-KBO Processor:
       argument filtering:
        pi(fAC) = [0,1]
        pi(i) = []
        pi(one) = []
        pi(phi) = [1]
        pi(phi#) = [1]
       precedence:
        phi# ~ phi ~ one ~ fAC > i
        weight function:
         w0 = 2
         w(i) = 7
         w(one) = 4
         w(fAC) = 3
         w(phi#) = 2
         w(phi) = 0
         usable rules:
          
         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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
           fAC(one(),x) -> x
           fAC(i(x),x) -> one()
           fAC(i(fAC(x,y1)),y1) -> i(x)
           fAC(i(x),i(y1)) -> i(fAC(x,y1))
           i(one()) -> one()
           i(i(x)) -> x
           i(fAC(i(y1),x)) -> fAC(i(x),y1)
          S:
           fAC(fAC(x11,x12),x13) -> fAC(x11,x12)
           fAC(x11,fAC(x12,x13)) -> fAC(x12,x13)
         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,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x10,i(fAC(x,y1)))
      f{AC,#}(x10,fAC(i(x),i(y1))) -> i#(fAC(x,y1))
      i#(fAC(i(y1),x)) -> f{AC,#}(i(x),y1)
      f{AC,#}(x10,fAC(i(x),i(y1))) -> f{AC,#}(x,y1)
      f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> f{AC,#}(x9,i(x))
      f{AC,#}(x9,fAC(i(fAC(x,y1)),y1)) -> i#(x)
      i#(fAC(i(y1),x)) -> i#(x)
      f{AC,#}(x8,fAC(i(x),x)) -> f{AC,#}(x8,one())
      f{AC,#}(x7,fAC(one(),x)) -> f{AC,#}(x7,x)
      f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x6,fAC(i(fAC(x,y1)),y2))
      f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(i(fAC(x,y1)),y2)
      f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> i#(fAC(x,y1))
      f{AC,#}(x6,fAC(fAC(i(x),i(y1)),y2)) -> f{AC,#}(x,y1)
      f{AC,#}(i(x),i(y1)) -> i#(fAC(x,y1))
      f{AC,#}(i(x),i(y1)) -> f{AC,#}(x,y1)
      f{AC,#}(i(fAC(x,y1)),y1) -> i#(x)
      f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(i(fAC(x,y1)),y2)
      f{AC,#}(fAC(i(x),i(y1)),y2) -> i#(fAC(x,y1))
      f{AC,#}(fAC(i(x),i(y1)),y2) -> f{AC,#}(x,y1)
     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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
      fAC(one(),x) -> x
      phi(one(),x) -> x
      fAC(i(x),x) -> one()
      i(one()) -> one()
      i(i(x)) -> x
      phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
      fAC(i(fAC(x,y1)),y1) -> i(x)
      i(fAC(i(y1),x)) -> fAC(i(x),y1)
      fAC(i(x),i(y1)) -> i(fAC(x,y1))
     S:
      f{AC,#}(fAC(x11,x12),x13) -> f{AC,#}(x11,x12)
      f{AC,#}(x11,fAC(x12,x13)) -> f{AC,#}(x12,x13)
     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(x10,fAC(i(x),i(y1))) -> fAC(x10,i(fAC(x,y1)))
       fAC(x10,fAC(i(x),i(y1))) -> i#(fAC(x,y1))
       i#(fAC(i(y1),x)) -> fAC(i(x),y1)
       fAC(x10,fAC(i(x),i(y1))) -> fAC(x,y1)
       fAC(x9,fAC(i(fAC(x,y1)),y1)) -> fAC(x9,i(x))
       fAC(x9,fAC(i(fAC(x,y1)),y1)) -> i#(x)
       i#(fAC(i(y1),x)) -> i#(x)
       fAC(x8,fAC(i(x),x)) -> fAC(x8,one())
       fAC(x7,fAC(one(),x)) -> fAC(x7,x)
       fAC(x6,fAC(fAC(i(x),i(y1)),y2)) -> fAC(x6,fAC(i(fAC(x,y1)),y2))
       fAC(x6,fAC(fAC(i(x),i(y1)),y2)) -> fAC(i(fAC(x,y1)),y2)
       fAC(x6,fAC(fAC(i(x),i(y1)),y2)) -> i#(fAC(x,y1))
       fAC(x6,fAC(fAC(i(x),i(y1)),y2)) -> fAC(x,y1)
       fAC(i(x),i(y1)) -> i#(fAC(x,y1))
       fAC(i(x),i(y1)) -> fAC(x,y1)
       fAC(i(fAC(x,y1)),y1) -> i#(x)
       fAC(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
       fAC(fAC(i(x),i(y1)),y2) -> i#(fAC(x,y1))
       fAC(fAC(i(x),i(y1)),y2) -> fAC(x,y1)
      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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
       fAC(one(),x) -> x
       phi(one(),x) -> x
       fAC(i(x),x) -> one()
       i(one()) -> one()
       i(i(x)) -> x
       phi(x,phi(y1,y2)) -> phi(fAC(x,y1),y2)
       fAC(i(fAC(x,y1)),y1) -> i(x)
       i(fAC(i(y1),x)) -> fAC(i(x),y1)
       fAC(i(x),i(y1)) -> i(fAC(x,y1))
      S:
       fAC(fAC(x11,x12),x13) -> fAC(x11,x12)
       fAC(x11,fAC(x12,x13)) -> fAC(x12,x13)
      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(x10,fAC(i(x),i(y1))) -> fAC(x10,i(fAC(x,y1)))
        fAC(x10,fAC(i(x),i(y1))) -> i#(fAC(x,y1))
        i#(fAC(i(y1),x)) -> fAC(i(x),y1)
        fAC(x10,fAC(i(x),i(y1))) -> fAC(x,y1)
        fAC(x9,fAC(i(fAC(x,y1)),y1)) -> fAC(x9,i(x))
        fAC(x9,fAC(i(fAC(x,y1)),y1)) -> i#(x)
        i#(fAC(i(y1),x)) -> i#(x)
        fAC(x8,fAC(i(x),x)) -> fAC(x8,one())
        fAC(x7,fAC(one(),x)) -> fAC(x7,x)
        fAC(x6,fAC(fAC(i(x),i(y1)),y2)) -> fAC(x6,fAC(i(fAC(x,y1)),y2))
        fAC(x6,fAC(fAC(i(x),i(y1)),y2)) -> fAC(i(fAC(x,y1)),y2)
        fAC(x6,fAC(fAC(i(x),i(y1)),y2)) -> i#(fAC(x,y1))
        fAC(x6,fAC(fAC(i(x),i(y1)),y2)) -> fAC(x,y1)
        fAC(i(x),i(y1)) -> i#(fAC(x,y1))
        fAC(i(x),i(y1)) -> fAC(x,y1)
        fAC(i(fAC(x,y1)),y1) -> i#(x)
        fAC(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
        fAC(fAC(i(x),i(y1)),y2) -> i#(fAC(x,y1))
        fAC(fAC(i(x),i(y1)),y2) -> fAC(x,y1)
       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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
        fAC(one(),x) -> x
        fAC(i(x),x) -> one()
        fAC(i(fAC(x,y1)),y1) -> i(x)
        fAC(i(x),i(y1)) -> i(fAC(x,y1))
        i(one()) -> one()
        i(i(x)) -> x
        i(fAC(i(y1),x)) -> fAC(i(x),y1)
       S:
        fAC(fAC(x11,x12),x13) -> fAC(x11,x12)
        fAC(x11,fAC(x12,x13)) -> fAC(x12,x13)
       AC-KBO Processor:
        argument filtering:
         pi(fAC) = [0,1]
         pi(i) = [0]
         pi(one) = []
         pi(i#) = [0]
        precedence:
         i# ~ one > i ~ fAC
         weight function:
          w0 = 1
          w(one) = 2
          w(i) = w(fAC) = 1
          w(i#) = 0
          usable rules:
           fAC(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
           fAC(one(),x) -> x
           fAC(i(x),x) -> one()
           fAC(i(fAC(x,y1)),y1) -> i(x)
           fAC(i(x),i(y1)) -> i(fAC(x,y1))
           i(one()) -> one()
           i(i(x)) -> x
           i(fAC(i(y1),x)) -> fAC(i(x),y1)
          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(fAC(i(x),i(y1)),y2) -> fAC(i(fAC(x,y1)),y2)
            fAC(one(),x) -> x
            fAC(i(x),x) -> one()
            fAC(i(fAC(x,y1)),y1) -> i(x)
            fAC(i(x),i(y1)) -> i(fAC(x,y1))
            i(one()) -> one()
            i(i(x)) -> x
            i(fAC(i(y1),x)) -> fAC(i(x),y1)
           S:
            fAC(fAC(x11,x12),x13) -> fAC(x11,x12)
            fAC(x11,fAC(x12,x13)) -> fAC(x12,x13)
          Qed