MAYBE
Time: 0.019

Problem:
 Equations:
  
 TRS:
  unionAC(X,empty()) -> X
  unionAC(empty(),X) -> X
  0(z()) -> z()
  U101(tt(),X) -> X
  U11(tt()) -> z()
  U111(tt(),A,B) -> plusAC(sum(A),sum(B))
  U21(tt(),X,Y) -> 0(multAC(X,Y))
  U31(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y)
  U41(tt(),X) -> X
  U51(tt(),X,Y) -> 0(plusAC(X,Y))
  U61(tt(),X,Y) -> 1(plusAC(X,Y))
  U71(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z())))
  U81(tt(),X) -> X
  U91(tt(),A,B) -> multAC(prod(A),prod(B))
  and(tt(),X) -> X
  isBag(empty()) -> tt()
  isBag(singl(V1)) -> isBin(V1)
  isBag(unionAC(V1,V2)) -> and(isBag(V1),isBag(V2))
  isBin(z()) -> tt()
  isBin(0(V1)) -> isBin(V1)
  isBin(1(V1)) -> isBin(V1)
  isBin(multAC(V1,V2)) -> and(isBin(V1),isBin(V2))
  isBin(plusAC(V1,V2)) -> and(isBin(V1),isBin(V2))
  isBin(prod(V1)) -> isBag(V1)
  isBin(sum(V1)) -> isBag(V1)
  multAC(z(),X) -> U11(isBin(X))
  multAC(0(X),Y) -> U21(and(isBin(X),isBin(Y)),X,Y)
  multAC(1(X),Y) -> U31(and(isBin(X),isBin(Y)),X,Y)
  plusAC(z(),X) -> U41(isBin(X),X)
  plusAC(0(X),0(Y)) -> U51(and(isBin(X),isBin(Y)),X,Y)
  plusAC(0(X),1(Y)) -> U61(and(isBin(X),isBin(Y)),X,Y)
  plusAC(1(X),1(Y)) -> U71(and(isBin(X),isBin(Y)),X,Y)
  prod(empty()) -> 1(z())
  prod(singl(X)) -> U81(isBin(X),X)
  prod(unionAC(A,B)) -> U91(and(isBag(A),isBag(B)),A,B)
  sum(empty()) -> 0(z())
  sum(singl(X)) -> U101(isBin(X),X)
  sum(unionAC(A,B)) -> U111(and(isBag(A),isBag(B)),A,B)

Proof:
 Open