YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    a: Unit
    b: Unit
    c: Unit
    f: Int -> Unit
    g: Int -> Unit
    h: Int -> Unit
  Rules
    f(?13) -> g(?13) [>=(?13, 1)]
    f(?14) -> h(?14) [<=(?14, 2)]
    g(?15) -> a [?15 = 1]
    g(?16) -> b [>=(?16, 2)]
    g(?17) -> c [<(?17, 1)]
    h(?18) -> a [<=(?18, 1)]
    h(?19) -> b [>(?19, 1)]
Confluent by Almost Development Closedness with proof:
    * Critical Pair
      Inner Rule
        f(?14') -> h(?14') [<=(?14', 2)]
      Outer Rule
        f(?13") -> g(?13") [>=(?13", 1)]
      Pair
        h(?13") ≈ g(?13") [<=(?13", 2), >=(?13", 1)]
    is split into the following CCPs and closed as follows:
      ** Critical Pair
        Inner Rule
          f(?14') -> h(?14') [<=(?14', 2)]
        Outer Rule
          f(?13") -> g(?13") [>=(?13", 1)]
        Pair
          h(?13") ≈ g(?13") [>=(?13", 2), not(?13" = 1), <=(?13", 2), >=(?13", 1)]
      which reaches the trivial constrained equation
        h(?13") ≈ g(?13") [>=(?13", 2), not(?13" = 1), <=(?13", 2), >=(?13", 1)]
          -o-> b ≈ g(?13") [>=(?13", 2), not(?13" = 1), <=(?13", 2), >=(?13", 1)]
          -o-> b ≈ b [>=(?13", 2), not(?13" = 1), <=(?13", 2), >=(?13", 1)]
      ** Critical Pair
        Inner Rule
          f(?14') -> h(?14') [<=(?14', 2)]
        Outer Rule
          f(?13") -> g(?13") [>=(?13", 1)]
        Pair
          h(?13") ≈ g(?13") [?13" = 1, <=(?13", 2), >=(?13", 1)]
      which reaches the trivial constrained equation
        h(?13") ≈ g(?13") [?13" = 1, <=(?13", 2), >=(?13", 1)]
          -o-> a ≈ g(?13") [?13" = 1, <=(?13", 2), >=(?13", 1)]
          -o-> a ≈ a [?13" = 1, <=(?13", 2), >=(?13", 1)]
    * Critical Pair
      Inner Rule
        f(?13') -> g(?13') [>=(?13', 1)]
      Outer Rule
        f(?14") -> h(?14") [<=(?14", 2)]
      Pair
        g(?14") ≈ h(?14") [>=(?14", 1), <=(?14", 2)]
    is split into the following CCPs and closed as follows:
      ** Critical Pair
        Inner Rule
          f(?13') -> g(?13') [>=(?13', 1)]
        Outer Rule
          f(?14") -> h(?14") [<=(?14", 2)]
        Pair
          g(?14") ≈ h(?14") [>=(?14", 2), not(?14" = 1), >=(?14", 1), <=(?14", 2)]
      which reaches the trivial constrained equation
        g(?14") ≈ h(?14") [>=(?14", 2), not(?14" = 1), >=(?14", 1), <=(?14", 2)]
          -o-> b ≈ h(?14") [>=(?14", 2), not(?14" = 1), >=(?14", 1), <=(?14", 2)]
          -o-> b ≈ b [>=(?14", 2), not(?14" = 1), >=(?14", 1), <=(?14", 2)]
      ** Critical Pair
        Inner Rule
          f(?13') -> g(?13') [>=(?13', 1)]
        Outer Rule
          f(?14") -> h(?14") [<=(?14", 2)]
        Pair
          g(?14") ≈ h(?14") [?14" = 1, >=(?14", 1), <=(?14", 2)]
      which reaches the trivial constrained equation
        g(?14") ≈ h(?14") [?14" = 1, >=(?14", 1), <=(?14", 2)]
          -o-> a ≈ h(?14") [?14" = 1, >=(?14", 1), <=(?14", 2)]
          -o-> a ≈ a [?14" = 1, >=(?14", 1), <=(?14", 2)]

Elapsed Time: 807.44 ms