YES
Time: 0.508

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,g(y,z)) -> g(fAC(x,y),fAC(x,z))
  fAC(x,u1(y)) -> u1(fAC(x,y))
  fAC(x,u2(y)) -> u2(fAC(x,y))
  fAC(x,u3(y)) -> u3(fAC(x,y))
  u1(g(x,y)) -> g(u1(x),u1(y))
  u2(g(x,y)) -> g(u2(x),u2(y))
  u3(g(x,y)) -> g(u3(x),u3(y))
  u2(u1(x)) -> u1(u2(x))
  u3(u1(x)) -> u1(u3(x))
  u3(u2(x)) -> u2(u3(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:
   f{AC,#}(x,g(y,z)) -> f{AC,#}(x,z)
   f{AC,#}(x,g(y,z)) -> f{AC,#}(x,y)
   f{AC,#}(x,u1(y)) -> f{AC,#}(x,y)
   f{AC,#}(x,u1(y)) -> u1#(fAC(x,y))
   f{AC,#}(x,u2(y)) -> f{AC,#}(x,y)
   f{AC,#}(x,u2(y)) -> u2#(fAC(x,y))
   f{AC,#}(x,u3(y)) -> f{AC,#}(x,y)
   f{AC,#}(x,u3(y)) -> u3#(fAC(x,y))
   u1#(g(x,y)) -> u1#(y)
   u1#(g(x,y)) -> u1#(x)
   u2#(g(x,y)) -> u2#(y)
   u2#(g(x,y)) -> u2#(x)
   u3#(g(x,y)) -> u3#(y)
   u3#(g(x,y)) -> u3#(x)
   u2#(u1(x)) -> u2#(x)
   u2#(u1(x)) -> u1#(u2(x))
   u3#(u1(x)) -> u3#(x)
   u3#(u1(x)) -> u1#(u3(x))
   u3#(u2(x)) -> u3#(x)
   u3#(u2(x)) -> u2#(u3(x))
   f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,z)
   f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,y)
   f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x6,g(fAC(x,y),fAC(x,z)))
   f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x,y)
   f{AC,#}(x7,fAC(x,u1(y))) -> u1#(fAC(x,y))
   f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x7,u1(fAC(x,y)))
   f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x,y)
   f{AC,#}(x8,fAC(x,u2(y))) -> u2#(fAC(x,y))
   f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x8,u2(fAC(x,y)))
   f{AC,#}(x9,fAC(x,u3(y))) -> f{AC,#}(x,y)
   f{AC,#}(x9,fAC(x,u3(y))) -> u3#(fAC(x,y))
   f{AC,#}(x9,fAC(x,u3(y))) -> f{AC,#}(x9,u3(fAC(x,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(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
   fAC(x,u1(y)) -> u1(fAC(x,y))
   fAC(x,u2(y)) -> u2(fAC(x,y))
   fAC(x,u3(y)) -> u3(fAC(x,y))
   u1(g(x,y)) -> g(u1(x),u1(y))
   u2(g(x,y)) -> g(u2(x),u2(y))
   u3(g(x,y)) -> g(u3(x),u3(y))
   u2(u1(x)) -> u1(u2(x))
   u3(u1(x)) -> u1(u3(x))
   u3(u2(x)) -> u2(u3(x))
  S:
   f{AC,#}(fAC(x10,x11),x12) -> f{AC,#}(x10,x11)
   f{AC,#}(x10,fAC(x11,x12)) -> f{AC,#}(x11,x12)
  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,#}(x,g(y,z)) -> f{AC,#}(x,z)
    f{AC,#}(x,g(y,z)) -> f{AC,#}(x,y)
    f{AC,#}(x,u1(y)) -> f{AC,#}(x,y)
    f{AC,#}(x,u1(y)) -> u1#(fAC(x,y))
    f{AC,#}(x,u2(y)) -> f{AC,#}(x,y)
    f{AC,#}(x,u2(y)) -> u2#(fAC(x,y))
    f{AC,#}(x,u3(y)) -> f{AC,#}(x,y)
    f{AC,#}(x,u3(y)) -> u3#(fAC(x,y))
    u1#(g(x,y)) -> u1#(y)
    u1#(g(x,y)) -> u1#(x)
    u2#(g(x,y)) -> u2#(y)
    u2#(g(x,y)) -> u2#(x)
    u3#(g(x,y)) -> u3#(y)
    u3#(g(x,y)) -> u3#(x)
    u2#(u1(x)) -> u2#(x)
    u2#(u1(x)) -> u1#(u2(x))
    u3#(u1(x)) -> u3#(x)
    u3#(u1(x)) -> u1#(u3(x))
    u3#(u2(x)) -> u3#(x)
    u3#(u2(x)) -> u2#(u3(x))
    f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,z)
    f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,y)
    f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x6,g(fAC(x,y),fAC(x,z)))
    f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x,y)
    f{AC,#}(x7,fAC(x,u1(y))) -> u1#(fAC(x,y))
    f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x7,u1(fAC(x,y)))
    f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x,y)
    f{AC,#}(x8,fAC(x,u2(y))) -> u2#(fAC(x,y))
    f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x8,u2(fAC(x,y)))
    f{AC,#}(x9,fAC(x,u3(y))) -> f{AC,#}(x,y)
    f{AC,#}(x9,fAC(x,u3(y))) -> u3#(fAC(x,y))
    f{AC,#}(x9,fAC(x,u3(y))) -> f{AC,#}(x9,u3(fAC(x,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(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
    fAC(x,u1(y)) -> u1(fAC(x,y))
    fAC(x,u2(y)) -> u2(fAC(x,y))
    fAC(x,u3(y)) -> u3(fAC(x,y))
    u1(g(x,y)) -> g(u1(x),u1(y))
    u2(g(x,y)) -> g(u2(x),u2(y))
    u3(g(x,y)) -> g(u3(x),u3(y))
    u2(u1(x)) -> u1(u2(x))
    u3(u1(x)) -> u1(u3(x))
    u3(u2(x)) -> u2(u3(x))
   S:
    f{AC,#}(fAC(x10,x11),x12) -> f{AC,#}(x10,x11)
    f{AC,#}(x10,fAC(x11,x12)) -> f{AC,#}(x11,x12)
   SCC Processor:
    #sccs: 4
    #rules: 23
    #arcs: 352/1024
    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,#}(x9,fAC(x,u3(y))) -> f{AC,#}(x9,u3(fAC(x,y)))
     f{AC,#}(x9,fAC(x,u3(y))) -> f{AC,#}(x,y)
     f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x8,u2(fAC(x,y)))
     f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x,y)
     f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x7,u1(fAC(x,y)))
     f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x,y)
     f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x6,g(fAC(x,y),fAC(x,z)))
     f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,y)
     f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,z)
     f{AC,#}(x,u3(y)) -> f{AC,#}(x,y)
     f{AC,#}(x,u2(y)) -> f{AC,#}(x,y)
     f{AC,#}(x,u1(y)) -> f{AC,#}(x,y)
     f{AC,#}(x,g(y,z)) -> f{AC,#}(x,y)
     f{AC,#}(x,g(y,z)) -> f{AC,#}(x,z)
    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,g(y,z)) -> g(fAC(x,y),fAC(x,z))
     fAC(x,u1(y)) -> u1(fAC(x,y))
     fAC(x,u2(y)) -> u2(fAC(x,y))
     fAC(x,u3(y)) -> u3(fAC(x,y))
     u1(g(x,y)) -> g(u1(x),u1(y))
     u2(g(x,y)) -> g(u2(x),u2(y))
     u3(g(x,y)) -> g(u3(x),u3(y))
     u2(u1(x)) -> u1(u2(x))
     u3(u1(x)) -> u1(u3(x))
     u3(u2(x)) -> u2(u3(x))
    S:
     f{AC,#}(fAC(x10,x11),x12) -> f{AC,#}(x10,x11)
     f{AC,#}(x10,fAC(x11,x12)) -> f{AC,#}(x11,x12)
    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(x9,fAC(x,u3(y))) -> fAC(x9,u3(fAC(x,y)))
      fAC(x9,fAC(x,u3(y))) -> fAC(x,y)
      fAC(x8,fAC(x,u2(y))) -> fAC(x8,u2(fAC(x,y)))
      fAC(x8,fAC(x,u2(y))) -> fAC(x,y)
      fAC(x7,fAC(x,u1(y))) -> fAC(x7,u1(fAC(x,y)))
      fAC(x7,fAC(x,u1(y))) -> fAC(x,y)
      fAC(x6,fAC(x,g(y,z))) -> fAC(x6,g(fAC(x,y),fAC(x,z)))
      fAC(x6,fAC(x,g(y,z))) -> fAC(x,y)
      fAC(x6,fAC(x,g(y,z))) -> fAC(x,z)
      fAC(x,u3(y)) -> fAC(x,y)
      fAC(x,u2(y)) -> fAC(x,y)
      fAC(x,u1(y)) -> fAC(x,y)
      fAC(x,g(y,z)) -> fAC(x,y)
      fAC(x,g(y,z)) -> fAC(x,z)
     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,g(y,z)) -> g(fAC(x,y),fAC(x,z))
      fAC(x,u1(y)) -> u1(fAC(x,y))
      fAC(x,u2(y)) -> u2(fAC(x,y))
      fAC(x,u3(y)) -> u3(fAC(x,y))
      u1(g(x,y)) -> g(u1(x),u1(y))
      u2(g(x,y)) -> g(u2(x),u2(y))
      u3(g(x,y)) -> g(u3(x),u3(y))
      u2(u1(x)) -> u1(u2(x))
      u3(u1(x)) -> u1(u3(x))
      u3(u2(x)) -> u2(u3(x))
     S:
      fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
      fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
     AC-RPO Processor:
      argument filtering:
       pi(fAC) = [0,1]
       pi(g) = []
       pi(u1) = []
       pi(u2) = []
       pi(u3) = []
      precedence:
       fAC > u3 > u2 > u1 > g
      status:
       g: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,g(y,z)) -> g(fAC(x,y),fAC(x,z))
        fAC(x,u1(y)) -> u1(fAC(x,y))
        fAC(x,u2(y)) -> u2(fAC(x,y))
        fAC(x,u3(y)) -> u3(fAC(x,y))
        u1(g(x,y)) -> g(u1(x),u1(y))
        u2(g(x,y)) -> g(u2(x),u2(y))
        u3(g(x,y)) -> g(u3(x),u3(y))
        u2(u1(x)) -> u1(u2(x))
        u3(u1(x)) -> u1(u3(x))
        u3(u2(x)) -> u2(u3(x))
       S:
        fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
        fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
      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:
     u3#(u2(x)) -> u3#(x)
     u3#(u1(x)) -> u3#(x)
     u3#(g(x,y)) -> u3#(x)
     u3#(g(x,y)) -> u3#(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(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
     fAC(x,u1(y)) -> u1(fAC(x,y))
     fAC(x,u2(y)) -> u2(fAC(x,y))
     fAC(x,u3(y)) -> u3(fAC(x,y))
     u1(g(x,y)) -> g(u1(x),u1(y))
     u2(g(x,y)) -> g(u2(x),u2(y))
     u3(g(x,y)) -> g(u3(x),u3(y))
     u2(u1(x)) -> u1(u2(x))
     u3(u1(x)) -> u1(u3(x))
     u3(u2(x)) -> u2(u3(x))
    S:
     f{AC,#}(fAC(x10,x11),x12) -> f{AC,#}(x10,x11)
     f{AC,#}(x10,fAC(x11,x12)) -> f{AC,#}(x11,x12)
    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:
      u3#(u2(x)) -> u3#(x)
      u3#(u1(x)) -> u3#(x)
      u3#(g(x,y)) -> u3#(x)
      u3#(g(x,y)) -> u3#(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(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
      fAC(x,u1(y)) -> u1(fAC(x,y))
      fAC(x,u2(y)) -> u2(fAC(x,y))
      fAC(x,u3(y)) -> u3(fAC(x,y))
      u1(g(x,y)) -> g(u1(x),u1(y))
      u2(g(x,y)) -> g(u2(x),u2(y))
      u3(g(x,y)) -> g(u3(x),u3(y))
      u2(u1(x)) -> u1(u2(x))
      u3(u1(x)) -> u1(u3(x))
      u3(u2(x)) -> u2(u3(x))
     S:
      fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
      fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
     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:
       u3#(u2(x)) -> u3#(x)
       u3#(u1(x)) -> u3#(x)
       u3#(g(x,y)) -> u3#(x)
       u3#(g(x,y)) -> u3#(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:
       
      S:
       fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
       fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
      AC-RPO Processor:
       argument filtering:
        pi(fAC) = []
        pi(g) = [0,1]
        pi(u1) = [0]
        pi(u2) = [0]
        pi(u3#) = [0]
       precedence:
        u2 > g > u1 > u3# > fAC
       status:
        g: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:
         
        S:
         fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
         fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
       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:
     u2#(u1(x)) -> u2#(x)
     u2#(g(x,y)) -> u2#(x)
     u2#(g(x,y)) -> u2#(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(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
     fAC(x,u1(y)) -> u1(fAC(x,y))
     fAC(x,u2(y)) -> u2(fAC(x,y))
     fAC(x,u3(y)) -> u3(fAC(x,y))
     u1(g(x,y)) -> g(u1(x),u1(y))
     u2(g(x,y)) -> g(u2(x),u2(y))
     u3(g(x,y)) -> g(u3(x),u3(y))
     u2(u1(x)) -> u1(u2(x))
     u3(u1(x)) -> u1(u3(x))
     u3(u2(x)) -> u2(u3(x))
    S:
     f{AC,#}(fAC(x10,x11),x12) -> f{AC,#}(x10,x11)
     f{AC,#}(x10,fAC(x11,x12)) -> f{AC,#}(x11,x12)
    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:
      u2#(u1(x)) -> u2#(x)
      u2#(g(x,y)) -> u2#(x)
      u2#(g(x,y)) -> u2#(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(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
      fAC(x,u1(y)) -> u1(fAC(x,y))
      fAC(x,u2(y)) -> u2(fAC(x,y))
      fAC(x,u3(y)) -> u3(fAC(x,y))
      u1(g(x,y)) -> g(u1(x),u1(y))
      u2(g(x,y)) -> g(u2(x),u2(y))
      u3(g(x,y)) -> g(u3(x),u3(y))
      u2(u1(x)) -> u1(u2(x))
      u3(u1(x)) -> u1(u3(x))
      u3(u2(x)) -> u2(u3(x))
     S:
      fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
      fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
     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:
       u2#(u1(x)) -> u2#(x)
       u2#(g(x,y)) -> u2#(x)
       u2#(g(x,y)) -> u2#(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:
       
      S:
       fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
       fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
      AC-RPO Processor:
       argument filtering:
        pi(fAC) = [0,1]
        pi(g) = [0,1]
        pi(u1) = [0]
        pi(u2#) = [0]
       precedence:
        g > fAC > u1 > u2#
       status:
        g: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:
         
        S:
         fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
         fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
       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:
    u1#(g(x,y)) -> u1#(x)
    u1#(g(x,y)) -> u1#(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(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
    fAC(x,u1(y)) -> u1(fAC(x,y))
    fAC(x,u2(y)) -> u2(fAC(x,y))
    fAC(x,u3(y)) -> u3(fAC(x,y))
    u1(g(x,y)) -> g(u1(x),u1(y))
    u2(g(x,y)) -> g(u2(x),u2(y))
    u3(g(x,y)) -> g(u3(x),u3(y))
    u2(u1(x)) -> u1(u2(x))
    u3(u1(x)) -> u1(u3(x))
    u3(u2(x)) -> u2(u3(x))
   S:
    f{AC,#}(fAC(x10,x11),x12) -> f{AC,#}(x10,x11)
    f{AC,#}(x10,fAC(x11,x12)) -> f{AC,#}(x11,x12)
   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:
     u1#(g(x,y)) -> u1#(x)
     u1#(g(x,y)) -> u1#(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(x,g(y,z)) -> g(fAC(x,y),fAC(x,z))
     fAC(x,u1(y)) -> u1(fAC(x,y))
     fAC(x,u2(y)) -> u2(fAC(x,y))
     fAC(x,u3(y)) -> u3(fAC(x,y))
     u1(g(x,y)) -> g(u1(x),u1(y))
     u2(g(x,y)) -> g(u2(x),u2(y))
     u3(g(x,y)) -> g(u3(x),u3(y))
     u2(u1(x)) -> u1(u2(x))
     u3(u1(x)) -> u1(u3(x))
     u3(u2(x)) -> u2(u3(x))
    S:
     fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
     fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
    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:
      u1#(g(x,y)) -> u1#(x)
      u1#(g(x,y)) -> u1#(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:
      
     S:
      fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
      fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
     AC-RPO Processor:
      argument filtering:
       pi(fAC) = [0,1]
       pi(g) = [0,1]
       pi(u1#) = [0]
      precedence:
       g > u1# > fAC
      status:
       g: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:
        
       S:
        fAC(fAC(x10,x11),x12) -> fAC(x10,x11)
        fAC(x10,fAC(x11,x12)) -> fAC(x11,x12)
      Qed