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

Elapsed Time:  66.36 ms