YES
LCTRS
  Theories
    Core, Ints
  Signature
    g2: (Int, Int) -> Int
    triangle2: Int -> Int
    u_16: Int -> Int
    u_23: Int -> Int
  Rules
    g2(?17, ?18) -> ?18 [<=(?17, 0)]
    g2(?19, ?20) -> u_23(g2(-(?19, 1), +(?19, ?20))) [>(?19, 0)]
    triangle2(?21) -> u_16(g2(?21, 0))
    u_16(?22) -> ?22
    u_23(?23) -> ?23
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  72.71 ms