MAYBE
Time: 0.465

Problem:
 Equations:
  unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
  unionAC(x5,x6) -> unionAC(x6,x5)
  unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
  unionAC(x6,x5) -> unionAC(x5,x6)
 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:
 DP Processor:
  Equations#:
   union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7))
   union{AC,#}(x5,x6) -> union{AC,#}(x6,x5)
   union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7)
   union{AC,#}(x6,x5) -> union{AC,#}(x5,x6)
  DPs:
   max#(unionAC(singl(s(x)),singl(s(y)))) -> union{AC,#}(singl(x),singl(y))
   max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y)))
   max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(Y,Z))
   max#(unionAC(singl(x),unionAC(Y,Z))) -> union{AC,#}(singl(x),singl(max(unionAC(Y,Z))))
   max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(singl(x),singl(max(unionAC(Y,Z)))))
   union{AC,#}(x8,unionAC(empty(),X)) -> union{AC,#}(x8,X)
  Equations:
   unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
   unionAC(x5,x6) -> unionAC(x6,x5)
   unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
   unionAC(x6,x5) -> unionAC(x5,x6)
  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)))))
  S:
   union{AC,#}(unionAC(x9,x10),x11) -> union{AC,#}(x9,x10)
   union{AC,#}(x9,unionAC(x10,x11)) -> union{AC,#}(x10,x11)
  AC-EDG Processor:
   Equations#:
    union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7))
    union{AC,#}(x5,x6) -> union{AC,#}(x6,x5)
    union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7)
    union{AC,#}(x6,x5) -> union{AC,#}(x5,x6)
   DPs:
    max#(unionAC(singl(s(x)),singl(s(y)))) -> union{AC,#}(singl(x),singl(y))
    max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y)))
    max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(Y,Z))
    max#(unionAC(singl(x),unionAC(Y,Z))) -> union{AC,#}(singl(x),singl(max(unionAC(Y,Z))))
    max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(singl(x),singl(max(unionAC(Y,Z)))))
    union{AC,#}(x8,unionAC(empty(),X)) -> union{AC,#}(x8,X)
   Equations:
    unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7))
    unionAC(x5,x6) -> unionAC(x6,x5)
    unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7)
    unionAC(x6,x5) -> unionAC(x5,x6)
   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)))))
   S:
    union{AC,#}(unionAC(x9,x10),x11) -> union{AC,#}(x9,x10)
    union{AC,#}(x9,unionAC(x10,x11)) -> union{AC,#}(x10,x11)
   Open