YES(?,ELEMENTARY)

'epo* (timeout of 60.0 seconds)'
--------------------------------
Answer:           YES(?,ELEMENTARY)
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  merge(nil(), y) -> y
     , merge(x, nil()) -> x
     , merge(.(x, y), .(u, v)) ->
       if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
     , ++(nil(), y) -> y
     , ++(.(x, y), z) -> .(x, ++(y, z))
     , if(true(), x, y) -> x
     , if(false(), x, y) -> x}

Proof Output:    
  Strict Rules in Predicative Notation:
   {  merge(nil(), y;) -> y
    , merge(x, nil();) -> x
    , merge(.(; x, y), .(; u, v);) ->
      if(; <(; x, u),
           .(; x, merge(y, .(; u, v);)),
           .(; u, merge(.(; x, y), v;)))
    , ++(nil(); y) -> y
    , ++(.(; x, y); z) -> .(; x, ++(y; z))
    , if(; true(), x, y) -> x
    , if(; false(), x, y) -> x}
  Safe Mapping:
   safe(merge) = {}, safe(nil) = {}, safe(.) = {1, 2},
   safe(if) = {1, 2, 3}, safe(<) = {1, 2}, safe(++) = {2},
   safe(true) = {}, safe(false) = {}
  Argument Permutation:
   mu(merge) = [1, 2], mu(if) = [3, 2, 1], mu(++) = [2, 1]
  Precedence:
   ++ ~ ++, ++ > if, if ~ if, merge > ++, merge > if, merge ~ merge