YES
LCTRS
  Theories
    Core, Ints
  Signature
    plus: (Int, Int) -> Int
    sum: Int -> Int
    sumsum: Int -> Int
    sumsum1: Int -> Int
    u0: (Int, Int, Int, Int) -> Int
    u1: (Int, Int, Int, Int) -> Int
  Rules
    plus(?58, ?59) -> +(?58, ?59)
    sum(?60) -> plus(sum(-(?60, 1)), ?60) [>=(-(?60, 1), 0)]
    sum(?61) -> 0 [<=(?61, 0)]
    sumsum(?62) -> plus(sumsum(-(?62, 1)), sum(?62)) [>=(-(?62, 1), 0)]
    sumsum(?63) -> 0 [<=(?63, 0)]
    sumsum1(?64) -> u0(?64, 0, 0, 0)
    u0(?65, ?66, ?67, ?68) -> ?68 [not(>=(?65, ?66))]
    u0(?69, ?70, ?71, ?72) -> u1(?69, ?70, 0, ?72) [>=(?69, ?70)]
    u1(?73, ?74, ?75, ?76) -> u0(?73, +(?74, 1), ?75, ?76) [not(>=(?74, ?75))]
    u1(?77, ?78, ?79, ?80) -> u1(?77, ?78, +(?79, 1), +(?80, ?79)) [>=(?78, ?79)]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  43.26 ms