YES
LCTRS
  Theories
    Core, Ints
  Signature
    minus: (Int, Int) -> Int
    quot: (Int, Int) -> Int
  Rules
    minus(?21, ?22) -> minus(0, -(?22, ?21)) [and(>=(?21, 0), >(?22, ?21))]
    minus(?23, ?24) -> -(?23, ?24) [and(>=(?24, 0), >=(?23, ?24))]
    quot(?25, ?26) -> +(quot(minus(?25, ?26), +(?26, 1)), 1) [and(>(?25, 0), >(?26, 0))]
    quot(?27, ?28) -> 0 [?27 = 0, >(?28, 0)]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  45.81 ms