MAYBE
Time: 0.461

Problem:
 Equations:
  +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
  +AC(x3,x4) -> +AC(x4,x3)
  *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5))
  *AC(x3,x4) -> *AC(x4,x3)
  UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5))
  UAC(x3,x4) -> UAC(x4,x3)
  +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
  +AC(x4,x3) -> +AC(x3,x4)
  *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5)
  *AC(x4,x3) -> *AC(x3,x4)
  UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5)
  UAC(x4,x3) -> UAC(x3,x4)
 TRS:
  +AC(0(),x) -> x
  +AC(s(x),s(y)) -> s(s(+AC(x,y)))
  *AC(0(),x) -> 0()
  *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y)))
  UAC(empty(),b) -> b
  sum(empty()) -> 0()
  sum(singl(x)) -> x
  sum(UAC(x,y)) -> +AC(sum(x),sum(y))
  prod(empty()) -> s(0())
  prod(singl(x)) -> x
  prod(UAC(x,y)) -> *AC(prod(x),prod(y))

Proof:
 DP Processor:
  Equations#:
   +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5))
   +{AC,#}(x3,x4) -> +{AC,#}(x4,x3)
   *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5))
   *{AC,#}(x3,x4) -> *{AC,#}(x4,x3)
   U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5))
   U{AC,#}(x3,x4) -> U{AC,#}(x4,x3)
   +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5)
   +{AC,#}(x4,x3) -> +{AC,#}(x3,x4)
   *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5)
   *{AC,#}(x4,x3) -> *{AC,#}(x3,x4)
   U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5)
   U{AC,#}(x4,x3) -> U{AC,#}(x3,x4)
  DPs:
   +{AC,#}(s(x),s(y)) -> +{AC,#}(x,y)
   *{AC,#}(s(x),s(y)) -> *{AC,#}(x,y)
   *{AC,#}(s(x),s(y)) -> +{AC,#}(x,y)
   *{AC,#}(s(x),s(y)) -> +{AC,#}(+AC(x,y),*AC(x,y))
   sum#(UAC(x,y)) -> sum#(y)
   sum#(UAC(x,y)) -> sum#(x)
   sum#(UAC(x,y)) -> +{AC,#}(sum(x),sum(y))
   prod#(UAC(x,y)) -> prod#(y)
   prod#(UAC(x,y)) -> prod#(x)
   prod#(UAC(x,y)) -> *{AC,#}(prod(x),prod(y))
   +{AC,#}(x6,+AC(0(),x)) -> +{AC,#}(x6,x)
   +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x,y)
   +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x7,s(s(+AC(x,y))))
   *{AC,#}(x8,*AC(0(),x)) -> *{AC,#}(x8,0())
   *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x,y)
   *{AC,#}(x9,*AC(s(x),s(y))) -> +{AC,#}(x,y)
   *{AC,#}(x9,*AC(s(x),s(y))) -> +{AC,#}(+AC(x,y),*AC(x,y))
   *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x9,s(+AC(+AC(x,y),*AC(x,y))))
   U{AC,#}(x10,UAC(empty(),b)) -> U{AC,#}(x10,b)
  Equations:
   +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
   +AC(x3,x4) -> +AC(x4,x3)
   *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5))
   *AC(x3,x4) -> *AC(x4,x3)
   UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5))
   UAC(x3,x4) -> UAC(x4,x3)
   +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
   +AC(x4,x3) -> +AC(x3,x4)
   *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5)
   *AC(x4,x3) -> *AC(x3,x4)
   UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5)
   UAC(x4,x3) -> UAC(x3,x4)
  TRS:
   +AC(0(),x) -> x
   +AC(s(x),s(y)) -> s(s(+AC(x,y)))
   *AC(0(),x) -> 0()
   *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y)))
   UAC(empty(),b) -> b
   sum(empty()) -> 0()
   sum(singl(x)) -> x
   sum(UAC(x,y)) -> +AC(sum(x),sum(y))
   prod(empty()) -> s(0())
   prod(singl(x)) -> x
   prod(UAC(x,y)) -> *AC(prod(x),prod(y))
  S:
   +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12)
   +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13)
   *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12)
   *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13)
   U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12)
   U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13)
  AC-EDG Processor:
   Equations#:
    +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5))
    +{AC,#}(x3,x4) -> +{AC,#}(x4,x3)
    *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5))
    *{AC,#}(x3,x4) -> *{AC,#}(x4,x3)
    U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5))
    U{AC,#}(x3,x4) -> U{AC,#}(x4,x3)
    +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5)
    +{AC,#}(x4,x3) -> +{AC,#}(x3,x4)
    *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5)
    *{AC,#}(x4,x3) -> *{AC,#}(x3,x4)
    U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5)
    U{AC,#}(x4,x3) -> U{AC,#}(x3,x4)
   DPs:
    +{AC,#}(s(x),s(y)) -> +{AC,#}(x,y)
    *{AC,#}(s(x),s(y)) -> *{AC,#}(x,y)
    *{AC,#}(s(x),s(y)) -> +{AC,#}(x,y)
    *{AC,#}(s(x),s(y)) -> +{AC,#}(+AC(x,y),*AC(x,y))
    sum#(UAC(x,y)) -> sum#(y)
    sum#(UAC(x,y)) -> sum#(x)
    sum#(UAC(x,y)) -> +{AC,#}(sum(x),sum(y))
    prod#(UAC(x,y)) -> prod#(y)
    prod#(UAC(x,y)) -> prod#(x)
    prod#(UAC(x,y)) -> *{AC,#}(prod(x),prod(y))
    +{AC,#}(x6,+AC(0(),x)) -> +{AC,#}(x6,x)
    +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x,y)
    +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x7,s(s(+AC(x,y))))
    *{AC,#}(x8,*AC(0(),x)) -> *{AC,#}(x8,0())
    *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x,y)
    *{AC,#}(x9,*AC(s(x),s(y))) -> +{AC,#}(x,y)
    *{AC,#}(x9,*AC(s(x),s(y))) -> +{AC,#}(+AC(x,y),*AC(x,y))
    *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x9,s(+AC(+AC(x,y),*AC(x,y))))
    U{AC,#}(x10,UAC(empty(),b)) -> U{AC,#}(x10,b)
   Equations:
    +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5))
    +AC(x3,x4) -> +AC(x4,x3)
    *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5))
    *AC(x3,x4) -> *AC(x4,x3)
    UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5))
    UAC(x3,x4) -> UAC(x4,x3)
    +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5)
    +AC(x4,x3) -> +AC(x3,x4)
    *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5)
    *AC(x4,x3) -> *AC(x3,x4)
    UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5)
    UAC(x4,x3) -> UAC(x3,x4)
   TRS:
    +AC(0(),x) -> x
    +AC(s(x),s(y)) -> s(s(+AC(x,y)))
    *AC(0(),x) -> 0()
    *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y)))
    UAC(empty(),b) -> b
    sum(empty()) -> 0()
    sum(singl(x)) -> x
    sum(UAC(x,y)) -> +AC(sum(x),sum(y))
    prod(empty()) -> s(0())
    prod(singl(x)) -> x
    prod(UAC(x,y)) -> *AC(prod(x),prod(y))
   S:
    +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12)
    +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13)
    *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12)
    *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13)
    U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12)
    U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13)
   Open