YES
LCTRS
  Theories
    Core, Ints
  Signature
    f1: Int -> Int
    u_5: Int -> Int
    u_8: Int -> Int
  Rules
    f1(?11) -> u_5(f1(+(?11, 11))) [<=(?11, 100)]
    f1(?12) -> -(?12, 10) [>(?12, 100)]
    u_5(?13) -> u_8(f1(?13))
    u_8(?14) -> ?14
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  65.98 ms