NO
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    fun1: (Int, Int) -> Unit
    fun2: (Int, Int, Int) -> Unit
    fun3: (Int, Int) -> Unit
    fun4: (Int, Int) -> Unit
    fun5: (Int, Int) -> Unit
    fun6: (Int, Int) -> Unit
    fun7: (Int, Int) -> Unit
    fun8: (Int, Int) -> Unit
  Rules
    fun1(?50, ?51) -> fun2(?50, ?51, ?52) [and(>(?50, 0), >(?51, 0))]
    fun1(?53, ?54) -> fun8(?53, ?54) [and(<=(?53, 0), <=(?54, 0))]
    fun2(?55, ?56, ?57) -> fun3(?55, ?56) [?57 = 1]
    fun2(?58, ?59, ?60) -> fun6(?58, ?59) [not(?60 = 1)]
    fun3(?61, ?62) -> fun4(-(?61, 1), ?62)
    fun4(?63, ?64) -> fun5(?63, ?65)
    fun5(?66, ?67) -> fun7(?66, ?67)
    fun6(?68, ?69) -> fun7(?68, -(?69, 1))
    fun7(?70, ?71) -> fun1(?70, ?71)
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      fun4(?63', ?64') -> fun5(?63', ?65')
    Outer Rule
      fun4(?63", ?64") -> fun5(?63", ?65")
    Pair
      fun5(?63", ?65') ≈ fun5(?63", ?65") [=(?65', ?65'), =(?65", ?65")]
  reaches the non-trivial normal form
    fun5(?63", ?65') ≈ fun5(?63", ?65") [?65' = ?65', ?65" = ?65"]
      -> fun7(?63", ?65') ≈ fun5(?63", ?65") [?65' = ?65', ?65" = ?65"]
      ->^* fun1(?63", ?65') ≈ fun5(?63", ?65") [?65' = ?65', ?65" = ?65"]
      -> fun1(?63", ?65') ≈ fun7(?63", ?65") [?65' = ?65', ?65" = ?65"]
      -> fun1(?63", ?65') ≈ fun1(?63", ?65") [?65' = ?65', ?65" = ?65"]

Elapsed Time: 552.66 ms