MAYBE
Time: 0.016

Problem:
 Equations:
  
 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