MAYBE
Time: 0.001234
TRS:
 {        merge(x, nil()) -> x,
          merge(nil(), y) -> y,
  merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
         if(true(), x, y) -> x,
        if(false(), x, y) -> x,
             ++(nil(), y) -> y,
           ++(.(x, y), z) -> .(x, ++(y, z))}
 DP:
  DP:
   {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)),
    merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v),
    merge#(.(x, y), .(u, v)) -> if#(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
             ++#(.(x, y), z) -> ++#(y, z)}
  TRS:
  {        merge(x, nil()) -> x,
           merge(nil(), y) -> y,
   merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
          if(true(), x, y) -> x,
         if(false(), x, y) -> x,
              ++(nil(), y) -> y,
            ++(.(x, y), z) -> .(x, ++(y, z))}
  EDG:
   {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))
    (merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)), merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)))
    (merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)), merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v))
    (merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)), merge#(.(x, y), .(u, v)) -> if#(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))))
    (merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v), merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)))
    (merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v), merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v))
    (merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v), merge#(.(x, y), .(u, v)) -> if#(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))))}
   STATUS:
    arrows: 0.562500
    SCCS (2):
     Scc:
      {++#(.(x, y), z) -> ++#(y, z)}
     Scc:
      {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)),
       merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v)}
     
     SCC (1):
      Strict:
       {++#(.(x, y), z) -> ++#(y, z)}
      Weak:
      {        merge(x, nil()) -> x,
               merge(nil(), y) -> y,
       merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
              if(true(), x, y) -> x,
             if(false(), x, y) -> x,
                  ++(nil(), y) -> y,
                ++(.(x, y), z) -> .(x, ++(y, z))}
      Open
     SCC (2):
      Strict:
       {merge#(.(x, y), .(u, v)) -> merge#(y, .(u, v)),
        merge#(.(x, y), .(u, v)) -> merge#(.(x, y), v)}
      Weak:
      {        merge(x, nil()) -> x,
               merge(nil(), y) -> y,
       merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))),
              if(true(), x, y) -> x,
             if(false(), x, y) -> x,
                  ++(nil(), y) -> y,
                ++(.(x, y), z) -> .(x, ++(y, z))}
      Open