YES
LCTRS
  Theories
    Core, Ints
  Defines
    max: ((x Int) (y Int)) Int (ite (>= x y) x y)
  Signature
    build: Int -> Int
    cmod: (Int, Int) -> Int
    if_mod: (Int, Int) -> Int
    minus: (Int, Int) -> Int
    pred: Int -> Int
  Rules
    cmod(?47, ?48) -> if_mod(?47, ?48) [and(>(?47, 0), >(?48, 0))]
    cmod(?49, ?50) -> 0 [or(?49 = 0, and(?50 = 0, >(?49, 0)))]
    if_mod(?51, ?52) -> ?51 [and(not(<=(-(?52, 1), -(?51, 1))), and(>(?51, 1), >(?52, 1)))]
    if_mod(?53, ?54) -> cmod(minus(-(?53, 1), -(?54, 1)), ?54) [and(<=(-(?54, 1), -(?53, 1)), and(>(?53, 1), >(?54, 1)))]
    minus(?55, ?56) -> ?57 [and(>=(?56, 0), and(>=(?55, ?56), ?57 = max(-(?55, ?56), 0)))]
Confluent by Development Closedness with proof:
    * Critical Pair
      Inner Rule
        minus(?55', ?56') -> ?57' [and(>=(?56', 0), and(>=(?55', ?56'), ?57' = max(-(?55', ?56'), 0)))]
      Outer Rule
        minus(?55", ?56") -> ?57" [and(>=(?56", 0), and(>=(?55", ?56"), ?57" = max(-(?55", ?56"), 0)))]
      Pair
        ?57' ≈ ?57" [and(>=(?56", 0), and(>=(?55", ?56"), ?57' = max(-(?55", ?56"), 0))), and(>=(?56", 0), and(>=(?55", ?56"), ?57" = max(-(?55", ?56"), 0)))]
    which reaches the trivial constrained equation
      ?57' ≈ ?57" [and(>=(?56", 0), and(>=(?55", ?56"), ?57' = max(-(?55", ?56"), 0))), and(>=(?56", 0), and(>=(?55", ?56"), ?57" = max(-(?55", ?56"), 0)))]
        -o-> ?57' ≈ ?57" [and(>=(?56", 0), and(>=(?55", ?56"), ?57' = max(-(?55", ?56"), 0))), and(>=(?56", 0), and(>=(?55", ?56"), ?57" = max(-(?55", ?56"), 0)))]

Elapsed Time: 128.66 ms