YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    sum: Int -> Int
    test: Int -> Unit
  Rules
    sum(?12) -> +(?12, sum(-(?12, 1))) [<(0, ?12)]
    sum(?13) -> 0 [or(<(?13, 0), ?13 = 0)]
    test(?14) -> test(?15) [and(>(?14, 0), ?14 = +(?15, 1))]
Confluent by Weak Orthogonality with proof:
  * Critical Pair
    Inner Rule
      test(?14') -> test(?15') [and(>(?14', 0), ?14' = +(?15', 1))]
    Outer Rule
      test(?14") -> test(?15") [and(>(?14", 0), ?14" = +(?15", 1))]
    Pair
      test(?15') ≈ test(?15") [and(>(?14", 0), ?14" = +(?15', 1)), and(>(?14", 0), ?14" = +(?15", 1))]
  but it is a trivial constrained equation
    test(?15') ≈ test(?15") [and(>(?14", 0), ?14" = +(?15', 1)), and(>(?14", 0), ?14" = +(?15", 1))]

Elapsed Time:  83.96 ms