MAYBE
Time: 1.289

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:
  0(#()) -> #()
  +AC(#(),x) -> x
  +AC(0(x),0(y)) -> 0(+AC(x,y))
  +AC(0(x),1(y)) -> 1(+AC(x,y))
  +AC(1(x),1(y)) -> 0(+AC(1(#()),+AC(x,y)))
  *AC(#(),x) -> #()
  *AC(0(x),y) -> 0(*AC(x,y))
  *AC(1(x),y) -> +AC(0(*AC(x,y)),y)
  UAC(empty(),b) -> b
  sum(empty()) -> 0(#())
  sum(singl(x)) -> x
  sum(UAC(x,y)) -> +AC(sum(x),sum(y))
  prod(empty()) -> 1(#())
  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,#}(0(x),0(y)) -> +{AC,#}(x,y)
   +{AC,#}(0(x),0(y)) -> 0#(+AC(x,y))
   +{AC,#}(0(x),1(y)) -> +{AC,#}(x,y)
   +{AC,#}(1(x),1(y)) -> +{AC,#}(x,y)
   +{AC,#}(1(x),1(y)) -> +{AC,#}(1(#()),+AC(x,y))
   +{AC,#}(1(x),1(y)) -> 0#(+AC(1(#()),+AC(x,y)))
   *{AC,#}(0(x),y) -> *{AC,#}(x,y)
   *{AC,#}(0(x),y) -> 0#(*AC(x,y))
   *{AC,#}(1(x),y) -> *{AC,#}(x,y)
   *{AC,#}(1(x),y) -> 0#(*AC(x,y))
   *{AC,#}(1(x),y) -> +{AC,#}(0(*AC(x,y)),y)
   sum#(empty()) -> 0#(#())
   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(#(),x)) -> +{AC,#}(x6,x)
   +{AC,#}(x7,+AC(0(x),0(y))) -> +{AC,#}(x,y)
   +{AC,#}(x7,+AC(0(x),0(y))) -> 0#(+AC(x,y))
   +{AC,#}(x7,+AC(0(x),0(y))) -> +{AC,#}(x7,0(+AC(x,y)))
   +{AC,#}(x8,+AC(0(x),1(y))) -> +{AC,#}(x,y)
   +{AC,#}(x8,+AC(0(x),1(y))) -> +{AC,#}(x8,1(+AC(x,y)))
   +{AC,#}(x9,+AC(1(x),1(y))) -> +{AC,#}(x,y)
   +{AC,#}(x9,+AC(1(x),1(y))) -> +{AC,#}(1(#()),+AC(x,y))
   +{AC,#}(x9,+AC(1(x),1(y))) -> 0#(+AC(1(#()),+AC(x,y)))
   +{AC,#}(x9,+AC(1(x),1(y))) -> +{AC,#}(x9,0(+AC(1(#()),+AC(x,y))))
   *{AC,#}(x10,*AC(#(),x)) -> *{AC,#}(x10,#())
   *{AC,#}(x11,*AC(0(x),y)) -> *{AC,#}(x,y)
   *{AC,#}(x11,*AC(0(x),y)) -> 0#(*AC(x,y))
   *{AC,#}(x11,*AC(0(x),y)) -> *{AC,#}(x11,0(*AC(x,y)))
   *{AC,#}(x12,*AC(1(x),y)) -> *{AC,#}(x,y)
   *{AC,#}(x12,*AC(1(x),y)) -> 0#(*AC(x,y))
   *{AC,#}(x12,*AC(1(x),y)) -> +{AC,#}(0(*AC(x,y)),y)
   *{AC,#}(x12,*AC(1(x),y)) -> *{AC,#}(x12,+AC(0(*AC(x,y)),y))
   U{AC,#}(x13,UAC(empty(),b)) -> U{AC,#}(x13,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:
   0(#()) -> #()
   +AC(#(),x) -> x
   +AC(0(x),0(y)) -> 0(+AC(x,y))
   +AC(0(x),1(y)) -> 1(+AC(x,y))
   +AC(1(x),1(y)) -> 0(+AC(1(#()),+AC(x,y)))
   *AC(#(),x) -> #()
   *AC(0(x),y) -> 0(*AC(x,y))
   *AC(1(x),y) -> +AC(0(*AC(x,y)),y)
   UAC(empty(),b) -> b
   sum(empty()) -> 0(#())
   sum(singl(x)) -> x
   sum(UAC(x,y)) -> +AC(sum(x),sum(y))
   prod(empty()) -> 1(#())
   prod(singl(x)) -> x
   prod(UAC(x,y)) -> *AC(prod(x),prod(y))
  S:
   +{AC,#}(+AC(x14,x15),x16) -> +{AC,#}(x14,x15)
   +{AC,#}(x14,+AC(x15,x16)) -> +{AC,#}(x15,x16)
   *{AC,#}(*AC(x14,x15),x16) -> *{AC,#}(x14,x15)
   *{AC,#}(x14,*AC(x15,x16)) -> *{AC,#}(x15,x16)
   U{AC,#}(UAC(x14,x15),x16) -> U{AC,#}(x14,x15)
   U{AC,#}(x14,UAC(x15,x16)) -> U{AC,#}(x15,x16)
  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,#}(0(x),0(y)) -> +{AC,#}(x,y)
    +{AC,#}(0(x),0(y)) -> 0#(+AC(x,y))
    +{AC,#}(0(x),1(y)) -> +{AC,#}(x,y)
    +{AC,#}(1(x),1(y)) -> +{AC,#}(x,y)
    +{AC,#}(1(x),1(y)) -> +{AC,#}(1(#()),+AC(x,y))
    +{AC,#}(1(x),1(y)) -> 0#(+AC(1(#()),+AC(x,y)))
    *{AC,#}(0(x),y) -> *{AC,#}(x,y)
    *{AC,#}(0(x),y) -> 0#(*AC(x,y))
    *{AC,#}(1(x),y) -> *{AC,#}(x,y)
    *{AC,#}(1(x),y) -> 0#(*AC(x,y))
    *{AC,#}(1(x),y) -> +{AC,#}(0(*AC(x,y)),y)
    sum#(empty()) -> 0#(#())
    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(#(),x)) -> +{AC,#}(x6,x)
    +{AC,#}(x7,+AC(0(x),0(y))) -> +{AC,#}(x,y)
    +{AC,#}(x7,+AC(0(x),0(y))) -> 0#(+AC(x,y))
    +{AC,#}(x7,+AC(0(x),0(y))) -> +{AC,#}(x7,0(+AC(x,y)))
    +{AC,#}(x8,+AC(0(x),1(y))) -> +{AC,#}(x,y)
    +{AC,#}(x8,+AC(0(x),1(y))) -> +{AC,#}(x8,1(+AC(x,y)))
    +{AC,#}(x9,+AC(1(x),1(y))) -> +{AC,#}(x,y)
    +{AC,#}(x9,+AC(1(x),1(y))) -> +{AC,#}(1(#()),+AC(x,y))
    +{AC,#}(x9,+AC(1(x),1(y))) -> 0#(+AC(1(#()),+AC(x,y)))
    +{AC,#}(x9,+AC(1(x),1(y))) -> +{AC,#}(x9,0(+AC(1(#()),+AC(x,y))))
    *{AC,#}(x10,*AC(#(),x)) -> *{AC,#}(x10,#())
    *{AC,#}(x11,*AC(0(x),y)) -> *{AC,#}(x,y)
    *{AC,#}(x11,*AC(0(x),y)) -> 0#(*AC(x,y))
    *{AC,#}(x11,*AC(0(x),y)) -> *{AC,#}(x11,0(*AC(x,y)))
    *{AC,#}(x12,*AC(1(x),y)) -> *{AC,#}(x,y)
    *{AC,#}(x12,*AC(1(x),y)) -> 0#(*AC(x,y))
    *{AC,#}(x12,*AC(1(x),y)) -> +{AC,#}(0(*AC(x,y)),y)
    *{AC,#}(x12,*AC(1(x),y)) -> *{AC,#}(x12,+AC(0(*AC(x,y)),y))
    U{AC,#}(x13,UAC(empty(),b)) -> U{AC,#}(x13,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:
    0(#()) -> #()
    +AC(#(),x) -> x
    +AC(0(x),0(y)) -> 0(+AC(x,y))
    +AC(0(x),1(y)) -> 1(+AC(x,y))
    +AC(1(x),1(y)) -> 0(+AC(1(#()),+AC(x,y)))
    *AC(#(),x) -> #()
    *AC(0(x),y) -> 0(*AC(x,y))
    *AC(1(x),y) -> +AC(0(*AC(x,y)),y)
    UAC(empty(),b) -> b
    sum(empty()) -> 0(#())
    sum(singl(x)) -> x
    sum(UAC(x,y)) -> +AC(sum(x),sum(y))
    prod(empty()) -> 1(#())
    prod(singl(x)) -> x
    prod(UAC(x,y)) -> *AC(prod(x),prod(y))
   S:
    +{AC,#}(+AC(x14,x15),x16) -> +{AC,#}(x14,x15)
    +{AC,#}(x14,+AC(x15,x16)) -> +{AC,#}(x15,x16)
    *{AC,#}(*AC(x14,x15),x16) -> *{AC,#}(x14,x15)
    *{AC,#}(x14,*AC(x15,x16)) -> *{AC,#}(x15,x16)
    U{AC,#}(UAC(x14,x15),x16) -> U{AC,#}(x14,x15)
    U{AC,#}(x14,UAC(x15,x16)) -> U{AC,#}(x15,x16)
   Open