MAYBE
Time: 1.358

Problem:
 Equations:
  +AC(+AC(x4,x5),x6) -> +AC(x4,+AC(x5,x6))
  +AC(x4,x5) -> +AC(x5,x4)
  *AC(*AC(x4,x5),x6) -> *AC(x4,*AC(x5,x6))
  *AC(x4,x5) -> *AC(x5,x4)
  UAC(UAC(x4,x5),x6) -> UAC(x4,UAC(x5,x6))
  UAC(x4,x5) -> UAC(x5,x4)
  +AC(x4,+AC(x5,x6)) -> +AC(+AC(x4,x5),x6)
  +AC(x5,x4) -> +AC(x4,x5)
  *AC(x4,*AC(x5,x6)) -> *AC(*AC(x4,x5),x6)
  *AC(x5,x4) -> *AC(x4,x5)
  UAC(x4,UAC(x5,x6)) -> UAC(UAC(x4,x5),x6)
  UAC(x5,x4) -> UAC(x4,x5)
 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)
  *AC(+AC(y,z),x) -> +AC(*AC(x,y),*AC(x,z))
  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(x4,x5),x6) -> +{AC,#}(x4,+AC(x5,x6))
   +{AC,#}(x4,x5) -> +{AC,#}(x5,x4)
   *{AC,#}(*AC(x4,x5),x6) -> *{AC,#}(x4,*AC(x5,x6))
   *{AC,#}(x4,x5) -> *{AC,#}(x5,x4)
   U{AC,#}(UAC(x4,x5),x6) -> U{AC,#}(x4,UAC(x5,x6))
   U{AC,#}(x4,x5) -> U{AC,#}(x5,x4)
   +{AC,#}(x4,+AC(x5,x6)) -> +{AC,#}(+AC(x4,x5),x6)
   +{AC,#}(x5,x4) -> +{AC,#}(x4,x5)
   *{AC,#}(x4,*AC(x5,x6)) -> *{AC,#}(*AC(x4,x5),x6)
   *{AC,#}(x5,x4) -> *{AC,#}(x4,x5)
   U{AC,#}(x4,UAC(x5,x6)) -> U{AC,#}(UAC(x4,x5),x6)
   U{AC,#}(x5,x4) -> U{AC,#}(x4,x5)
  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)
   *{AC,#}(+AC(y,z),x) -> *{AC,#}(x,z)
   *{AC,#}(+AC(y,z),x) -> *{AC,#}(x,y)
   *{AC,#}(+AC(y,z),x) -> +{AC,#}(*AC(x,y),*AC(x,z))
   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,#}(x7,+AC(#(),x)) -> +{AC,#}(x7,x)
   +{AC,#}(x8,+AC(0(x),0(y))) -> +{AC,#}(x,y)
   +{AC,#}(x8,+AC(0(x),0(y))) -> 0#(+AC(x,y))
   +{AC,#}(x8,+AC(0(x),0(y))) -> +{AC,#}(x8,0(+AC(x,y)))
   +{AC,#}(x9,+AC(0(x),1(y))) -> +{AC,#}(x,y)
   +{AC,#}(x9,+AC(0(x),1(y))) -> +{AC,#}(x9,1(+AC(x,y)))
   +{AC,#}(x10,+AC(1(x),1(y))) -> +{AC,#}(x,y)
   +{AC,#}(x10,+AC(1(x),1(y))) -> +{AC,#}(1(#()),+AC(x,y))
   +{AC,#}(x10,+AC(1(x),1(y))) -> 0#(+AC(1(#()),+AC(x,y)))
   +{AC,#}(x10,+AC(1(x),1(y))) -> +{AC,#}(x10,0(+AC(1(#()),+AC(x,y))))
   *{AC,#}(x11,*AC(#(),x)) -> *{AC,#}(x11,#())
   *{AC,#}(x12,*AC(0(x),y)) -> *{AC,#}(x,y)
   *{AC,#}(x12,*AC(0(x),y)) -> 0#(*AC(x,y))
   *{AC,#}(x12,*AC(0(x),y)) -> *{AC,#}(x12,0(*AC(x,y)))
   *{AC,#}(x13,*AC(1(x),y)) -> *{AC,#}(x,y)
   *{AC,#}(x13,*AC(1(x),y)) -> 0#(*AC(x,y))
   *{AC,#}(x13,*AC(1(x),y)) -> +{AC,#}(0(*AC(x,y)),y)
   *{AC,#}(x13,*AC(1(x),y)) -> *{AC,#}(x13,+AC(0(*AC(x,y)),y))
   *{AC,#}(x14,*AC(+AC(y,z),x)) -> *{AC,#}(x,z)
   *{AC,#}(x14,*AC(+AC(y,z),x)) -> *{AC,#}(x,y)
   *{AC,#}(x14,*AC(+AC(y,z),x)) -> +{AC,#}(*AC(x,y),*AC(x,z))
   *{AC,#}(x14,*AC(+AC(y,z),x)) -> *{AC,#}(x14,+AC(*AC(x,y),*AC(x,z)))
   U{AC,#}(x15,UAC(empty(),b)) -> U{AC,#}(x15,b)
  Equations:
   +AC(+AC(x4,x5),x6) -> +AC(x4,+AC(x5,x6))
   +AC(x4,x5) -> +AC(x5,x4)
   *AC(*AC(x4,x5),x6) -> *AC(x4,*AC(x5,x6))
   *AC(x4,x5) -> *AC(x5,x4)
   UAC(UAC(x4,x5),x6) -> UAC(x4,UAC(x5,x6))
   UAC(x4,x5) -> UAC(x5,x4)
   +AC(x4,+AC(x5,x6)) -> +AC(+AC(x4,x5),x6)
   +AC(x5,x4) -> +AC(x4,x5)
   *AC(x4,*AC(x5,x6)) -> *AC(*AC(x4,x5),x6)
   *AC(x5,x4) -> *AC(x4,x5)
   UAC(x4,UAC(x5,x6)) -> UAC(UAC(x4,x5),x6)
   UAC(x5,x4) -> UAC(x4,x5)
  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)
   *AC(+AC(y,z),x) -> +AC(*AC(x,y),*AC(x,z))
   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(x16,x17),x18) -> +{AC,#}(x16,x17)
   +{AC,#}(x16,+AC(x17,x18)) -> +{AC,#}(x17,x18)
   *{AC,#}(*AC(x16,x17),x18) -> *{AC,#}(x16,x17)
   *{AC,#}(x16,*AC(x17,x18)) -> *{AC,#}(x17,x18)
   U{AC,#}(UAC(x16,x17),x18) -> U{AC,#}(x16,x17)
   U{AC,#}(x16,UAC(x17,x18)) -> U{AC,#}(x17,x18)
  AC-EDG Processor:
   Equations#:
    +{AC,#}(+AC(x4,x5),x6) -> +{AC,#}(x4,+AC(x5,x6))
    +{AC,#}(x4,x5) -> +{AC,#}(x5,x4)
    *{AC,#}(*AC(x4,x5),x6) -> *{AC,#}(x4,*AC(x5,x6))
    *{AC,#}(x4,x5) -> *{AC,#}(x5,x4)
    U{AC,#}(UAC(x4,x5),x6) -> U{AC,#}(x4,UAC(x5,x6))
    U{AC,#}(x4,x5) -> U{AC,#}(x5,x4)
    +{AC,#}(x4,+AC(x5,x6)) -> +{AC,#}(+AC(x4,x5),x6)
    +{AC,#}(x5,x4) -> +{AC,#}(x4,x5)
    *{AC,#}(x4,*AC(x5,x6)) -> *{AC,#}(*AC(x4,x5),x6)
    *{AC,#}(x5,x4) -> *{AC,#}(x4,x5)
    U{AC,#}(x4,UAC(x5,x6)) -> U{AC,#}(UAC(x4,x5),x6)
    U{AC,#}(x5,x4) -> U{AC,#}(x4,x5)
   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)
    *{AC,#}(+AC(y,z),x) -> *{AC,#}(x,z)
    *{AC,#}(+AC(y,z),x) -> *{AC,#}(x,y)
    *{AC,#}(+AC(y,z),x) -> +{AC,#}(*AC(x,y),*AC(x,z))
    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,#}(x7,+AC(#(),x)) -> +{AC,#}(x7,x)
    +{AC,#}(x8,+AC(0(x),0(y))) -> +{AC,#}(x,y)
    +{AC,#}(x8,+AC(0(x),0(y))) -> 0#(+AC(x,y))
    +{AC,#}(x8,+AC(0(x),0(y))) -> +{AC,#}(x8,0(+AC(x,y)))
    +{AC,#}(x9,+AC(0(x),1(y))) -> +{AC,#}(x,y)
    +{AC,#}(x9,+AC(0(x),1(y))) -> +{AC,#}(x9,1(+AC(x,y)))
    +{AC,#}(x10,+AC(1(x),1(y))) -> +{AC,#}(x,y)
    +{AC,#}(x10,+AC(1(x),1(y))) -> +{AC,#}(1(#()),+AC(x,y))
    +{AC,#}(x10,+AC(1(x),1(y))) -> 0#(+AC(1(#()),+AC(x,y)))
    +{AC,#}(x10,+AC(1(x),1(y))) -> +{AC,#}(x10,0(+AC(1(#()),+AC(x,y))))
    *{AC,#}(x11,*AC(#(),x)) -> *{AC,#}(x11,#())
    *{AC,#}(x12,*AC(0(x),y)) -> *{AC,#}(x,y)
    *{AC,#}(x12,*AC(0(x),y)) -> 0#(*AC(x,y))
    *{AC,#}(x12,*AC(0(x),y)) -> *{AC,#}(x12,0(*AC(x,y)))
    *{AC,#}(x13,*AC(1(x),y)) -> *{AC,#}(x,y)
    *{AC,#}(x13,*AC(1(x),y)) -> 0#(*AC(x,y))
    *{AC,#}(x13,*AC(1(x),y)) -> +{AC,#}(0(*AC(x,y)),y)
    *{AC,#}(x13,*AC(1(x),y)) -> *{AC,#}(x13,+AC(0(*AC(x,y)),y))
    *{AC,#}(x14,*AC(+AC(y,z),x)) -> *{AC,#}(x,z)
    *{AC,#}(x14,*AC(+AC(y,z),x)) -> *{AC,#}(x,y)
    *{AC,#}(x14,*AC(+AC(y,z),x)) -> +{AC,#}(*AC(x,y),*AC(x,z))
    *{AC,#}(x14,*AC(+AC(y,z),x)) -> *{AC,#}(x14,+AC(*AC(x,y),*AC(x,z)))
    U{AC,#}(x15,UAC(empty(),b)) -> U{AC,#}(x15,b)
   Equations:
    +AC(+AC(x4,x5),x6) -> +AC(x4,+AC(x5,x6))
    +AC(x4,x5) -> +AC(x5,x4)
    *AC(*AC(x4,x5),x6) -> *AC(x4,*AC(x5,x6))
    *AC(x4,x5) -> *AC(x5,x4)
    UAC(UAC(x4,x5),x6) -> UAC(x4,UAC(x5,x6))
    UAC(x4,x5) -> UAC(x5,x4)
    +AC(x4,+AC(x5,x6)) -> +AC(+AC(x4,x5),x6)
    +AC(x5,x4) -> +AC(x4,x5)
    *AC(x4,*AC(x5,x6)) -> *AC(*AC(x4,x5),x6)
    *AC(x5,x4) -> *AC(x4,x5)
    UAC(x4,UAC(x5,x6)) -> UAC(UAC(x4,x5),x6)
    UAC(x5,x4) -> UAC(x4,x5)
   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)
    *AC(+AC(y,z),x) -> +AC(*AC(x,y),*AC(x,z))
    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(x16,x17),x18) -> +{AC,#}(x16,x17)
    +{AC,#}(x16,+AC(x17,x18)) -> +{AC,#}(x17,x18)
    *{AC,#}(*AC(x16,x17),x18) -> *{AC,#}(x16,x17)
    *{AC,#}(x16,*AC(x17,x18)) -> *{AC,#}(x17,x18)
    U{AC,#}(UAC(x16,x17),x18) -> U{AC,#}(x16,x17)
    U{AC,#}(x16,UAC(x17,x18)) -> U{AC,#}(x17,x18)
   Open