YES
LCTRS
  Theories
    Core, Ints
  Signature
    geq: (Int, Int) -> Bool
    plus: (Int, Int) -> Int
    sum: Int -> Int
    sum2: (Bool, Int) -> Int
  Rules
    geq(?22, ?23) -> false [<(?22, ?23)]
    geq(?24, ?25) -> true [>=(?24, ?25)]
    plus(?26, ?27) -> ?28 [+(?26, ?27) = ?28]
    sum(?29) -> sum2(geq(0, ?29), ?29)
    sum2(?30, ?31) -> plus(?31, sum(plus(?31, -1))) [?30 = false]
    sum2(?32, ?33) -> 0 [?32 = true]
Confluent by Parallel Closedness with proof:
    * Critical Pair
      Inner Rule
        plus(?26', ?27') -> ?28' [+(?26', ?27') = ?28']
      Outer Rule
        plus(?26", ?27") -> ?28" [+(?26", ?27") = ?28"]
      Pair
        ?28' ≈ ?28" [+(?26", ?27") = ?28', +(?26", ?27") = ?28"]
    which reaches the trivial constrained equation
      ?28' ≈ ?28" [+(?26", ?27") = ?28', +(?26", ?27") = ?28"]
        -||-> ?28' ≈ ?28" [+(?26", ?27") = ?28', +(?26", ?27") = ?28"]

Elapsed Time:  79.03 ms