NO
LCTRS
  Theories
    Core, Ints
  Signature
    minus: (Int, Int) -> Int
    quot: (Int, Int) -> Int
  Rules
    minus(?27, ?28) -> minus(0, -(?28, ?27)) [and(>=(?27, 0), >(?28, ?27))]
    minus(?29, ?30) -> -(?29, ?30) [and(>=(?30, 0), >=(?29, ?30))]
    minus(minus(?31, ?32), ?33) -> minus(?31, +(?32, ?33))
    quot(?34, ?35) -> +(quot(minus(?34, ?35), +(?35, 1)), 1) [and(>(?34, 0), >(?35, 0))]
    quot(?36, ?37) -> 0 [?36 = 0, >(?37, 0)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      minus(?27', ?28') -> minus(0, -(?28', ?27')) [and(>=(?27', 0), >(?28', ?27'))]
    Outer Rule
      minus(minus(?31", ?32"), ?33") -> minus(?31", +(?32", ?33"))
    Pair
      minus(minus(0, -(?32", ?31")), ?33") ≈ minus(?31", +(?32", ?33")) [and(>=(?31", 0), >(?32", ?31"))]
  reaches the non-trivial normal form
    minus(minus(0, -(?32", ?31")), ?33") ≈ minus(?31", +(?32", ?33")) [and(>=(?31", 0), >(?32", ?31"))]
      -> minus(minus(0, ?324'), ?33") ≈ minus(?31", +(?32", ?33")) [and(>=(?31", 0), >(?32", ?31")), ?324' = -(?32", ?31")]
      ->^* minus(0, +(?324', ?33")) ≈ minus(?31", +(?32", ?33")) [and(>=(?31", 0), >(?32", ?31")), ?324' = -(?32", ?31")]

Elapsed Time: 197.90 ms