MAYBE
Time: 4.372

Problem:
 Equations:
  
 TRS:
  unionAC(X,empty()) -> X
  unionAC(empty(),X) -> X
  0(z()) -> z()
  U101(tt(),X,Y) -> 0(multAC(X,Y))
  U11(tt(),V1) -> U12(isBin(V1))
  U111(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y)
  U12(tt()) -> tt()
  U121(tt(),X) -> X
  U131(tt(),X,Y) -> 0(plusAC(X,Y))
  U141(tt(),X,Y) -> 1(plusAC(X,Y))
  U151(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z())))
  U161(tt(),X) -> X
  U171(tt(),A,B) -> multAC(prod(A),prod(B))
  U181(tt(),X) -> X
  U191(tt(),A,B) -> plusAC(sum(A),sum(B))
  U21(tt(),V1,V2) -> U22(isBag(V1),V2)
  U22(tt(),V2) -> U23(isBag(V2))
  U23(tt()) -> tt()
  U31(tt(),V1) -> U32(isBin(V1))
  U32(tt()) -> tt()
  U41(tt(),V1) -> U42(isBin(V1))
  U42(tt()) -> tt()
  U51(tt(),V1,V2) -> U52(isBin(V1),V2)
  U52(tt(),V2) -> U53(isBin(V2))
  U53(tt()) -> tt()
  U61(tt(),V1,V2) -> U62(isBin(V1),V2)
  U62(tt(),V2) -> U63(isBin(V2))
  U63(tt()) -> tt()
  U71(tt(),V1) -> U72(isBag(V1))
  U72(tt()) -> tt()
  U81(tt(),V1) -> U82(isBag(V1))
  U82(tt()) -> tt()
  U91(tt()) -> z()
  and(tt(),X) -> X
  isBag(empty()) -> tt()
  isBag(singl(V1)) -> U11(isBinKind(V1),V1)
  isBag(unionAC(V1,V2)) -> U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)
  isBagKind(empty()) -> tt()
  isBagKind(singl(V1)) -> isBinKind(V1)
  isBagKind(unionAC(V1,V2)) -> and(isBagKind(V1),isBagKind(V2))
  isBin(z()) -> tt()
  isBin(0(V1)) -> U31(isBinKind(V1),V1)
  isBin(1(V1)) -> U41(isBinKind(V1),V1)
  isBin(multAC(V1,V2)) -> U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)
  isBin(plusAC(V1,V2)) -> U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)
  isBin(prod(V1)) -> U71(isBagKind(V1),V1)
  isBin(sum(V1)) -> U81(isBagKind(V1),V1)
  isBinKind(z()) -> tt()
  isBinKind(0(V1)) -> isBinKind(V1)
  isBinKind(1(V1)) -> isBinKind(V1)
  isBinKind(multAC(V1,V2)) -> and(isBinKind(V1),isBinKind(V2))
  isBinKind(plusAC(V1,V2)) -> and(isBinKind(V1),isBinKind(V2))
  isBinKind(prod(V1)) -> isBagKind(V1)
  isBinKind(sum(V1)) -> isBagKind(V1)
  multAC(z(),X) -> U91(and(isBin(X),isBinKind(X)))
  multAC(0(X),Y) -> U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
  multAC(1(X),Y) -> U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
  plusAC(z(),X) -> U121(and(isBin(X),isBinKind(X)),X)
  plusAC(0(X),0(Y)) -> U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
  plusAC(0(X),1(Y)) -> U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
  plusAC(1(X),1(Y)) -> U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
  prod(empty()) -> 1(z())
  prod(singl(X)) -> U161(and(isBin(X),isBinKind(X)),X)
  prod(unionAC(A,B)) -> U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)
  sum(empty()) -> 0(z())
  sum(singl(X)) -> U181(and(isBin(X),isBinKind(X)),X)
  sum(unionAC(A,B)) -> U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)

Proof:
 Open