MAYBE
Time: 0.026

Problem:
 Equations:
  
 TRS:
  unionAC(X,empty()) -> X
  unionAC(empty(),X) -> X
  0(z()) -> z()
  U101(tt(),X,Y) -> U102(isBin(Y),X,Y)
  U102(tt(),X,Y) -> 0(multAC(X,Y))
  U11(tt()) -> tt()
  U111(tt(),X,Y) -> U112(isBin(Y),X,Y)
  U112(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y)
  U121(tt(),X) -> X
  U131(tt(),X,Y) -> U132(isBin(Y),X,Y)
  U132(tt(),X,Y) -> 0(plusAC(X,Y))
  U141(tt(),X,Y) -> U142(isBin(Y),X,Y)
  U142(tt(),X,Y) -> 1(plusAC(X,Y))
  U151(tt(),X,Y) -> U152(isBin(Y),X,Y)
  U152(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z())))
  U161(tt(),X) -> X
  U171(tt(),A,B) -> U172(isBag(B),A,B)
  U172(tt(),A,B) -> multAC(prod(A),prod(B))
  U181(tt(),X) -> X
  U191(tt(),A,B) -> U192(isBag(B),A,B)
  U192(tt(),A,B) -> plusAC(sum(A),sum(B))
  U21(tt(),V2) -> U22(isBag(V2))
  U22(tt()) -> tt()
  U31(tt()) -> tt()
  U41(tt()) -> tt()
  U51(tt(),V2) -> U52(isBin(V2))
  U52(tt()) -> tt()
  U61(tt(),V2) -> U62(isBin(V2))
  U62(tt()) -> tt()
  U71(tt()) -> tt()
  U81(tt()) -> tt()
  U91(tt()) -> z()
  isBag(empty()) -> tt()
  isBag(singl(V1)) -> U11(isBin(V1))
  isBag(unionAC(V1,V2)) -> U21(isBag(V1),V2)
  isBin(z()) -> tt()
  isBin(0(V1)) -> U31(isBin(V1))
  isBin(1(V1)) -> U41(isBin(V1))
  isBin(multAC(V1,V2)) -> U51(isBin(V1),V2)
  isBin(plusAC(V1,V2)) -> U61(isBin(V1),V2)
  isBin(prod(V1)) -> U71(isBag(V1))
  isBin(sum(V1)) -> U81(isBag(V1))
  multAC(z(),X) -> U91(isBin(X))
  multAC(0(X),Y) -> U101(isBin(X),X,Y)
  multAC(1(X),Y) -> U111(isBin(X),X,Y)
  plusAC(z(),X) -> U121(isBin(X),X)
  plusAC(0(X),0(Y)) -> U131(isBin(X),X,Y)
  plusAC(0(X),1(Y)) -> U141(isBin(X),X,Y)
  plusAC(1(X),1(Y)) -> U151(isBin(X),X,Y)
  prod(empty()) -> 1(z())
  prod(singl(X)) -> U161(isBin(X),X)
  prod(unionAC(A,B)) -> U171(isBag(A),A,B)
  sum(empty()) -> 0(z())
  sum(singl(X)) -> U181(isBin(X),X)
  sum(unionAC(A,B)) -> U191(isBag(A),A,B)

Proof:
 Open