YES
LCTRS
  Theories
    Core, Ints
  Signature
    double: Int -> Int
    sucsuc: Int -> Int
    u: (Int, Int, Int) -> Int
  Rules
    double(?16) -> u(?16, 1, 0)
    sucsuc(?17) -> +(?17, 2)
    u(?18, ?19, ?20) -> ?20 [not(<=(?19, ?18))]
    u(?21, ?22, ?23) -> u(?21, +(?22, 1), sucsuc(?23)) [<=(?22, ?21)]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  44.60 ms