MAYBE
Time: 0.394

Problem:
 Equations:
  fAC(fAC(x5,x6),x12) -> fAC(x5,fAC(x6,x12))
  fAC(x5,x6) -> fAC(x6,x5)
  fAC(x5,fAC(x6,x12)) -> fAC(fAC(x5,x6),x12)
  fAC(x6,x5) -> fAC(x5,x6)
 TRS:
  fAC(h(x1),fAC(h(a()),g(a()))) -> h(x1)
  fAC(g(x1),fAC(h(a()),g(a()))) -> g(x1)
  fAC(a(),x1) -> fAC(h(x1),h(a()))
  fAC(a(),x1) -> fAC(g(x1),g(a()))
  fAC(g(x2),h(x1)) -> fAC(g(x1),h(x2))

Proof:
 DP Processor:
  Equations#:
   f{AC,#}(fAC(x5,x6),x12) -> f{AC,#}(x5,fAC(x6,x12))
   f{AC,#}(x5,x6) -> f{AC,#}(x6,x5)
   f{AC,#}(x5,fAC(x6,x12)) -> f{AC,#}(fAC(x5,x6),x12)
   f{AC,#}(x6,x5) -> f{AC,#}(x5,x6)
  DPs:
   f{AC,#}(a(),x1) -> f{AC,#}(h(x1),h(a()))
   f{AC,#}(a(),x1) -> f{AC,#}(g(x1),g(a()))
   f{AC,#}(g(x2),h(x1)) -> f{AC,#}(g(x1),h(x2))
   f{AC,#}(x7,fAC(h(x1),fAC(h(a()),g(a())))) -> f{AC,#}(x7,h(x1))
   f{AC,#}(x8,fAC(g(x1),fAC(h(a()),g(a())))) -> f{AC,#}(x8,g(x1))
   f{AC,#}(x9,fAC(a(),x1)) -> f{AC,#}(h(x1),h(a()))
   f{AC,#}(x9,fAC(a(),x1)) -> f{AC,#}(x9,fAC(h(x1),h(a())))
   f{AC,#}(x10,fAC(a(),x1)) -> f{AC,#}(g(x1),g(a()))
   f{AC,#}(x10,fAC(a(),x1)) -> f{AC,#}(x10,fAC(g(x1),g(a())))
   f{AC,#}(x11,fAC(g(x2),h(x1))) -> f{AC,#}(g(x1),h(x2))
   f{AC,#}(x11,fAC(g(x2),h(x1))) -> f{AC,#}(x11,fAC(g(x1),h(x2)))
  Equations:
   fAC(fAC(x5,x6),x12) -> fAC(x5,fAC(x6,x12))
   fAC(x5,x6) -> fAC(x6,x5)
   fAC(x5,fAC(x6,x12)) -> fAC(fAC(x5,x6),x12)
   fAC(x6,x5) -> fAC(x5,x6)
  TRS:
   fAC(h(x1),fAC(h(a()),g(a()))) -> h(x1)
   fAC(g(x1),fAC(h(a()),g(a()))) -> g(x1)
   fAC(a(),x1) -> fAC(h(x1),h(a()))
   fAC(a(),x1) -> fAC(g(x1),g(a()))
   fAC(g(x2),h(x1)) -> fAC(g(x1),h(x2))
  S:
   f{AC,#}(fAC(x13,x14),x23) -> f{AC,#}(x13,x14)
   f{AC,#}(x13,fAC(x14,x23)) -> f{AC,#}(x14,x23)
  AC-EDG Processor:
   Equations#:
    f{AC,#}(fAC(x5,x6),x12) -> f{AC,#}(x5,fAC(x6,x12))
    f{AC,#}(x5,x6) -> f{AC,#}(x6,x5)
    f{AC,#}(x5,fAC(x6,x12)) -> f{AC,#}(fAC(x5,x6),x12)
    f{AC,#}(x6,x5) -> f{AC,#}(x5,x6)
   DPs:
    f{AC,#}(a(),x1) -> f{AC,#}(h(x1),h(a()))
    f{AC,#}(a(),x1) -> f{AC,#}(g(x1),g(a()))
    f{AC,#}(g(x2),h(x1)) -> f{AC,#}(g(x1),h(x2))
    f{AC,#}(x7,fAC(h(x1),fAC(h(a()),g(a())))) -> f{AC,#}(x7,h(x1))
    f{AC,#}(x8,fAC(g(x1),fAC(h(a()),g(a())))) -> f{AC,#}(x8,g(x1))
    f{AC,#}(x9,fAC(a(),x1)) -> f{AC,#}(h(x1),h(a()))
    f{AC,#}(x9,fAC(a(),x1)) -> f{AC,#}(x9,fAC(h(x1),h(a())))
    f{AC,#}(x10,fAC(a(),x1)) -> f{AC,#}(g(x1),g(a()))
    f{AC,#}(x10,fAC(a(),x1)) -> f{AC,#}(x10,fAC(g(x1),g(a())))
    f{AC,#}(x11,fAC(g(x2),h(x1))) -> f{AC,#}(g(x1),h(x2))
    f{AC,#}(x11,fAC(g(x2),h(x1))) -> f{AC,#}(x11,fAC(g(x1),h(x2)))
   Equations:
    fAC(fAC(x5,x6),x12) -> fAC(x5,fAC(x6,x12))
    fAC(x5,x6) -> fAC(x6,x5)
    fAC(x5,fAC(x6,x12)) -> fAC(fAC(x5,x6),x12)
    fAC(x6,x5) -> fAC(x5,x6)
   TRS:
    fAC(h(x1),fAC(h(a()),g(a()))) -> h(x1)
    fAC(g(x1),fAC(h(a()),g(a()))) -> g(x1)
    fAC(a(),x1) -> fAC(h(x1),h(a()))
    fAC(a(),x1) -> fAC(g(x1),g(a()))
    fAC(g(x2),h(x1)) -> fAC(g(x1),h(x2))
   S:
    f{AC,#}(fAC(x13,x14),x23) -> f{AC,#}(x13,x14)
    f{AC,#}(x13,fAC(x14,x23)) -> f{AC,#}(x14,x23)
   Open