MAYBE
Time: 14.622

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) -> 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:
 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) -> isBin#(Y)
   U101#(tt(),X,Y) -> U102#(isBin(Y),X,Y)
   U102#(tt(),X,Y) -> mult{AC,#}(X,Y)
   U102#(tt(),X,Y) -> 0#(multAC(X,Y))
   U111#(tt(),X,Y) -> isBin#(Y)
   U111#(tt(),X,Y) -> U112#(isBin(Y),X,Y)
   U112#(tt(),X,Y) -> mult{AC,#}(X,Y)
   U112#(tt(),X,Y) -> 0#(multAC(X,Y))
   U112#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y)
   U131#(tt(),X,Y) -> isBin#(Y)
   U131#(tt(),X,Y) -> U132#(isBin(Y),X,Y)
   U132#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U132#(tt(),X,Y) -> 0#(plusAC(X,Y))
   U141#(tt(),X,Y) -> isBin#(Y)
   U141#(tt(),X,Y) -> U142#(isBin(Y),X,Y)
   U142#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U151#(tt(),X,Y) -> isBin#(Y)
   U151#(tt(),X,Y) -> U152#(isBin(Y),X,Y)
   U152#(tt(),X,Y) -> plus{AC,#}(X,Y)
   U152#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z()))
   U152#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z())))
   U171#(tt(),A,B) -> isBag#(B)
   U171#(tt(),A,B) -> U172#(isBag(B),A,B)
   U172#(tt(),A,B) -> prod#(B)
   U172#(tt(),A,B) -> prod#(A)
   U172#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B))
   U191#(tt(),A,B) -> isBag#(B)
   U191#(tt(),A,B) -> U192#(isBag(B),A,B)
   U192#(tt(),A,B) -> sum#(B)
   U192#(tt(),A,B) -> sum#(A)
   U192#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B))
   U21#(tt(),V2) -> isBag#(V2)
   U21#(tt(),V2) -> U22#(isBag(V2))
   U51#(tt(),V2) -> isBin#(V2)
   U51#(tt(),V2) -> U52#(isBin(V2))
   U61#(tt(),V2) -> isBin#(V2)
   U61#(tt(),V2) -> U62#(isBin(V2))
   isBag#(singl(V1)) -> isBin#(V1)
   isBag#(singl(V1)) -> U11#(isBin(V1))
   isBag#(unionAC(V1,V2)) -> isBag#(V1)
   isBag#(unionAC(V1,V2)) -> U21#(isBag(V1),V2)
   isBin#(0(V1)) -> isBin#(V1)
   isBin#(0(V1)) -> U31#(isBin(V1))
   isBin#(1(V1)) -> isBin#(V1)
   isBin#(1(V1)) -> U41#(isBin(V1))
   isBin#(multAC(V1,V2)) -> isBin#(V1)
   isBin#(multAC(V1,V2)) -> U51#(isBin(V1),V2)
   isBin#(plusAC(V1,V2)) -> isBin#(V1)
   isBin#(plusAC(V1,V2)) -> U61#(isBin(V1),V2)
   isBin#(prod(V1)) -> isBag#(V1)
   isBin#(prod(V1)) -> U71#(isBag(V1))
   isBin#(sum(V1)) -> isBag#(V1)
   isBin#(sum(V1)) -> U81#(isBag(V1))
   mult{AC,#}(z(),X) -> isBin#(X)
   mult{AC,#}(z(),X) -> U91#(isBin(X))
   mult{AC,#}(0(X),Y) -> isBin#(X)
   mult{AC,#}(0(X),Y) -> U101#(isBin(X),X,Y)
   mult{AC,#}(1(X),Y) -> isBin#(X)
   mult{AC,#}(1(X),Y) -> U111#(isBin(X),X,Y)
   plus{AC,#}(z(),X) -> isBin#(X)
   plus{AC,#}(z(),X) -> U121#(isBin(X),X)
   plus{AC,#}(0(X),0(Y)) -> isBin#(X)
   plus{AC,#}(0(X),0(Y)) -> U131#(isBin(X),X,Y)
   plus{AC,#}(0(X),1(Y)) -> isBin#(X)
   plus{AC,#}(0(X),1(Y)) -> U141#(isBin(X),X,Y)
   plus{AC,#}(1(X),1(Y)) -> isBin#(X)
   plus{AC,#}(1(X),1(Y)) -> U151#(isBin(X),X,Y)
   prod#(singl(X)) -> isBin#(X)
   prod#(singl(X)) -> U161#(isBin(X),X)
   prod#(unionAC(A,B)) -> isBag#(A)
   prod#(unionAC(A,B)) -> U171#(isBag(A),A,B)
   sum#(empty()) -> 0#(z())
   sum#(singl(X)) -> isBin#(X)
   sum#(singl(X)) -> U181#(isBin(X),X)
   sum#(unionAC(A,B)) -> isBag#(A)
   sum#(unionAC(A,B)) -> U191#(isBag(A),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)) -> isBin#(X)
   mult{AC,#}(x12,multAC(z(),X)) -> U91#(isBin(X))
   mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U91(isBin(X)))
   mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X)
   mult{AC,#}(x13,multAC(0(X),Y)) -> U101#(isBin(X),X,Y)
   mult{AC,#}(x13,multAC(0(X),Y)) -> mult{AC,#}(x13,U101(isBin(X),X,Y))
   mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X)
   mult{AC,#}(x14,multAC(1(X),Y)) -> U111#(isBin(X),X,Y)
   mult{AC,#}(x14,multAC(1(X),Y)) -> mult{AC,#}(x14,U111(isBin(X),X,Y))
   plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X)
   plus{AC,#}(x15,plusAC(z(),X)) -> U121#(isBin(X),X)
   plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U121(isBin(X),X))
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X)
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> U131#(isBin(X),X,Y)
   plus{AC,#}(x16,plusAC(0(X),0(Y))) -> plus{AC,#}(x16,U131(isBin(X),X,Y))
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X)
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> U141#(isBin(X),X,Y)
   plus{AC,#}(x17,plusAC(0(X),1(Y))) -> plus{AC,#}(x17,U141(isBin(X),X,Y))
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X)
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> U151#(isBin(X),X,Y)
   plus{AC,#}(x18,plusAC(1(X),1(Y))) -> plus{AC,#}(x18,U151(isBin(X),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) -> 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)
  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) -> isBin#(Y)
    U101#(tt(),X,Y) -> U102#(isBin(Y),X,Y)
    U102#(tt(),X,Y) -> mult{AC,#}(X,Y)
    U102#(tt(),X,Y) -> 0#(multAC(X,Y))
    U111#(tt(),X,Y) -> isBin#(Y)
    U111#(tt(),X,Y) -> U112#(isBin(Y),X,Y)
    U112#(tt(),X,Y) -> mult{AC,#}(X,Y)
    U112#(tt(),X,Y) -> 0#(multAC(X,Y))
    U112#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y)
    U131#(tt(),X,Y) -> isBin#(Y)
    U131#(tt(),X,Y) -> U132#(isBin(Y),X,Y)
    U132#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U132#(tt(),X,Y) -> 0#(plusAC(X,Y))
    U141#(tt(),X,Y) -> isBin#(Y)
    U141#(tt(),X,Y) -> U142#(isBin(Y),X,Y)
    U142#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U151#(tt(),X,Y) -> isBin#(Y)
    U151#(tt(),X,Y) -> U152#(isBin(Y),X,Y)
    U152#(tt(),X,Y) -> plus{AC,#}(X,Y)
    U152#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z()))
    U152#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z())))
    U171#(tt(),A,B) -> isBag#(B)
    U171#(tt(),A,B) -> U172#(isBag(B),A,B)
    U172#(tt(),A,B) -> prod#(B)
    U172#(tt(),A,B) -> prod#(A)
    U172#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B))
    U191#(tt(),A,B) -> isBag#(B)
    U191#(tt(),A,B) -> U192#(isBag(B),A,B)
    U192#(tt(),A,B) -> sum#(B)
    U192#(tt(),A,B) -> sum#(A)
    U192#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B))
    U21#(tt(),V2) -> isBag#(V2)
    U21#(tt(),V2) -> U22#(isBag(V2))
    U51#(tt(),V2) -> isBin#(V2)
    U51#(tt(),V2) -> U52#(isBin(V2))
    U61#(tt(),V2) -> isBin#(V2)
    U61#(tt(),V2) -> U62#(isBin(V2))
    isBag#(singl(V1)) -> isBin#(V1)
    isBag#(singl(V1)) -> U11#(isBin(V1))
    isBag#(unionAC(V1,V2)) -> isBag#(V1)
    isBag#(unionAC(V1,V2)) -> U21#(isBag(V1),V2)
    isBin#(0(V1)) -> isBin#(V1)
    isBin#(0(V1)) -> U31#(isBin(V1))
    isBin#(1(V1)) -> isBin#(V1)
    isBin#(1(V1)) -> U41#(isBin(V1))
    isBin#(multAC(V1,V2)) -> isBin#(V1)
    isBin#(multAC(V1,V2)) -> U51#(isBin(V1),V2)
    isBin#(plusAC(V1,V2)) -> isBin#(V1)
    isBin#(plusAC(V1,V2)) -> U61#(isBin(V1),V2)
    isBin#(prod(V1)) -> isBag#(V1)
    isBin#(prod(V1)) -> U71#(isBag(V1))
    isBin#(sum(V1)) -> isBag#(V1)
    isBin#(sum(V1)) -> U81#(isBag(V1))
    mult{AC,#}(z(),X) -> isBin#(X)
    mult{AC,#}(z(),X) -> U91#(isBin(X))
    mult{AC,#}(0(X),Y) -> isBin#(X)
    mult{AC,#}(0(X),Y) -> U101#(isBin(X),X,Y)
    mult{AC,#}(1(X),Y) -> isBin#(X)
    mult{AC,#}(1(X),Y) -> U111#(isBin(X),X,Y)
    plus{AC,#}(z(),X) -> isBin#(X)
    plus{AC,#}(z(),X) -> U121#(isBin(X),X)
    plus{AC,#}(0(X),0(Y)) -> isBin#(X)
    plus{AC,#}(0(X),0(Y)) -> U131#(isBin(X),X,Y)
    plus{AC,#}(0(X),1(Y)) -> isBin#(X)
    plus{AC,#}(0(X),1(Y)) -> U141#(isBin(X),X,Y)
    plus{AC,#}(1(X),1(Y)) -> isBin#(X)
    plus{AC,#}(1(X),1(Y)) -> U151#(isBin(X),X,Y)
    prod#(singl(X)) -> isBin#(X)
    prod#(singl(X)) -> U161#(isBin(X),X)
    prod#(unionAC(A,B)) -> isBag#(A)
    prod#(unionAC(A,B)) -> U171#(isBag(A),A,B)
    sum#(empty()) -> 0#(z())
    sum#(singl(X)) -> isBin#(X)
    sum#(singl(X)) -> U181#(isBin(X),X)
    sum#(unionAC(A,B)) -> isBag#(A)
    sum#(unionAC(A,B)) -> U191#(isBag(A),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)) -> isBin#(X)
    mult{AC,#}(x12,multAC(z(),X)) -> U91#(isBin(X))
    mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U91(isBin(X)))
    mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X)
    mult{AC,#}(x13,multAC(0(X),Y)) -> U101#(isBin(X),X,Y)
    mult{AC,#}(x13,multAC(0(X),Y)) -> mult{AC,#}(x13,U101(isBin(X),X,Y))
    mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X)
    mult{AC,#}(x14,multAC(1(X),Y)) -> U111#(isBin(X),X,Y)
    mult{AC,#}(x14,multAC(1(X),Y)) -> mult{AC,#}(x14,U111(isBin(X),X,Y))
    plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X)
    plus{AC,#}(x15,plusAC(z(),X)) -> U121#(isBin(X),X)
    plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U121(isBin(X),X))
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X)
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> U131#(isBin(X),X,Y)
    plus{AC,#}(x16,plusAC(0(X),0(Y))) -> plus{AC,#}(x16,U131(isBin(X),X,Y))
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X)
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> U141#(isBin(X),X,Y)
    plus{AC,#}(x17,plusAC(0(X),1(Y))) -> plus{AC,#}(x17,U141(isBin(X),X,Y))
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X)
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> U151#(isBin(X),X,Y)
    plus{AC,#}(x18,plusAC(1(X),1(Y))) -> plus{AC,#}(x18,U151(isBin(X),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) -> 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)
   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