MAYBE
Time: 0.253

Problem:
 Equations:
  +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
  +AC(x3,x4) -> +AC(x4,x3)
  +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
  +AC(x4,x3) -> +AC(x3,x4)
 TRS:
  +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
  k(a(),g(g(a()))) -> k(g(a()),f(a()))
  +AC(g(x),y) -> g(+AC(x,y))
  f(+AC(x,y)) -> +AC(f(x),y)
  k(a(),b()) -> k(b(),a())
  k(g(a()),a()) -> k(a(),g(b()))
  k(g(a()),b()) -> k(a(),g(a()))

Proof:
 DP Processor:
  Equations#:
   +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5))
   +{AC,#}(x3,x4) -> +{AC,#}(x4,x3)
   +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5)
   +{AC,#}(x4,x3) -> +{AC,#}(x3,x4)
  DPs:
   +{AC,#}(f(b()),g(a())) -> f#(a())
   +{AC,#}(f(b()),g(a())) -> +{AC,#}(f(a()),g(b()))
   k#(a(),g(g(a()))) -> f#(a())
   k#(a(),g(g(a()))) -> k#(g(a()),f(a()))
   +{AC,#}(g(x),y) -> +{AC,#}(x,y)
   f#(+AC(x,y)) -> f#(x)
   f#(+AC(x,y)) -> +{AC,#}(f(x),y)
   k#(a(),b()) -> k#(b(),a())
   k#(g(a()),a()) -> k#(a(),g(b()))
   k#(g(a()),b()) -> k#(a(),g(a()))
   +{AC,#}(x6,+AC(f(b()),g(a()))) -> f#(a())
   +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(f(a()),g(b()))
   +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(x6,+AC(f(a()),g(b())))
   +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x,y)
   +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x7,g(+AC(x,y)))
  Equations:
   +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
   +AC(x3,x4) -> +AC(x4,x3)
   +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
   +AC(x4,x3) -> +AC(x3,x4)
  TRS:
   +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
   k(a(),g(g(a()))) -> k(g(a()),f(a()))
   +AC(g(x),y) -> g(+AC(x,y))
   f(+AC(x,y)) -> +AC(f(x),y)
   k(a(),b()) -> k(b(),a())
   k(g(a()),a()) -> k(a(),g(b()))
   k(g(a()),b()) -> k(a(),g(a()))
  S:
   +{AC,#}(+AC(x8,x9),x10) -> +{AC,#}(x8,x9)
   +{AC,#}(x8,+AC(x9,x10)) -> +{AC,#}(x9,x10)
  AC-EDG Processor:
   Equations#:
    +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5))
    +{AC,#}(x3,x4) -> +{AC,#}(x4,x3)
    +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5)
    +{AC,#}(x4,x3) -> +{AC,#}(x3,x4)
   DPs:
    +{AC,#}(f(b()),g(a())) -> f#(a())
    +{AC,#}(f(b()),g(a())) -> +{AC,#}(f(a()),g(b()))
    k#(a(),g(g(a()))) -> f#(a())
    k#(a(),g(g(a()))) -> k#(g(a()),f(a()))
    +{AC,#}(g(x),y) -> +{AC,#}(x,y)
    f#(+AC(x,y)) -> f#(x)
    f#(+AC(x,y)) -> +{AC,#}(f(x),y)
    k#(a(),b()) -> k#(b(),a())
    k#(g(a()),a()) -> k#(a(),g(b()))
    k#(g(a()),b()) -> k#(a(),g(a()))
    +{AC,#}(x6,+AC(f(b()),g(a()))) -> f#(a())
    +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(f(a()),g(b()))
    +{AC,#}(x6,+AC(f(b()),g(a()))) -> +{AC,#}(x6,+AC(f(a()),g(b())))
    +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x,y)
    +{AC,#}(x7,+AC(g(x),y)) -> +{AC,#}(x7,g(+AC(x,y)))
   Equations:
    +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
    +AC(x3,x4) -> +AC(x4,x3)
    +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
    +AC(x4,x3) -> +AC(x3,x4)
   TRS:
    +AC(f(b()),g(a())) -> +AC(f(a()),g(b()))
    k(a(),g(g(a()))) -> k(g(a()),f(a()))
    +AC(g(x),y) -> g(+AC(x,y))
    f(+AC(x,y)) -> +AC(f(x),y)
    k(a(),b()) -> k(b(),a())
    k(g(a()),a()) -> k(a(),g(b()))
    k(g(a()),b()) -> k(a(),g(a()))
   S:
    +{AC,#}(+AC(x8,x9),x10) -> +{AC,#}(x8,x9)
    +{AC,#}(x8,+AC(x9,x10)) -> +{AC,#}(x9,x10)
   Open