MAYBE
Time: 1.397

Problem:
 Equations:
  unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
  unionAC(x5,x6) -> unionAC(x6,x5)
  multAC(multAC(x5,x6),x7) -> multAC(x5,multAC(x6,x7))
  multAC(x5,x6) -> multAC(x6,x5)
  plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7))
  plusAC(x5,x6) -> plusAC(x6,x5)
  unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
  unionAC(x6,x5) -> unionAC(x5,x6)
  multAC(x5,multAC(x6,x7)) -> multAC(multAC(x5,x6),x7)
  multAC(x6,x5) -> multAC(x5,x6)
  plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7)
  plusAC(x6,x5) -> plusAC(x5,x6)
 TRS:
  unionAC(X,empty()) -> X
  unionAC(empty(),X) -> X
  0(z()) -> z()
  and(tt(),X) -> X
  multAC(z(),X) -> z()
  multAC(0(X),Y) -> 0(multAC(X,Y))
  multAC(1(X),Y) -> plusAC(0(multAC(X,Y)),Y)
  plusAC(z(),X) -> X
  plusAC(0(X),0(Y)) -> 0(plusAC(X,Y))
  plusAC(0(X),1(Y)) -> 1(plusAC(X,Y))
  plusAC(1(X),1(Y)) -> 0(plusAC(plusAC(X,Y),1(z())))
  prod(empty()) -> 1(z())
  prod(singl(X)) -> X
  prod(unionAC(A,B)) -> multAC(prod(A),prod(B))
  sum(empty()) -> 0(z())
  sum(singl(X)) -> X
  sum(unionAC(A,B)) -> plusAC(sum(A),sum(B))

Proof:
 DP Processor:
  Equations#:
   union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7))
   union{AC,#}(x5,x6) -> union{AC,#}(x6,x5)
   mult{AC,#}(multAC(x5,x6),x7) -> mult{AC,#}(x5,multAC(x6,x7))
   mult{AC,#}(x5,x6) -> mult{AC,#}(x6,x5)
   plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7))
   plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5)
   union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7)
   union{AC,#}(x6,x5) -> union{AC,#}(x5,x6)
   mult{AC,#}(x5,multAC(x6,x7)) -> mult{AC,#}(multAC(x5,x6),x7)
   mult{AC,#}(x6,x5) -> mult{AC,#}(x5,x6)
   plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7)
   plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6)
  DPs:
   mult{AC,#}(0(X),Y) -> mult{AC,#}(X,Y)
   mult{AC,#}(0(X),Y) -> 0#(multAC(X,Y))
   mult{AC,#}(1(X),Y) -> mult{AC,#}(X,Y)
   mult{AC,#}(1(X),Y) -> 0#(multAC(X,Y))
   mult{AC,#}(1(X),Y) -> plus{AC,#}(0(multAC(X,Y)),Y)
   plus{AC,#}(0(X),0(Y)) -> plus{AC,#}(X,Y)
   plus{AC,#}(0(X),0(Y)) -> 0#(plusAC(X,Y))
   plus{AC,#}(0(X),1(Y)) -> plus{AC,#}(X,Y)
   plus{AC,#}(1(X),1(Y)) -> plus{AC,#}(X,Y)
   plus{AC,#}(1(X),1(Y)) -> plus{AC,#}(plusAC(X,Y),1(z()))
   plus{AC,#}(1(X),1(Y)) -> 0#(plusAC(plusAC(X,Y),1(z())))
   prod#(unionAC(A,B)) -> prod#(B)
   prod#(unionAC(A,B)) -> prod#(A)
   prod#(unionAC(A,B)) -> mult{AC,#}(prod(A),prod(B))
   sum#(empty()) -> 0#(z())
   sum#(unionAC(A,B)) -> sum#(B)
   sum#(unionAC(A,B)) -> sum#(A)
   sum#(unionAC(A,B)) -> plus{AC,#}(sum(A),sum(B))
   union{AC,#}(x8,unionAC(X,empty())) -> union{AC,#}(x8,X)
   union{AC,#}(x9,unionAC(empty(),X)) -> union{AC,#}(x9,X)
   mult{AC,#}(x10,multAC(z(),X)) -> mult{AC,#}(x10,z())
   mult{AC,#}(x11,multAC(0(X),Y)) -> mult{AC,#}(X,Y)
   mult{AC,#}(x11,multAC(0(X),Y)) -> 0#(multAC(X,Y))
   mult{AC,#}(x11,multAC(0(X),Y)) -> mult{AC,#}(x11,0(multAC(X,Y)))
   mult{AC,#}(x12,multAC(1(X),Y)) -> mult{AC,#}(X,Y)
   mult{AC,#}(x12,multAC(1(X),Y)) -> 0#(multAC(X,Y))
   mult{AC,#}(x12,multAC(1(X),Y)) -> plus{AC,#}(0(multAC(X,Y)),Y)
   mult{AC,#}(x12,multAC(1(X),Y)) -> mult{AC,#}(x12,plusAC(0(multAC(X,Y)),Y))
   plus{AC,#}(x13,plusAC(z(),X)) -> plus{AC,#}(x13,X)
   plus{AC,#}(x14,plusAC(0(X),0(Y))) -> plus{AC,#}(X,Y)
   plus{AC,#}(x14,plusAC(0(X),0(Y))) -> 0#(plusAC(X,Y))
   plus{AC,#}(x14,plusAC(0(X),0(Y))) -> plus{AC,#}(x14,0(plusAC(X,Y)))
   plus{AC,#}(x15,plusAC(0(X),1(Y))) -> plus{AC,#}(X,Y)
   plus{AC,#}(x15,plusAC(0(X),1(Y))) -> plus{AC,#}(x15,1(plusAC(X,Y)))
   plus{AC,#}(x16,plusAC(1(X),1(Y))) -> plus{AC,#}(X,Y)
   plus{AC,#}(x16,plusAC(1(X),1(Y))) -> plus{AC,#}(plusAC(X,Y),1(z()))
   plus{AC,#}(x16,plusAC(1(X),1(Y))) -> 0#(plusAC(plusAC(X,Y),1(z())))
   plus{AC,#}(x16,plusAC(1(X),1(Y))) -> plus{AC,#}(x16,0(plusAC(plusAC(X,Y),1(z()))))
  Equations:
   unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
   unionAC(x5,x6) -> unionAC(x6,x5)
   multAC(multAC(x5,x6),x7) -> multAC(x5,multAC(x6,x7))
   multAC(x5,x6) -> multAC(x6,x5)
   plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7))
   plusAC(x5,x6) -> plusAC(x6,x5)
   unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
   unionAC(x6,x5) -> unionAC(x5,x6)
   multAC(x5,multAC(x6,x7)) -> multAC(multAC(x5,x6),x7)
   multAC(x6,x5) -> multAC(x5,x6)
   plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7)
   plusAC(x6,x5) -> plusAC(x5,x6)
  TRS:
   unionAC(X,empty()) -> X
   unionAC(empty(),X) -> X
   0(z()) -> z()
   and(tt(),X) -> X
   multAC(z(),X) -> z()
   multAC(0(X),Y) -> 0(multAC(X,Y))
   multAC(1(X),Y) -> plusAC(0(multAC(X,Y)),Y)
   plusAC(z(),X) -> X
   plusAC(0(X),0(Y)) -> 0(plusAC(X,Y))
   plusAC(0(X),1(Y)) -> 1(plusAC(X,Y))
   plusAC(1(X),1(Y)) -> 0(plusAC(plusAC(X,Y),1(z())))
   prod(empty()) -> 1(z())
   prod(singl(X)) -> X
   prod(unionAC(A,B)) -> multAC(prod(A),prod(B))
   sum(empty()) -> 0(z())
   sum(singl(X)) -> X
   sum(unionAC(A,B)) -> plusAC(sum(A),sum(B))
  S:
   union{AC,#}(unionAC(x17,x18),x19) -> union{AC,#}(x17,x18)
   union{AC,#}(x17,unionAC(x18,x19)) -> union{AC,#}(x18,x19)
   mult{AC,#}(multAC(x17,x18),x19) -> mult{AC,#}(x17,x18)
   mult{AC,#}(x17,multAC(x18,x19)) -> mult{AC,#}(x18,x19)
   plus{AC,#}(plusAC(x17,x18),x19) -> plus{AC,#}(x17,x18)
   plus{AC,#}(x17,plusAC(x18,x19)) -> plus{AC,#}(x18,x19)
  AC-EDG Processor:
   Equations#:
    union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7))
    union{AC,#}(x5,x6) -> union{AC,#}(x6,x5)
    mult{AC,#}(multAC(x5,x6),x7) -> mult{AC,#}(x5,multAC(x6,x7))
    mult{AC,#}(x5,x6) -> mult{AC,#}(x6,x5)
    plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7))
    plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5)
    union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7)
    union{AC,#}(x6,x5) -> union{AC,#}(x5,x6)
    mult{AC,#}(x5,multAC(x6,x7)) -> mult{AC,#}(multAC(x5,x6),x7)
    mult{AC,#}(x6,x5) -> mult{AC,#}(x5,x6)
    plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7)
    plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6)
   DPs:
    mult{AC,#}(0(X),Y) -> mult{AC,#}(X,Y)
    mult{AC,#}(0(X),Y) -> 0#(multAC(X,Y))
    mult{AC,#}(1(X),Y) -> mult{AC,#}(X,Y)
    mult{AC,#}(1(X),Y) -> 0#(multAC(X,Y))
    mult{AC,#}(1(X),Y) -> plus{AC,#}(0(multAC(X,Y)),Y)
    plus{AC,#}(0(X),0(Y)) -> plus{AC,#}(X,Y)
    plus{AC,#}(0(X),0(Y)) -> 0#(plusAC(X,Y))
    plus{AC,#}(0(X),1(Y)) -> plus{AC,#}(X,Y)
    plus{AC,#}(1(X),1(Y)) -> plus{AC,#}(X,Y)
    plus{AC,#}(1(X),1(Y)) -> plus{AC,#}(plusAC(X,Y),1(z()))
    plus{AC,#}(1(X),1(Y)) -> 0#(plusAC(plusAC(X,Y),1(z())))
    prod#(unionAC(A,B)) -> prod#(B)
    prod#(unionAC(A,B)) -> prod#(A)
    prod#(unionAC(A,B)) -> mult{AC,#}(prod(A),prod(B))
    sum#(empty()) -> 0#(z())
    sum#(unionAC(A,B)) -> sum#(B)
    sum#(unionAC(A,B)) -> sum#(A)
    sum#(unionAC(A,B)) -> plus{AC,#}(sum(A),sum(B))
    union{AC,#}(x8,unionAC(X,empty())) -> union{AC,#}(x8,X)
    union{AC,#}(x9,unionAC(empty(),X)) -> union{AC,#}(x9,X)
    mult{AC,#}(x10,multAC(z(),X)) -> mult{AC,#}(x10,z())
    mult{AC,#}(x11,multAC(0(X),Y)) -> mult{AC,#}(X,Y)
    mult{AC,#}(x11,multAC(0(X),Y)) -> 0#(multAC(X,Y))
    mult{AC,#}(x11,multAC(0(X),Y)) -> mult{AC,#}(x11,0(multAC(X,Y)))
    mult{AC,#}(x12,multAC(1(X),Y)) -> mult{AC,#}(X,Y)
    mult{AC,#}(x12,multAC(1(X),Y)) -> 0#(multAC(X,Y))
    mult{AC,#}(x12,multAC(1(X),Y)) -> plus{AC,#}(0(multAC(X,Y)),Y)
    mult{AC,#}(x12,multAC(1(X),Y)) -> mult{AC,#}(x12,plusAC(0(multAC(X,Y)),Y))
    plus{AC,#}(x13,plusAC(z(),X)) -> plus{AC,#}(x13,X)
    plus{AC,#}(x14,plusAC(0(X),0(Y))) -> plus{AC,#}(X,Y)
    plus{AC,#}(x14,plusAC(0(X),0(Y))) -> 0#(plusAC(X,Y))
    plus{AC,#}(x14,plusAC(0(X),0(Y))) -> plus{AC,#}(x14,0(plusAC(X,Y)))
    plus{AC,#}(x15,plusAC(0(X),1(Y))) -> plus{AC,#}(X,Y)
    plus{AC,#}(x15,plusAC(0(X),1(Y))) -> plus{AC,#}(x15,1(plusAC(X,Y)))
    plus{AC,#}(x16,plusAC(1(X),1(Y))) -> plus{AC,#}(X,Y)
    plus{AC,#}(x16,plusAC(1(X),1(Y))) -> plus{AC,#}(plusAC(X,Y),1(z()))
    plus{AC,#}(x16,plusAC(1(X),1(Y))) -> 0#(plusAC(plusAC(X,Y),1(z())))
    plus{AC,#}(x16,plusAC(1(X),1(Y))) -> plus{AC,#}(x16,0(plusAC(plusAC(X,Y),1(z()))))
   Equations:
    unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
    unionAC(x5,x6) -> unionAC(x6,x5)
    multAC(multAC(x5,x6),x7) -> multAC(x5,multAC(x6,x7))
    multAC(x5,x6) -> multAC(x6,x5)
    plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7))
    plusAC(x5,x6) -> plusAC(x6,x5)
    unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
    unionAC(x6,x5) -> unionAC(x5,x6)
    multAC(x5,multAC(x6,x7)) -> multAC(multAC(x5,x6),x7)
    multAC(x6,x5) -> multAC(x5,x6)
    plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7)
    plusAC(x6,x5) -> plusAC(x5,x6)
   TRS:
    unionAC(X,empty()) -> X
    unionAC(empty(),X) -> X
    0(z()) -> z()
    and(tt(),X) -> X
    multAC(z(),X) -> z()
    multAC(0(X),Y) -> 0(multAC(X,Y))
    multAC(1(X),Y) -> plusAC(0(multAC(X,Y)),Y)
    plusAC(z(),X) -> X
    plusAC(0(X),0(Y)) -> 0(plusAC(X,Y))
    plusAC(0(X),1(Y)) -> 1(plusAC(X,Y))
    plusAC(1(X),1(Y)) -> 0(plusAC(plusAC(X,Y),1(z())))
    prod(empty()) -> 1(z())
    prod(singl(X)) -> X
    prod(unionAC(A,B)) -> multAC(prod(A),prod(B))
    sum(empty()) -> 0(z())
    sum(singl(X)) -> X
    sum(unionAC(A,B)) -> plusAC(sum(A),sum(B))
   S:
    union{AC,#}(unionAC(x17,x18),x19) -> union{AC,#}(x17,x18)
    union{AC,#}(x17,unionAC(x18,x19)) -> union{AC,#}(x18,x19)
    mult{AC,#}(multAC(x17,x18),x19) -> mult{AC,#}(x17,x18)
    mult{AC,#}(x17,multAC(x18,x19)) -> mult{AC,#}(x18,x19)
    plus{AC,#}(plusAC(x17,x18),x19) -> plus{AC,#}(x17,x18)
    plus{AC,#}(x17,plusAC(x18,x19)) -> plus{AC,#}(x18,x19)
   Open