MAYBE
Time: 0.021

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:
 Open