MAYBE
Time: 0.737

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)
   Open