YES
LCTRS
  Theories
    Core
  Sorts
    Unit
  Signature
    a: Unit
    b: Unit
    c: Unit
    f: Unit -> Unit
    g: Unit -> Unit
    h: Unit -> Unit
  Rules
    a -> h(c)
    c -> b
    f(a) -> g(b)
    f(h(?2)) -> g(?2)
Confluent by Almost Development Closedness with proof:
    * Critical Pair
      Inner Rule
        a -> h(c)
      Outer Rule
        f(a) -> g(b)
      Pair
        f(h(c)) ≈ g(b)
    which reaches the trivial constrained equation
      f(h(c)) ≈ g(b) 
        -o-> g(b) ≈ g(b) 

Elapsed Time:  92.15 ms