MAYBE
Time: 0.850

Problem:
 Equations:
  fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
  fAC(x3,x4) -> fAC(x4,x3)
  hAC(hAC(x3,x4),x5) -> hAC(x3,hAC(x4,x5))
  hAC(x3,x4) -> hAC(x4,x3)
  fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
  fAC(x4,x3) -> fAC(x3,x4)
  hAC(x3,hAC(x4,x5)) -> hAC(hAC(x3,x4),x5)
  hAC(x4,x3) -> hAC(x3,x4)
 TRS:
  fAC(hAC(g(g(x)),x),g(fAC(x,y))) -> fAC(hAC(g(x),g(x)),fAC(g(x),y))
  hAC(fAC(x,y),x) -> fAC(hAC(x,y),x)
  fAC(g(x),y) -> g(fAC(x,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)
   h{AC,#}(hAC(x3,x4),x5) -> h{AC,#}(x3,hAC(x4,x5))
   h{AC,#}(x3,x4) -> h{AC,#}(x4,x3)
   f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5)
   f{AC,#}(x4,x3) -> f{AC,#}(x3,x4)
   h{AC,#}(x3,hAC(x4,x5)) -> h{AC,#}(hAC(x3,x4),x5)
   h{AC,#}(x4,x3) -> h{AC,#}(x3,x4)
  DPs:
   f{AC,#}(hAC(g(g(x)),x),g(fAC(x,y))) -> f{AC,#}(g(x),y)
   f{AC,#}(hAC(g(g(x)),x),g(fAC(x,y))) -> h{AC,#}(g(x),g(x))
   f{AC,#}(hAC(g(g(x)),x),g(fAC(x,y))) -> f{AC,#}(hAC(g(x),g(x)),fAC(g(x),y))
   h{AC,#}(fAC(x,y),x) -> h{AC,#}(x,y)
   h{AC,#}(fAC(x,y),x) -> f{AC,#}(hAC(x,y),x)
   f{AC,#}(g(x),y) -> f{AC,#}(x,y)
   f{AC,#}(x6,fAC(hAC(g(g(x)),x),g(fAC(x,y)))) -> f{AC,#}(g(x),y)
   f{AC,#}(x6,fAC(hAC(g(g(x)),x),g(fAC(x,y)))) -> h{AC,#}(g(x),g(x))
   f{AC,#}(x6,fAC(hAC(g(g(x)),x),g(fAC(x,y)))) -> f{AC,#}(hAC(g(x),g(x)),fAC(g(x),y))
   f{AC,#}(x6,fAC(hAC(g(g(x)),x),g(fAC(x,y)))) -> f{AC,#}(x6,fAC(hAC(g(x),g(x)),fAC(g(x),y)))
   h{AC,#}(x7,hAC(fAC(x,y),x)) -> h{AC,#}(x,y)
   h{AC,#}(x7,hAC(fAC(x,y),x)) -> f{AC,#}(hAC(x,y),x)
   h{AC,#}(x7,hAC(fAC(x,y),x)) -> h{AC,#}(x7,fAC(hAC(x,y),x))
   f{AC,#}(x8,fAC(g(x),y)) -> f{AC,#}(x,y)
   f{AC,#}(x8,fAC(g(x),y)) -> f{AC,#}(x8,g(fAC(x,y)))
  Equations:
   fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
   fAC(x3,x4) -> fAC(x4,x3)
   hAC(hAC(x3,x4),x5) -> hAC(x3,hAC(x4,x5))
   hAC(x3,x4) -> hAC(x4,x3)
   fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
   fAC(x4,x3) -> fAC(x3,x4)
   hAC(x3,hAC(x4,x5)) -> hAC(hAC(x3,x4),x5)
   hAC(x4,x3) -> hAC(x3,x4)
  TRS:
   fAC(hAC(g(g(x)),x),g(fAC(x,y))) -> fAC(hAC(g(x),g(x)),fAC(g(x),y))
   hAC(fAC(x,y),x) -> fAC(hAC(x,y),x)
   fAC(g(x),y) -> g(fAC(x,y))
  S:
   f{AC,#}(fAC(x9,x10),x11) -> f{AC,#}(x9,x10)
   f{AC,#}(x9,fAC(x10,x11)) -> f{AC,#}(x10,x11)
   h{AC,#}(hAC(x9,x10),x11) -> h{AC,#}(x9,x10)
   h{AC,#}(x9,hAC(x10,x11)) -> h{AC,#}(x10,x11)
  AC-EDG Processor:
   Equations#:
    f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5))
    f{AC,#}(x3,x4) -> f{AC,#}(x4,x3)
    h{AC,#}(hAC(x3,x4),x5) -> h{AC,#}(x3,hAC(x4,x5))
    h{AC,#}(x3,x4) -> h{AC,#}(x4,x3)
    f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5)
    f{AC,#}(x4,x3) -> f{AC,#}(x3,x4)
    h{AC,#}(x3,hAC(x4,x5)) -> h{AC,#}(hAC(x3,x4),x5)
    h{AC,#}(x4,x3) -> h{AC,#}(x3,x4)
   DPs:
    f{AC,#}(hAC(g(g(x)),x),g(fAC(x,y))) -> f{AC,#}(g(x),y)
    f{AC,#}(hAC(g(g(x)),x),g(fAC(x,y))) -> h{AC,#}(g(x),g(x))
    f{AC,#}(hAC(g(g(x)),x),g(fAC(x,y))) -> f{AC,#}(hAC(g(x),g(x)),fAC(g(x),y))
    h{AC,#}(fAC(x,y),x) -> h{AC,#}(x,y)
    h{AC,#}(fAC(x,y),x) -> f{AC,#}(hAC(x,y),x)
    f{AC,#}(g(x),y) -> f{AC,#}(x,y)
    f{AC,#}(x6,fAC(hAC(g(g(x)),x),g(fAC(x,y)))) -> f{AC,#}(g(x),y)
    f{AC,#}(x6,fAC(hAC(g(g(x)),x),g(fAC(x,y)))) -> h{AC,#}(g(x),g(x))
    f{AC,#}(x6,fAC(hAC(g(g(x)),x),g(fAC(x,y)))) -> f{AC,#}(hAC(g(x),g(x)),fAC(g(x),y))
    f{AC,#}(x6,fAC(hAC(g(g(x)),x),g(fAC(x,y)))) -> f{AC,#}(x6,fAC(hAC(g(x),g(x)),fAC(g(x),y)))
    h{AC,#}(x7,hAC(fAC(x,y),x)) -> h{AC,#}(x,y)
    h{AC,#}(x7,hAC(fAC(x,y),x)) -> f{AC,#}(hAC(x,y),x)
    h{AC,#}(x7,hAC(fAC(x,y),x)) -> h{AC,#}(x7,fAC(hAC(x,y),x))
    f{AC,#}(x8,fAC(g(x),y)) -> f{AC,#}(x,y)
    f{AC,#}(x8,fAC(g(x),y)) -> f{AC,#}(x8,g(fAC(x,y)))
   Equations:
    fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5))
    fAC(x3,x4) -> fAC(x4,x3)
    hAC(hAC(x3,x4),x5) -> hAC(x3,hAC(x4,x5))
    hAC(x3,x4) -> hAC(x4,x3)
    fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5)
    fAC(x4,x3) -> fAC(x3,x4)
    hAC(x3,hAC(x4,x5)) -> hAC(hAC(x3,x4),x5)
    hAC(x4,x3) -> hAC(x3,x4)
   TRS:
    fAC(hAC(g(g(x)),x),g(fAC(x,y))) -> fAC(hAC(g(x),g(x)),fAC(g(x),y))
    hAC(fAC(x,y),x) -> fAC(hAC(x,y),x)
    fAC(g(x),y) -> g(fAC(x,y))
   S:
    f{AC,#}(fAC(x9,x10),x11) -> f{AC,#}(x9,x10)
    f{AC,#}(x9,fAC(x10,x11)) -> f{AC,#}(x10,x11)
    h{AC,#}(hAC(x9,x10),x11) -> h{AC,#}(x9,x10)
    h{AC,#}(x9,hAC(x10,x11)) -> h{AC,#}(x10,x11)
   Open