YES(?,POLY) 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: YES(?,POLY) Input Problem: innermost runtime-complexity with respect to Rules: { merge(x, nil()) -> x , merge(nil(), y) -> y , merge(++(x, y), ++(u(), v())) -> ++(x, merge(y, ++(u(), v()))) , merge(++(x, y), ++(u(), v())) -> ++(u(), merge(++(x, y), v()))} Proof Output: The input was oriented with the instance of POP* as induced by the precedence empty and safe mapping safe(merge) = {}, safe(nil) = {}, safe(++) = {1, 2}, safe(u) = {}, safe(v) = {} . For your convenience, here is the input in predicative notation: Rules: { merge(x, nil();) -> x , merge(nil(), y;) -> y , merge(++(; x, y), ++(; u(), v());) -> ++(; x, merge(y, ++(; u(), v());)) , merge(++(; x, y), ++(; u(), v());) -> ++(; u(), merge(++(; x, y), v();))}