MAYBE
Time: 0.434

Problem:
 Equations:
  
 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:
 Open