MAYBE
Time: 2.247

Problem:
 Equations:
  unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
  unionAC(x5,x6) -> unionAC(x6,x5)
  multAC(multAC(x5,x6),x7) -> multAC(x5,multAC(x6,x7))
  multAC(x5,x6) -> multAC(x6,x5)
  plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7))
  plusAC(x5,x6) -> plusAC(x6,x5)
  unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
  unionAC(x6,x5) -> unionAC(x5,x6)
  multAC(x5,multAC(x6,x7)) -> multAC(multAC(x5,x6),x7)
  multAC(x6,x5) -> multAC(x5,x6)
  plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7)
  plusAC(x6,x5) -> plusAC(x5,x6)
 TRS:
  unionAC(X,empty()) -> X
  unionAC(empty(),X) -> X
  0(z()) -> z()
  U11(tt(),X,Y) -> U12(tt(),X,Y)
  U12(tt(),X,Y) -> 0(multAC(X,Y))
  U21(tt(),X,Y) -> U22(tt(),X,Y)
  U22(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y)
  U31(tt(),X,Y) -> U32(tt(),X,Y)
  U32(tt(),X,Y) -> 0(plusAC(X,Y))
  U41(tt(),X,Y) -> U42(tt(),X,Y)
  U42(tt(),X,Y) -> 1(plusAC(X,Y))
  U51(tt(),X,Y) -> U52(tt(),X,Y)
  U52(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z())))
  U61(tt(),A,B) -> U62(tt(),A,B)
  U62(tt(),A,B) -> multAC(prod(A),prod(B))
  U71(tt(),A,B) -> U72(tt(),A,B)
  U72(tt(),A,B) -> plusAC(sum(A),sum(B))
  multAC(z(),X) -> z()
  multAC(0(X),Y) -> U11(tt(),X,Y)
  multAC(1(X),Y) -> U21(tt(),X,Y)
  plusAC(z(),X) -> X
  plusAC(0(X),0(Y)) -> U31(tt(),X,Y)
  plusAC(0(X),1(Y)) -> U41(tt(),X,Y)
  plusAC(1(X),1(Y)) -> U51(tt(),X,Y)
  prod(empty()) -> 1(z())
  prod(singl(X)) -> X
  prod(unionAC(A,B)) -> U61(tt(),A,B)
  sum(empty()) -> 0(z())
  sum(singl(X)) -> X
  sum(unionAC(A,B)) -> U71(tt(),A,B)

Proof:
 DP Processor:
  Equations#:
   union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7))
   union{AC,#}(x5,x6) -> union{AC,#}(x6,x5)
   mult{AC,#}(multAC(x5,x6),x7) -> mult{AC,#}(x5,multAC(x6,x7))
   mult{AC,#}(x5,x6) -> mult{AC,#}(x6,x5)
   plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7))
   plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5)
   union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7)
   union{AC,#}(x6,x5) -> union{AC,#}(x5,x6)
   mult{AC,#}(x5,multAC(x6,x7)) -> mult{AC,#}(multAC(x5,x6),x7)
   mult{AC,#}(x6,x5) -> mult{AC,#}(x5,x6)
   plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7)
   plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6)
  DPs:
   U11#(tt(),X,Y) -> U12#(tt(),X,Y)
   U12#(tt(),X,Y) -> mult{AC,#}(X,Y)
   U12#(tt(),X,Y) -> 0#(multAC(X,Y))
   U21#(tt(),X,Y) -> U22#(tt(),X,Y)
   U22#(tt(),X,Y) -> mult{AC,#}(X,Y)
   U22#(tt(),X,Y) -> 0#(multAC(X,Y))
   U22#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y)
   U31#(tt(),X,Y) -> U32#(tt(),X,Y)
   U32#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U32#(tt(),X,Y) -> 0#(plusAC(X,Y))
   U41#(tt(),X,Y) -> U42#(tt(),X,Y)
   U42#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U51#(tt(),X,Y) -> U52#(tt(),X,Y)
   U52#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U52#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z()))
   U52#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z())))
   U61#(tt(),A,B) -> U62#(tt(),A,B)
   U62#(tt(),A,B) -> prod#(B)
   U62#(tt(),A,B) -> prod#(A)
   U62#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B))
   U71#(tt(),A,B) -> U72#(tt(),A,B)
   U72#(tt(),A,B) -> sum#(B)
   U72#(tt(),A,B) -> sum#(A)
   U72#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B))
   mult{AC,#}(0(X),Y) -> U11#(tt(),X,Y)
   mult{AC,#}(1(X),Y) -> U21#(tt(),X,Y)
   plus{AC,#}(0(X),0(Y)) -> U31#(tt(),X,Y)
   plus{AC,#}(0(X),1(Y)) -> U41#(tt(),X,Y)
   plus{AC,#}(1(X),1(Y)) -> U51#(tt(),X,Y)
   prod#(unionAC(A,B)) -> U61#(tt(),A,B)
   sum#(empty()) -> 0#(z())
   sum#(unionAC(A,B)) -> U71#(tt(),A,B)
   union{AC,#}(x8,unionAC(X,empty())) -> union{AC,#}(x8,X)
   union{AC,#}(x9,unionAC(empty(),X)) -> union{AC,#}(x9,X)
   mult{AC,#}(x10,multAC(z(),X)) -> mult{AC,#}(x10,z())
   mult{AC,#}(x11,multAC(0(X),Y)) -> U11#(tt(),X,Y)
   mult{AC,#}(x11,multAC(0(X),Y)) -> mult{AC,#}(x11,U11(tt(),X,Y))
   mult{AC,#}(x12,multAC(1(X),Y)) -> U21#(tt(),X,Y)
   mult{AC,#}(x12,multAC(1(X),Y)) -> mult{AC,#}(x12,U21(tt(),X,Y))
   plus{AC,#}(x13,plusAC(z(),X)) -> plus{AC,#}(x13,X)
   plus{AC,#}(x14,plusAC(0(X),0(Y))) -> U31#(tt(),X,Y)
   plus{AC,#}(x14,plusAC(0(X),0(Y))) -> plus{AC,#}(x14,U31(tt(),X,Y))
   plus{AC,#}(x15,plusAC(0(X),1(Y))) -> U41#(tt(),X,Y)
   plus{AC,#}(x15,plusAC(0(X),1(Y))) -> plus{AC,#}(x15,U41(tt(),X,Y))
   plus{AC,#}(x16,plusAC(1(X),1(Y))) -> U51#(tt(),X,Y)
   plus{AC,#}(x16,plusAC(1(X),1(Y))) -> plus{AC,#}(x16,U51(tt(),X,Y))
  Equations:
   unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
   unionAC(x5,x6) -> unionAC(x6,x5)
   multAC(multAC(x5,x6),x7) -> multAC(x5,multAC(x6,x7))
   multAC(x5,x6) -> multAC(x6,x5)
   plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7))
   plusAC(x5,x6) -> plusAC(x6,x5)
   unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
   unionAC(x6,x5) -> unionAC(x5,x6)
   multAC(x5,multAC(x6,x7)) -> multAC(multAC(x5,x6),x7)
   multAC(x6,x5) -> multAC(x5,x6)
   plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7)
   plusAC(x6,x5) -> plusAC(x5,x6)
  TRS:
   unionAC(X,empty()) -> X
   unionAC(empty(),X) -> X
   0(z()) -> z()
   U11(tt(),X,Y) -> U12(tt(),X,Y)
   U12(tt(),X,Y) -> 0(multAC(X,Y))
   U21(tt(),X,Y) -> U22(tt(),X,Y)
   U22(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y)
   U31(tt(),X,Y) -> U32(tt(),X,Y)
   U32(tt(),X,Y) -> 0(plusAC(X,Y))
   U41(tt(),X,Y) -> U42(tt(),X,Y)
   U42(tt(),X,Y) -> 1(plusAC(X,Y))
   U51(tt(),X,Y) -> U52(tt(),X,Y)
   U52(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z())))
   U61(tt(),A,B) -> U62(tt(),A,B)
   U62(tt(),A,B) -> multAC(prod(A),prod(B))
   U71(tt(),A,B) -> U72(tt(),A,B)
   U72(tt(),A,B) -> plusAC(sum(A),sum(B))
   multAC(z(),X) -> z()
   multAC(0(X),Y) -> U11(tt(),X,Y)
   multAC(1(X),Y) -> U21(tt(),X,Y)
   plusAC(z(),X) -> X
   plusAC(0(X),0(Y)) -> U31(tt(),X,Y)
   plusAC(0(X),1(Y)) -> U41(tt(),X,Y)
   plusAC(1(X),1(Y)) -> U51(tt(),X,Y)
   prod(empty()) -> 1(z())
   prod(singl(X)) -> X
   prod(unionAC(A,B)) -> U61(tt(),A,B)
   sum(empty()) -> 0(z())
   sum(singl(X)) -> X
   sum(unionAC(A,B)) -> U71(tt(),A,B)
  S:
   union{AC,#}(unionAC(x17,x18),x19) -> union{AC,#}(x17,x18)
   union{AC,#}(x17,unionAC(x18,x19)) -> union{AC,#}(x18,x19)
   mult{AC,#}(multAC(x17,x18),x19) -> mult{AC,#}(x17,x18)
   mult{AC,#}(x17,multAC(x18,x19)) -> mult{AC,#}(x18,x19)
   plus{AC,#}(plusAC(x17,x18),x19) -> plus{AC,#}(x17,x18)
   plus{AC,#}(x17,plusAC(x18,x19)) -> plus{AC,#}(x18,x19)
  AC-EDG Processor:
   Equations#:
    union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7))
    union{AC,#}(x5,x6) -> union{AC,#}(x6,x5)
    mult{AC,#}(multAC(x5,x6),x7) -> mult{AC,#}(x5,multAC(x6,x7))
    mult{AC,#}(x5,x6) -> mult{AC,#}(x6,x5)
    plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7))
    plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5)
    union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7)
    union{AC,#}(x6,x5) -> union{AC,#}(x5,x6)
    mult{AC,#}(x5,multAC(x6,x7)) -> mult{AC,#}(multAC(x5,x6),x7)
    mult{AC,#}(x6,x5) -> mult{AC,#}(x5,x6)
    plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7)
    plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6)
   DPs:
    U11#(tt(),X,Y) -> U12#(tt(),X,Y)
    U12#(tt(),X,Y) -> mult{AC,#}(X,Y)
    U12#(tt(),X,Y) -> 0#(multAC(X,Y))
    U21#(tt(),X,Y) -> U22#(tt(),X,Y)
    U22#(tt(),X,Y) -> mult{AC,#}(X,Y)
    U22#(tt(),X,Y) -> 0#(multAC(X,Y))
    U22#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y)
    U31#(tt(),X,Y) -> U32#(tt(),X,Y)
    U32#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U32#(tt(),X,Y) -> 0#(plusAC(X,Y))
    U41#(tt(),X,Y) -> U42#(tt(),X,Y)
    U42#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U51#(tt(),X,Y) -> U52#(tt(),X,Y)
    U52#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U52#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z()))
    U52#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z())))
    U61#(tt(),A,B) -> U62#(tt(),A,B)
    U62#(tt(),A,B) -> prod#(B)
    U62#(tt(),A,B) -> prod#(A)
    U62#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B))
    U71#(tt(),A,B) -> U72#(tt(),A,B)
    U72#(tt(),A,B) -> sum#(B)
    U72#(tt(),A,B) -> sum#(A)
    U72#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B))
    mult{AC,#}(0(X),Y) -> U11#(tt(),X,Y)
    mult{AC,#}(1(X),Y) -> U21#(tt(),X,Y)
    plus{AC,#}(0(X),0(Y)) -> U31#(tt(),X,Y)
    plus{AC,#}(0(X),1(Y)) -> U41#(tt(),X,Y)
    plus{AC,#}(1(X),1(Y)) -> U51#(tt(),X,Y)
    prod#(unionAC(A,B)) -> U61#(tt(),A,B)
    sum#(empty()) -> 0#(z())
    sum#(unionAC(A,B)) -> U71#(tt(),A,B)
    union{AC,#}(x8,unionAC(X,empty())) -> union{AC,#}(x8,X)
    union{AC,#}(x9,unionAC(empty(),X)) -> union{AC,#}(x9,X)
    mult{AC,#}(x10,multAC(z(),X)) -> mult{AC,#}(x10,z())
    mult{AC,#}(x11,multAC(0(X),Y)) -> U11#(tt(),X,Y)
    mult{AC,#}(x11,multAC(0(X),Y)) -> mult{AC,#}(x11,U11(tt(),X,Y))
    mult{AC,#}(x12,multAC(1(X),Y)) -> U21#(tt(),X,Y)
    mult{AC,#}(x12,multAC(1(X),Y)) -> mult{AC,#}(x12,U21(tt(),X,Y))
    plus{AC,#}(x13,plusAC(z(),X)) -> plus{AC,#}(x13,X)
    plus{AC,#}(x14,plusAC(0(X),0(Y))) -> U31#(tt(),X,Y)
    plus{AC,#}(x14,plusAC(0(X),0(Y))) -> plus{AC,#}(x14,U31(tt(),X,Y))
    plus{AC,#}(x15,plusAC(0(X),1(Y))) -> U41#(tt(),X,Y)
    plus{AC,#}(x15,plusAC(0(X),1(Y))) -> plus{AC,#}(x15,U41(tt(),X,Y))
    plus{AC,#}(x16,plusAC(1(X),1(Y))) -> U51#(tt(),X,Y)
    plus{AC,#}(x16,plusAC(1(X),1(Y))) -> plus{AC,#}(x16,U51(tt(),X,Y))
   Equations:
    unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
    unionAC(x5,x6) -> unionAC(x6,x5)
    multAC(multAC(x5,x6),x7) -> multAC(x5,multAC(x6,x7))
    multAC(x5,x6) -> multAC(x6,x5)
    plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7))
    plusAC(x5,x6) -> plusAC(x6,x5)
    unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
    unionAC(x6,x5) -> unionAC(x5,x6)
    multAC(x5,multAC(x6,x7)) -> multAC(multAC(x5,x6),x7)
    multAC(x6,x5) -> multAC(x5,x6)
    plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7)
    plusAC(x6,x5) -> plusAC(x5,x6)
   TRS:
    unionAC(X,empty()) -> X
    unionAC(empty(),X) -> X
    0(z()) -> z()
    U11(tt(),X,Y) -> U12(tt(),X,Y)
    U12(tt(),X,Y) -> 0(multAC(X,Y))
    U21(tt(),X,Y) -> U22(tt(),X,Y)
    U22(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y)
    U31(tt(),X,Y) -> U32(tt(),X,Y)
    U32(tt(),X,Y) -> 0(plusAC(X,Y))
    U41(tt(),X,Y) -> U42(tt(),X,Y)
    U42(tt(),X,Y) -> 1(plusAC(X,Y))
    U51(tt(),X,Y) -> U52(tt(),X,Y)
    U52(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z())))
    U61(tt(),A,B) -> U62(tt(),A,B)
    U62(tt(),A,B) -> multAC(prod(A),prod(B))
    U71(tt(),A,B) -> U72(tt(),A,B)
    U72(tt(),A,B) -> plusAC(sum(A),sum(B))
    multAC(z(),X) -> z()
    multAC(0(X),Y) -> U11(tt(),X,Y)
    multAC(1(X),Y) -> U21(tt(),X,Y)
    plusAC(z(),X) -> X
    plusAC(0(X),0(Y)) -> U31(tt(),X,Y)
    plusAC(0(X),1(Y)) -> U41(tt(),X,Y)
    plusAC(1(X),1(Y)) -> U51(tt(),X,Y)
    prod(empty()) -> 1(z())
    prod(singl(X)) -> X
    prod(unionAC(A,B)) -> U61(tt(),A,B)
    sum(empty()) -> 0(z())
    sum(singl(X)) -> X
    sum(unionAC(A,B)) -> U71(tt(),A,B)
   S:
    union{AC,#}(unionAC(x17,x18),x19) -> union{AC,#}(x17,x18)
    union{AC,#}(x17,unionAC(x18,x19)) -> union{AC,#}(x18,x19)
    mult{AC,#}(multAC(x17,x18),x19) -> mult{AC,#}(x17,x18)
    mult{AC,#}(x17,multAC(x18,x19)) -> mult{AC,#}(x18,x19)
    plus{AC,#}(plusAC(x17,x18),x19) -> plus{AC,#}(x17,x18)
    plus{AC,#}(x17,plusAC(x18,x19)) -> plus{AC,#}(x18,x19)
   Open