MAYBE
Time: 34.231

Problem:
 Equations:
  unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9))
  unionAC(x7,x8) -> unionAC(x8,x7)
  multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9))
  multAC(x7,x8) -> multAC(x8,x7)
  plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9))
  plusAC(x7,x8) -> plusAC(x8,x7)
  unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9)
  unionAC(x8,x7) -> unionAC(x7,x8)
  multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9)
  multAC(x8,x7) -> multAC(x7,x8)
  plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9)
  plusAC(x8,x7) -> plusAC(x7,x8)
 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:
 DP Processor:
  Equations#:
   union{AC,#}(unionAC(x7,x8),x9) -> union{AC,#}(x7,unionAC(x8,x9))
   union{AC,#}(x7,x8) -> union{AC,#}(x8,x7)
   mult{AC,#}(multAC(x7,x8),x9) -> mult{AC,#}(x7,multAC(x8,x9))
   mult{AC,#}(x7,x8) -> mult{AC,#}(x8,x7)
   plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,plusAC(x8,x9))
   plus{AC,#}(x7,x8) -> plus{AC,#}(x8,x7)
   union{AC,#}(x7,unionAC(x8,x9)) -> union{AC,#}(unionAC(x7,x8),x9)
   union{AC,#}(x8,x7) -> union{AC,#}(x7,x8)
   mult{AC,#}(x7,multAC(x8,x9)) -> mult{AC,#}(multAC(x7,x8),x9)
   mult{AC,#}(x8,x7) -> mult{AC,#}(x7,x8)
   plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(plusAC(x7,x8),x9)
   plus{AC,#}(x8,x7) -> plus{AC,#}(x7,x8)
  DPs:
   U101#(tt(),X,Y) -> mult{AC,#}(X,Y)
   U101#(tt(),X,Y) -> 0#(multAC(X,Y))
   U11#(tt(),V1) -> isBin#(V1)
   U11#(tt(),V1) -> U12#(isBin(V1))
   U111#(tt(),X,Y) -> mult{AC,#}(X,Y)
   U111#(tt(),X,Y) -> 0#(multAC(X,Y))
   U111#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y)
   U131#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U131#(tt(),X,Y) -> 0#(plusAC(X,Y))
   U141#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U151#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U151#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z()))
   U151#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z())))
   U171#(tt(),A,B) -> prod#(B)
   U171#(tt(),A,B) -> prod#(A)
   U171#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B))
   U191#(tt(),A,B) -> sum#(B)
   U191#(tt(),A,B) -> sum#(A)
   U191#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B))
   U21#(tt(),V1,V2) -> isBag#(V1)
   U21#(tt(),V1,V2) -> U22#(isBag(V1),V2)
   U22#(tt(),V2) -> isBag#(V2)
   U22#(tt(),V2) -> U23#(isBag(V2))
   U31#(tt(),V1) -> isBin#(V1)
   U31#(tt(),V1) -> U32#(isBin(V1))
   U41#(tt(),V1) -> isBin#(V1)
   U41#(tt(),V1) -> U42#(isBin(V1))
   U51#(tt(),V1,V2) -> isBin#(V1)
   U51#(tt(),V1,V2) -> U52#(isBin(V1),V2)
   U52#(tt(),V2) -> isBin#(V2)
   U52#(tt(),V2) -> U53#(isBin(V2))
   U61#(tt(),V1,V2) -> isBin#(V1)
   U61#(tt(),V1,V2) -> U62#(isBin(V1),V2)
   U62#(tt(),V2) -> isBin#(V2)
   U62#(tt(),V2) -> U63#(isBin(V2))
   U71#(tt(),V1) -> isBag#(V1)
   U71#(tt(),V1) -> U72#(isBag(V1))
   U81#(tt(),V1) -> isBag#(V1)
   U81#(tt(),V1) -> U82#(isBag(V1))
   isBag#(singl(V1)) -> isBinKind#(V1)
   isBag#(singl(V1)) -> U11#(isBinKind(V1),V1)
   isBag#(unionAC(V1,V2)) -> isBagKind#(V2)
   isBag#(unionAC(V1,V2)) -> isBagKind#(V1)
   isBag#(unionAC(V1,V2)) -> and#(isBagKind(V1),isBagKind(V2))
   isBag#(unionAC(V1,V2)) -> U21#(and(isBagKind(V1),isBagKind(V2)),V1,V2)
   isBagKind#(singl(V1)) -> isBinKind#(V1)
   isBagKind#(unionAC(V1,V2)) -> isBagKind#(V2)
   isBagKind#(unionAC(V1,V2)) -> isBagKind#(V1)
   isBagKind#(unionAC(V1,V2)) -> and#(isBagKind(V1),isBagKind(V2))
   isBin#(0(V1)) -> isBinKind#(V1)
   isBin#(0(V1)) -> U31#(isBinKind(V1),V1)
   isBin#(1(V1)) -> isBinKind#(V1)
   isBin#(1(V1)) -> U41#(isBinKind(V1),V1)
   isBin#(multAC(V1,V2)) -> isBinKind#(V2)
   isBin#(multAC(V1,V2)) -> isBinKind#(V1)
   isBin#(multAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2))
   isBin#(multAC(V1,V2)) -> U51#(and(isBinKind(V1),isBinKind(V2)),V1,V2)
   isBin#(plusAC(V1,V2)) -> isBinKind#(V2)
   isBin#(plusAC(V1,V2)) -> isBinKind#(V1)
   isBin#(plusAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2))
   isBin#(plusAC(V1,V2)) -> U61#(and(isBinKind(V1),isBinKind(V2)),V1,V2)
   isBin#(prod(V1)) -> isBagKind#(V1)
   isBin#(prod(V1)) -> U71#(isBagKind(V1),V1)
   isBin#(sum(V1)) -> isBagKind#(V1)
   isBin#(sum(V1)) -> U81#(isBagKind(V1),V1)
   isBinKind#(0(V1)) -> isBinKind#(V1)
   isBinKind#(1(V1)) -> isBinKind#(V1)
   isBinKind#(multAC(V1,V2)) -> isBinKind#(V2)
   isBinKind#(multAC(V1,V2)) -> isBinKind#(V1)
   isBinKind#(multAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2))
   isBinKind#(plusAC(V1,V2)) -> isBinKind#(V2)
   isBinKind#(plusAC(V1,V2)) -> isBinKind#(V1)
   isBinKind#(plusAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2))
   isBinKind#(prod(V1)) -> isBagKind#(V1)
   isBinKind#(sum(V1)) -> isBagKind#(V1)
   mult{AC,#}(z(),X) -> isBinKind#(X)
   mult{AC,#}(z(),X) -> isBin#(X)
   mult{AC,#}(z(),X) -> and#(isBin(X),isBinKind(X))
   mult{AC,#}(z(),X) -> U91#(and(isBin(X),isBinKind(X)))
   mult{AC,#}(0(X),Y) -> isBinKind#(Y)
   mult{AC,#}(0(X),Y) -> isBin#(Y)
   mult{AC,#}(0(X),Y) -> and#(isBin(Y),isBinKind(Y))
   mult{AC,#}(0(X),Y) -> isBinKind#(X)
   mult{AC,#}(0(X),Y) -> isBin#(X)
   mult{AC,#}(0(X),Y) -> and#(isBin(X),isBinKind(X))
   mult{AC,#}(0(X),Y) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   mult{AC,#}(0(X),Y) -> U101#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   mult{AC,#}(1(X),Y) -> isBinKind#(Y)
   mult{AC,#}(1(X),Y) -> isBin#(Y)
   mult{AC,#}(1(X),Y) -> and#(isBin(Y),isBinKind(Y))
   mult{AC,#}(1(X),Y) -> isBinKind#(X)
   mult{AC,#}(1(X),Y) -> isBin#(X)
   mult{AC,#}(1(X),Y) -> and#(isBin(X),isBinKind(X))
   mult{AC,#}(1(X),Y) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   mult{AC,#}(1(X),Y) -> U111#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   plus{AC,#}(z(),X) -> isBinKind#(X)
   plus{AC,#}(z(),X) -> isBin#(X)
   plus{AC,#}(z(),X) -> and#(isBin(X),isBinKind(X))
   plus{AC,#}(z(),X) -> U121#(and(isBin(X),isBinKind(X)),X)
   plus{AC,#}(0(X),0(Y)) -> isBinKind#(Y)
   plus{AC,#}(0(X),0(Y)) -> isBin#(Y)
   plus{AC,#}(0(X),0(Y)) -> and#(isBin(Y),isBinKind(Y))
   plus{AC,#}(0(X),0(Y)) -> isBinKind#(X)
   plus{AC,#}(0(X),0(Y)) -> isBin#(X)
   plus{AC,#}(0(X),0(Y)) -> and#(isBin(X),isBinKind(X))
   plus{AC,#}(0(X),0(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   plus{AC,#}(0(X),0(Y)) -> U131#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   plus{AC,#}(0(X),1(Y)) -> isBinKind#(Y)
   plus{AC,#}(0(X),1(Y)) -> isBin#(Y)
   plus{AC,#}(0(X),1(Y)) -> and#(isBin(Y),isBinKind(Y))
   plus{AC,#}(0(X),1(Y)) -> isBinKind#(X)
   plus{AC,#}(0(X),1(Y)) -> isBin#(X)
   plus{AC,#}(0(X),1(Y)) -> and#(isBin(X),isBinKind(X))
   plus{AC,#}(0(X),1(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   plus{AC,#}(0(X),1(Y)) -> U141#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   plus{AC,#}(1(X),1(Y)) -> isBinKind#(Y)
   plus{AC,#}(1(X),1(Y)) -> isBin#(Y)
   plus{AC,#}(1(X),1(Y)) -> and#(isBin(Y),isBinKind(Y))
   plus{AC,#}(1(X),1(Y)) -> isBinKind#(X)
   plus{AC,#}(1(X),1(Y)) -> isBin#(X)
   plus{AC,#}(1(X),1(Y)) -> and#(isBin(X),isBinKind(X))
   plus{AC,#}(1(X),1(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   plus{AC,#}(1(X),1(Y)) -> U151#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   prod#(singl(X)) -> isBinKind#(X)
   prod#(singl(X)) -> isBin#(X)
   prod#(singl(X)) -> and#(isBin(X),isBinKind(X))
   prod#(singl(X)) -> U161#(and(isBin(X),isBinKind(X)),X)
   prod#(unionAC(A,B)) -> isBagKind#(B)
   prod#(unionAC(A,B)) -> isBag#(B)
   prod#(unionAC(A,B)) -> and#(isBag(B),isBagKind(B))
   prod#(unionAC(A,B)) -> isBagKind#(A)
   prod#(unionAC(A,B)) -> isBag#(A)
   prod#(unionAC(A,B)) -> and#(isBag(A),isBagKind(A))
   prod#(unionAC(A,B)) -> and#(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B)))
   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)) -> isBinKind#(X)
   sum#(singl(X)) -> isBin#(X)
   sum#(singl(X)) -> and#(isBin(X),isBinKind(X))
   sum#(singl(X)) -> U181#(and(isBin(X),isBinKind(X)),X)
   sum#(unionAC(A,B)) -> isBagKind#(B)
   sum#(unionAC(A,B)) -> isBag#(B)
   sum#(unionAC(A,B)) -> and#(isBag(B),isBagKind(B))
   sum#(unionAC(A,B)) -> isBagKind#(A)
   sum#(unionAC(A,B)) -> isBag#(A)
   sum#(unionAC(A,B)) -> and#(isBag(A),isBagKind(A))
   sum#(unionAC(A,B)) -> and#(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B)))
   sum#(unionAC(A,B)) -> U191#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)
   union{AC,#}(x10,unionAC(X,empty())) -> union{AC,#}(x10,X)
   union{AC,#}(x11,unionAC(empty(),X)) -> union{AC,#}(x11,X)
   mult{AC,#}(x12,multAC(z(),X)) -> isBinKind#(X)
   mult{AC,#}(x12,multAC(z(),X)) -> isBin#(X)
   mult{AC,#}(x12,multAC(z(),X)) -> and#(isBin(X),isBinKind(X))
   mult{AC,#}(x12,multAC(z(),X)) -> U91#(and(isBin(X),isBinKind(X)))
   mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U91(and(isBin(X),isBinKind(X))))
   mult{AC,#}(x13,multAC(0(X),Y)) -> isBinKind#(Y)
   mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(Y)
   mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(Y),isBinKind(Y))
   mult{AC,#}(x13,multAC(0(X),Y)) -> isBinKind#(X)
   mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X)
   mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(X),isBinKind(X))
   mult{AC,#}(x13,multAC(0(X),Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   mult{AC,#}(x13,multAC(0(X),Y)) ->
   U101#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   mult{AC,#}(x13,multAC(0(X),Y)) ->
   mult{AC,#}(x13,U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
   mult{AC,#}(x14,multAC(1(X),Y)) -> isBinKind#(Y)
   mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(Y)
   mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(Y),isBinKind(Y))
   mult{AC,#}(x14,multAC(1(X),Y)) -> isBinKind#(X)
   mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X)
   mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(X),isBinKind(X))
   mult{AC,#}(x14,multAC(1(X),Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   mult{AC,#}(x14,multAC(1(X),Y)) ->
   U111#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   mult{AC,#}(x14,multAC(1(X),Y)) ->
   mult{AC,#}(x14,U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
   plus{AC,#}(x15,plusAC(z(),X)) -> isBinKind#(X)
   plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X)
   plus{AC,#}(x15,plusAC(z(),X)) -> and#(isBin(X),isBinKind(X))
   plus{AC,#}(x15,plusAC(z(),X)) -> U121#(and(isBin(X),isBinKind(X)),X)
   plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U121(and(isBin(X),isBinKind(X)),X))
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBinKind#(Y)
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(Y)
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(Y),isBinKind(Y))
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBinKind#(X)
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X)
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(X),isBinKind(X))
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   plus{AC,#}(x16,plusAC(0(X),0(Y))) ->
   U131#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   plus{AC,#}(x16,plusAC(0(X),0(Y))) ->
   plus{AC,#}(x16,U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBinKind#(Y)
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(Y)
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(Y),isBinKind(Y))
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBinKind#(X)
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X)
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(X),isBinKind(X))
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   plus{AC,#}(x17,plusAC(0(X),1(Y))) ->
   U141#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   plus{AC,#}(x17,plusAC(0(X),1(Y))) ->
   plus{AC,#}(x17,U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBinKind#(Y)
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(Y)
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(Y),isBinKind(Y))
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBinKind#(X)
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X)
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(X),isBinKind(X))
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
   plus{AC,#}(x18,plusAC(1(X),1(Y))) ->
   U151#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
   plus{AC,#}(x18,plusAC(1(X),1(Y))) ->
   plus{AC,#}(x18,U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
  Equations:
   unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9))
   unionAC(x7,x8) -> unionAC(x8,x7)
   multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9))
   multAC(x7,x8) -> multAC(x8,x7)
   plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9))
   plusAC(x7,x8) -> plusAC(x8,x7)
   unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9)
   unionAC(x8,x7) -> unionAC(x7,x8)
   multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9)
   multAC(x8,x7) -> multAC(x7,x8)
   plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9)
   plusAC(x8,x7) -> plusAC(x7,x8)
  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)
  S:
   union{AC,#}(unionAC(x19,x20),x21) -> union{AC,#}(x19,x20)
   union{AC,#}(x19,unionAC(x20,x21)) -> union{AC,#}(x20,x21)
   mult{AC,#}(multAC(x19,x20),x21) -> mult{AC,#}(x19,x20)
   mult{AC,#}(x19,multAC(x20,x21)) -> mult{AC,#}(x20,x21)
   plus{AC,#}(plusAC(x19,x20),x21) -> plus{AC,#}(x19,x20)
   plus{AC,#}(x19,plusAC(x20,x21)) -> plus{AC,#}(x20,x21)
  AC-EDG Processor:
   Equations#:
    union{AC,#}(unionAC(x7,x8),x9) -> union{AC,#}(x7,unionAC(x8,x9))
    union{AC,#}(x7,x8) -> union{AC,#}(x8,x7)
    mult{AC,#}(multAC(x7,x8),x9) -> mult{AC,#}(x7,multAC(x8,x9))
    mult{AC,#}(x7,x8) -> mult{AC,#}(x8,x7)
    plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,plusAC(x8,x9))
    plus{AC,#}(x7,x8) -> plus{AC,#}(x8,x7)
    union{AC,#}(x7,unionAC(x8,x9)) -> union{AC,#}(unionAC(x7,x8),x9)
    union{AC,#}(x8,x7) -> union{AC,#}(x7,x8)
    mult{AC,#}(x7,multAC(x8,x9)) -> mult{AC,#}(multAC(x7,x8),x9)
    mult{AC,#}(x8,x7) -> mult{AC,#}(x7,x8)
    plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(plusAC(x7,x8),x9)
    plus{AC,#}(x8,x7) -> plus{AC,#}(x7,x8)
   DPs:
    U101#(tt(),X,Y) -> mult{AC,#}(X,Y)
    U101#(tt(),X,Y) -> 0#(multAC(X,Y))
    U11#(tt(),V1) -> isBin#(V1)
    U11#(tt(),V1) -> U12#(isBin(V1))
    U111#(tt(),X,Y) -> mult{AC,#}(X,Y)
    U111#(tt(),X,Y) -> 0#(multAC(X,Y))
    U111#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y)
    U131#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U131#(tt(),X,Y) -> 0#(plusAC(X,Y))
    U141#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U151#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U151#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z()))
    U151#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z())))
    U171#(tt(),A,B) -> prod#(B)
    U171#(tt(),A,B) -> prod#(A)
    U171#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B))
    U191#(tt(),A,B) -> sum#(B)
    U191#(tt(),A,B) -> sum#(A)
    U191#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B))
    U21#(tt(),V1,V2) -> isBag#(V1)
    U21#(tt(),V1,V2) -> U22#(isBag(V1),V2)
    U22#(tt(),V2) -> isBag#(V2)
    U22#(tt(),V2) -> U23#(isBag(V2))
    U31#(tt(),V1) -> isBin#(V1)
    U31#(tt(),V1) -> U32#(isBin(V1))
    U41#(tt(),V1) -> isBin#(V1)
    U41#(tt(),V1) -> U42#(isBin(V1))
    U51#(tt(),V1,V2) -> isBin#(V1)
    U51#(tt(),V1,V2) -> U52#(isBin(V1),V2)
    U52#(tt(),V2) -> isBin#(V2)
    U52#(tt(),V2) -> U53#(isBin(V2))
    U61#(tt(),V1,V2) -> isBin#(V1)
    U61#(tt(),V1,V2) -> U62#(isBin(V1),V2)
    U62#(tt(),V2) -> isBin#(V2)
    U62#(tt(),V2) -> U63#(isBin(V2))
    U71#(tt(),V1) -> isBag#(V1)
    U71#(tt(),V1) -> U72#(isBag(V1))
    U81#(tt(),V1) -> isBag#(V1)
    U81#(tt(),V1) -> U82#(isBag(V1))
    isBag#(singl(V1)) -> isBinKind#(V1)
    isBag#(singl(V1)) -> U11#(isBinKind(V1),V1)
    isBag#(unionAC(V1,V2)) -> isBagKind#(V2)
    isBag#(unionAC(V1,V2)) -> isBagKind#(V1)
    isBag#(unionAC(V1,V2)) -> and#(isBagKind(V1),isBagKind(V2))
    isBag#(unionAC(V1,V2)) -> U21#(and(isBagKind(V1),isBagKind(V2)),V1,V2)
    isBagKind#(singl(V1)) -> isBinKind#(V1)
    isBagKind#(unionAC(V1,V2)) -> isBagKind#(V2)
    isBagKind#(unionAC(V1,V2)) -> isBagKind#(V1)
    isBagKind#(unionAC(V1,V2)) -> and#(isBagKind(V1),isBagKind(V2))
    isBin#(0(V1)) -> isBinKind#(V1)
    isBin#(0(V1)) -> U31#(isBinKind(V1),V1)
    isBin#(1(V1)) -> isBinKind#(V1)
    isBin#(1(V1)) -> U41#(isBinKind(V1),V1)
    isBin#(multAC(V1,V2)) -> isBinKind#(V2)
    isBin#(multAC(V1,V2)) -> isBinKind#(V1)
    isBin#(multAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2))
    isBin#(multAC(V1,V2)) -> U51#(and(isBinKind(V1),isBinKind(V2)),V1,V2)
    isBin#(plusAC(V1,V2)) -> isBinKind#(V2)
    isBin#(plusAC(V1,V2)) -> isBinKind#(V1)
    isBin#(plusAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2))
    isBin#(plusAC(V1,V2)) -> U61#(and(isBinKind(V1),isBinKind(V2)),V1,V2)
    isBin#(prod(V1)) -> isBagKind#(V1)
    isBin#(prod(V1)) -> U71#(isBagKind(V1),V1)
    isBin#(sum(V1)) -> isBagKind#(V1)
    isBin#(sum(V1)) -> U81#(isBagKind(V1),V1)
    isBinKind#(0(V1)) -> isBinKind#(V1)
    isBinKind#(1(V1)) -> isBinKind#(V1)
    isBinKind#(multAC(V1,V2)) -> isBinKind#(V2)
    isBinKind#(multAC(V1,V2)) -> isBinKind#(V1)
    isBinKind#(multAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2))
    isBinKind#(plusAC(V1,V2)) -> isBinKind#(V2)
    isBinKind#(plusAC(V1,V2)) -> isBinKind#(V1)
    isBinKind#(plusAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2))
    isBinKind#(prod(V1)) -> isBagKind#(V1)
    isBinKind#(sum(V1)) -> isBagKind#(V1)
    mult{AC,#}(z(),X) -> isBinKind#(X)
    mult{AC,#}(z(),X) -> isBin#(X)
    mult{AC,#}(z(),X) -> and#(isBin(X),isBinKind(X))
    mult{AC,#}(z(),X) -> U91#(and(isBin(X),isBinKind(X)))
    mult{AC,#}(0(X),Y) -> isBinKind#(Y)
    mult{AC,#}(0(X),Y) -> isBin#(Y)
    mult{AC,#}(0(X),Y) -> and#(isBin(Y),isBinKind(Y))
    mult{AC,#}(0(X),Y) -> isBinKind#(X)
    mult{AC,#}(0(X),Y) -> isBin#(X)
    mult{AC,#}(0(X),Y) -> and#(isBin(X),isBinKind(X))
    mult{AC,#}(0(X),Y) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    mult{AC,#}(0(X),Y) -> U101#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    mult{AC,#}(1(X),Y) -> isBinKind#(Y)
    mult{AC,#}(1(X),Y) -> isBin#(Y)
    mult{AC,#}(1(X),Y) -> and#(isBin(Y),isBinKind(Y))
    mult{AC,#}(1(X),Y) -> isBinKind#(X)
    mult{AC,#}(1(X),Y) -> isBin#(X)
    mult{AC,#}(1(X),Y) -> and#(isBin(X),isBinKind(X))
    mult{AC,#}(1(X),Y) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    mult{AC,#}(1(X),Y) -> U111#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    plus{AC,#}(z(),X) -> isBinKind#(X)
    plus{AC,#}(z(),X) -> isBin#(X)
    plus{AC,#}(z(),X) -> and#(isBin(X),isBinKind(X))
    plus{AC,#}(z(),X) -> U121#(and(isBin(X),isBinKind(X)),X)
    plus{AC,#}(0(X),0(Y)) -> isBinKind#(Y)
    plus{AC,#}(0(X),0(Y)) -> isBin#(Y)
    plus{AC,#}(0(X),0(Y)) -> and#(isBin(Y),isBinKind(Y))
    plus{AC,#}(0(X),0(Y)) -> isBinKind#(X)
    plus{AC,#}(0(X),0(Y)) -> isBin#(X)
    plus{AC,#}(0(X),0(Y)) -> and#(isBin(X),isBinKind(X))
    plus{AC,#}(0(X),0(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    plus{AC,#}(0(X),0(Y)) -> U131#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    plus{AC,#}(0(X),1(Y)) -> isBinKind#(Y)
    plus{AC,#}(0(X),1(Y)) -> isBin#(Y)
    plus{AC,#}(0(X),1(Y)) -> and#(isBin(Y),isBinKind(Y))
    plus{AC,#}(0(X),1(Y)) -> isBinKind#(X)
    plus{AC,#}(0(X),1(Y)) -> isBin#(X)
    plus{AC,#}(0(X),1(Y)) -> and#(isBin(X),isBinKind(X))
    plus{AC,#}(0(X),1(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    plus{AC,#}(0(X),1(Y)) -> U141#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    plus{AC,#}(1(X),1(Y)) -> isBinKind#(Y)
    plus{AC,#}(1(X),1(Y)) -> isBin#(Y)
    plus{AC,#}(1(X),1(Y)) -> and#(isBin(Y),isBinKind(Y))
    plus{AC,#}(1(X),1(Y)) -> isBinKind#(X)
    plus{AC,#}(1(X),1(Y)) -> isBin#(X)
    plus{AC,#}(1(X),1(Y)) -> and#(isBin(X),isBinKind(X))
    plus{AC,#}(1(X),1(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    plus{AC,#}(1(X),1(Y)) -> U151#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    prod#(singl(X)) -> isBinKind#(X)
    prod#(singl(X)) -> isBin#(X)
    prod#(singl(X)) -> and#(isBin(X),isBinKind(X))
    prod#(singl(X)) -> U161#(and(isBin(X),isBinKind(X)),X)
    prod#(unionAC(A,B)) -> isBagKind#(B)
    prod#(unionAC(A,B)) -> isBag#(B)
    prod#(unionAC(A,B)) -> and#(isBag(B),isBagKind(B))
    prod#(unionAC(A,B)) -> isBagKind#(A)
    prod#(unionAC(A,B)) -> isBag#(A)
    prod#(unionAC(A,B)) -> and#(isBag(A),isBagKind(A))
    prod#(unionAC(A,B)) -> and#(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B)))
    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)) -> isBinKind#(X)
    sum#(singl(X)) -> isBin#(X)
    sum#(singl(X)) -> and#(isBin(X),isBinKind(X))
    sum#(singl(X)) -> U181#(and(isBin(X),isBinKind(X)),X)
    sum#(unionAC(A,B)) -> isBagKind#(B)
    sum#(unionAC(A,B)) -> isBag#(B)
    sum#(unionAC(A,B)) -> and#(isBag(B),isBagKind(B))
    sum#(unionAC(A,B)) -> isBagKind#(A)
    sum#(unionAC(A,B)) -> isBag#(A)
    sum#(unionAC(A,B)) -> and#(isBag(A),isBagKind(A))
    sum#(unionAC(A,B)) -> and#(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B)))
    sum#(unionAC(A,B)) -> U191#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)
    union{AC,#}(x10,unionAC(X,empty())) -> union{AC,#}(x10,X)
    union{AC,#}(x11,unionAC(empty(),X)) -> union{AC,#}(x11,X)
    mult{AC,#}(x12,multAC(z(),X)) -> isBinKind#(X)
    mult{AC,#}(x12,multAC(z(),X)) -> isBin#(X)
    mult{AC,#}(x12,multAC(z(),X)) -> and#(isBin(X),isBinKind(X))
    mult{AC,#}(x12,multAC(z(),X)) -> U91#(and(isBin(X),isBinKind(X)))
    mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U91(and(isBin(X),isBinKind(X))))
    mult{AC,#}(x13,multAC(0(X),Y)) -> isBinKind#(Y)
    mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(Y)
    mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(Y),isBinKind(Y))
    mult{AC,#}(x13,multAC(0(X),Y)) -> isBinKind#(X)
    mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X)
    mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(X),isBinKind(X))
    mult{AC,#}(x13,multAC(0(X),Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    mult{AC,#}(x13,multAC(0(X),Y)) ->
    U101#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    mult{AC,#}(x13,multAC(0(X),Y)) ->
    mult{AC,#}(x13,U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
    mult{AC,#}(x14,multAC(1(X),Y)) -> isBinKind#(Y)
    mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(Y)
    mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(Y),isBinKind(Y))
    mult{AC,#}(x14,multAC(1(X),Y)) -> isBinKind#(X)
    mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X)
    mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(X),isBinKind(X))
    mult{AC,#}(x14,multAC(1(X),Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    mult{AC,#}(x14,multAC(1(X),Y)) ->
    U111#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    mult{AC,#}(x14,multAC(1(X),Y)) ->
    mult{AC,#}(x14,U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
    plus{AC,#}(x15,plusAC(z(),X)) -> isBinKind#(X)
    plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X)
    plus{AC,#}(x15,plusAC(z(),X)) -> and#(isBin(X),isBinKind(X))
    plus{AC,#}(x15,plusAC(z(),X)) -> U121#(and(isBin(X),isBinKind(X)),X)
    plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U121(and(isBin(X),isBinKind(X)),X))
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBinKind#(Y)
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(Y)
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(Y),isBinKind(Y))
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBinKind#(X)
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X)
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(X),isBinKind(X))
    plus{AC,#}(x16,plusAC(0(X),0(Y))) ->
    and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    plus{AC,#}(x16,plusAC(0(X),0(Y))) ->
    U131#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    plus{AC,#}(x16,plusAC(0(X),0(Y))) ->
    plus{AC,#}(x16,U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBinKind#(Y)
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(Y)
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(Y),isBinKind(Y))
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBinKind#(X)
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X)
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(X),isBinKind(X))
    plus{AC,#}(x17,plusAC(0(X),1(Y))) ->
    and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    plus{AC,#}(x17,plusAC(0(X),1(Y))) ->
    U141#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    plus{AC,#}(x17,plusAC(0(X),1(Y))) ->
    plus{AC,#}(x17,U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBinKind#(Y)
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(Y)
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(Y),isBinKind(Y))
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBinKind#(X)
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X)
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(X),isBinKind(X))
    plus{AC,#}(x18,plusAC(1(X),1(Y))) ->
    and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y)))
    plus{AC,#}(x18,plusAC(1(X),1(Y))) ->
    U151#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)
    plus{AC,#}(x18,plusAC(1(X),1(Y))) ->
    plus{AC,#}(x18,U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y))
   Equations:
    unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9))
    unionAC(x7,x8) -> unionAC(x8,x7)
    multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9))
    multAC(x7,x8) -> multAC(x8,x7)
    plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9))
    plusAC(x7,x8) -> plusAC(x8,x7)
    unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9)
    unionAC(x8,x7) -> unionAC(x7,x8)
    multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9)
    multAC(x8,x7) -> multAC(x7,x8)
    plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9)
    plusAC(x8,x7) -> plusAC(x7,x8)
   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)
   S:
    union{AC,#}(unionAC(x19,x20),x21) -> union{AC,#}(x19,x20)
    union{AC,#}(x19,unionAC(x20,x21)) -> union{AC,#}(x20,x21)
    mult{AC,#}(multAC(x19,x20),x21) -> mult{AC,#}(x19,x20)
    mult{AC,#}(x19,multAC(x20,x21)) -> mult{AC,#}(x20,x21)
    plus{AC,#}(plusAC(x19,x20),x21) -> plus{AC,#}(x19,x20)
    plus{AC,#}(x19,plusAC(x20,x21)) -> plus{AC,#}(x20,x21)
   Open