YES
LCTRS
  Theories
    Core, Ints
  Signature
    f1: Int -> Int
    u_5: (Int, Int) -> Int
  Rules
    u_5(!n, !w_2) -> +(!n, !w_2)
    f1(!n) -> u_5(!n, f1(-(!n, 1))) [>(!n, 0)]
    f1(!n) -> !n [<=(!n, 0)]
RPO with precedence:
  {f1} > {u_5 > <= 1 0 - +}

Elapsed Time:  42.36 ms