MAYBE
Time: 0.008

Problem:
 Equations:
  
 TRS:
  unionAC(empty(),X) -> X
  max(singl(x)) -> x
  max(unionAC(singl(x),singl(0()))) -> x
  max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y))))
  max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z)))))

Proof:
 Open